source
structure Lean.Elab.Term.LetRecDeclView :
Type

- ref : Syntax
- attrs : Array Attribute
- shortDeclName : Name
- declName : Name
- parentName? : Option Name
- binderIds : Array Syntax
- type : Expr
- mvar : Expr
- valStx : Syntax
- termination : TerminationHints

Instances For

source
structure Lean.Elab.Term.LetRecView :
Type

- decls : Array LetRecDeclView
- body : Syntax

Instances For

source
def Lean.Elab.Term.elabLetRec :
TermElab
Equations

- One or more equations did not get rendered due to their size.

Instances For