structure Lean.Elab.Term.LetRecDeclView : Type

• ref : Lean.Syntax
• attrs : Array Lean.Elab.Attribute
• shortDeclName : Lake.Name
• declName : Lake.Name
• binderIds : Array Lean.Syntax
• type : Lean.Expr
• mvar : Lean.Expr
• valStx : Lean.Syntax

structure Lean.Elab.Term.LetRecView : Type

• decls : Array Lean.Elab.Term.LetRecDeclView
• body : Lean.Syntax

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