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 : Lean.Expr) (resultType : Lean.Expr) (step : Lean.Expr) (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

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

Equations

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

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

Equations

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

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

Equations

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

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.