structure Lean.Elab.Term.LetRecDeclView : Type

• ref : Syntax
• attrs : Array Attribute
• shortDeclName : Name
• declName : Name
• binderIds : Array Syntax
• type : Expr
• mvar : Expr
• valStx : Syntax
• termination : TerminationHints

structure Lean.Elab.Term.LetRecView : Type

• decls : Array LetRecDeclView
• body : Syntax

def Lean.Elab.Term.elabLetRec : TermElab