Documentation

Lean.Elab.Binders

Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
def Lean.Elab.Term.elabLetDeclAux (id : Lean.Syntax) (binders : Array Lean.Syntax) (typeStx : Lean.Syntax) (valStx : Lean.Syntax) (body : Lean.Syntax) (expectedType? : Option Lean.Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) :
Equations
Equations
Equations
def Lean.Elab.Term.elabLetDeclCore (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) :
Equations