Documentation

Lean.Elab.MutualDef

structure Lean.Elab.DefViewElabHeader :
Type
Equations
  • Lean.Elab.instInhabitedDefViewElabHeader = { default := { ref := default, modifiers := default, kind := default, shortDeclName := default, declName := default, levelNames := default, binderIds := default, numParams := default, type := default, valueStx := default } }
Equations
Equations
Equations
  • Lean.Elab.Term.MutualClosure.pushLetRecs preDefs letRecClosures kind modifiers = List.foldl (fun preDefs c => let type := Lean.Meta.Closure.mkForall c.localDecls c.toLift.type; let val := Lean.Meta.Closure.mkLambda c.localDecls c.toLift.val; Array.push preDefs { ref := c.ref, kind := kind, levelParams := [], modifiers := { docString? := modifiers.docString?, visibility := modifiers.visibility, isNoncomputable := modifiers.isNoncomputable, recKind := modifiers.recKind, isUnsafe := modifiers.isUnsafe, attrs := c.toLift.attrs }, declName := c.toLift.declName, type := type, value := val }) preDefs letRecClosures
Equations
Equations
structure Lean.Elab.Term.MkInstResult :
Type
Equations
Equations
Equations
Equations