# Documentation

Lean.Elab.Calc

Decompose e into (r, a, b).

Remark: it assumes the last two arguments are explicit.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.mkCalcTrans (result : Lean.Expr) (resultType : Lean.Expr) (step : Lean.Expr) (stepType : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.

Adds a type annotation to a hole that occurs immediately at the beginning of the term. This is so that coercions can trigger when elaborating the term. See https://github.com/leanprover/lean4/issues/2040 for futher rationale.

• _ < 3 is annotated
• (_) < 3 is not, because it occurs after an atom
• in _ < _ only the first one is annotated
• _ + 2 < 3 is annotated (not the best heuristic, ideally we'd like to annotate _ + 2)
• lt _ 3 is not, because it occurs after an identifier
Equations
• = do let __do_lift ← pure { raw := __do_lift }
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.elabCalcSteps (steps : Lean.TSyntax calcSteps) :
Equations
• One or more equations did not get rendered due to their size.

Elaborator for the calc` term mode variant.

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