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

Decompose e into (r, a, b).

Remark: it assumes the last two arguments are explicit.

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

def Lean.Elab.Term.annotateFirstHoleWithType (t : Term) (type : Expr) : TermElabM 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 further 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 : Expr) (t : Syntax) : StateT Bool TermElabM Syntax

structure Lean.Elab.Term.CalcStepView : Type

View of a calcStep.

• ref : Syntax
• term : Term

  A relation term like a ≤ b

• proof : Term

  A proof of term

instance Lean.Elab.Term.instInhabitedCalcStepView : Inhabited CalcStepView

def Lean.Elab.Term.mkCalcFirstStepView (step0 : TSyntax `Lean.calcFirstStep) : TermElabM CalcStepView

def Lean.Elab.Term.mkCalcStepViews (steps : TSyntax `Lean.calcSteps) : TermElabM (Array CalcStepView)

def Lean.Elab.Term.elabCalcSteps (steps : Array CalcStepView) : TermElabM (Expr × Expr)

def Lean.Elab.Term.throwCalcFailure {α : Type} (steps : Array CalcStepView) (expectedType result : Expr) : MetaM α

Warning! It is very tempting to try to improve calc so that it makes use of the expected type to unify with the LHS and RHS. Two people have already re-implemented elabCalcSteps trying to do so and then reverted the changes, not being aware of examples like https://github.com/leanprover/lean4/issues/2073

The problem is that the expected type might need to be unfolded to get an accurate LHS and RHS. (Consider ≤ vs ≥. Users expect to be able to use calc to prove ≥ using chained ≤!) Furthermore, the types of the LHS and RHS do not need to be the same (consider x ∈ S as a relation), so we also cannot use the expected LHS and RHS as type hints.

def Lean.Elab.Term.elabCalc : TermElab

Elaborator for the calc term mode variant.