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.

Equations

• Lean.Elab.Term.getCalcRelation? e = if e.getAppNumArgs < 2 then pure none else pure (some (e.appFn!.appFn!, e.appFn!.appArg!, e.appArg!))

def Lean.Elab.Term.mkCalcTrans (result resultType step 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 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

Equations

• Lean.Elab.Term.annotateFirstHoleWithType t type = do let __do_lift ← (Lean.Elab.Term.annotateFirstHoleWithType.go type t.raw).run' true pure { raw := __do_lift }

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

structure Lean.Elab.Term.CalcStepView : Type

View of a calcStep.

• ref : Lean.Syntax
• term : Lean.Term

  A relation term like a ≤ b

• proof : Lean.Term

  A proof of term

instance Lean.Elab.Term.instInhabitedCalcStepView : Inhabited Lean.Elab.Term.CalcStepView

Equations

• Lean.Elab.Term.instInhabitedCalcStepView = { default := { ref := default, term := default, proof := default } }

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

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

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

def Lean.Elab.Term.throwCalcFailure {α : Type} (steps : Array Lean.Elab.Term.CalcStepView) (expectedType result : Lean.Expr) : Lean.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 : Lean.Elab.Term.TermElab

Elaborator for the calc term mode variant.

Equations

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