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)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.