def Lean.Elab.Term.getCalcRelation? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Decompose e into (r, a, b).

Remark: it assumes the last two arguments are explicit.

def Lean.Elab.Term.mkCalcTrans (result : Lean.Expr) (resultType : Lean.Expr) (step : Lean.Expr) (stepType : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

def Lean.Elab.Term.annotateFirstHoleWithType (t : Lean.Term) (type : Lean.Expr) : Lean.Elab.TermElabM Lean.Term

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

partial def Lean.Elab.Term.annotateFirstHoleWithType.go (type : Lean.Expr) (t : Lean.Syntax) : StateT Bool Lean.Elab.TermElabM Lean.Syntax

def Lean.Elab.Term.getCalcFirstStep (step0 : Lean.TSyntax `calcFirstStep) : Lean.Elab.TermElabM (Lean.TSyntax `calcStep)

def Lean.Elab.Term.getCalcSteps (steps : Lean.TSyntax `calcSteps) : Lean.Elab.TermElabM (Array (Lean.TSyntax `calcStep))

def Lean.Elab.Term.elabCalcSteps (steps : Lean.TSyntax `calcSteps) : Lean.Elab.TermElabM Lean.Expr

def Lean.Elab.Term.elabCalc : Lean.Elab.Term.TermElab

Elaborator for the calc term mode variant.