MCPcopy Create free account
hub / github.com/agenticsorg/lean-agentic / DefDecl

Class DefDecl

leanr-syntax/src/ast.rs:28–35  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

26/// Function/constant definition
27#[derive(Debug, Clone, PartialEq)]
28pub struct DefDecl {
29 pub span: Span,
30 pub name: Ident,
31 pub universe_params: Vec<Ident>,
32 pub params: Vec<Param>,
33 pub return_type: Option<Box<Expr>>,
34 pub body: Box<Expr>,
35}
36
37/// Theorem declaration (like def but for proofs)
38#[derive(Debug, Clone, PartialEq)]

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected