Decompose e into (r, a, b).
Remark: it assumes the last two arguments are explicit.
Instances For
def
Lean.Elab.Term.mkCalcTrans
(result : Lean.Expr)
(resultType : Lean.Expr)
(step : Lean.Expr)
(stepType : Lean.Expr)
 :
Instances For
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.
- _ < 3is annotated
- (_) < 3is not, because it occurs after an atom
- in _ < _only the first one is annotated
- _ + 2 < 3is annotated (not the best heuristic, ideally we'd like to annotate- _ + 2)
- lt _ 3is not, because it occurs after an identifier
Instances For
def
Lean.Elab.Term.getCalcFirstStep
(step0 : Lean.TSyntax `calcFirstStep)
 :
Lean.Elab.TermElabM (Lean.TSyntax `calcStep)
Instances For
def
Lean.Elab.Term.getCalcSteps
(steps : Lean.TSyntax `calcSteps)
 :
Lean.Elab.TermElabM (Array (Lean.TSyntax `calcStep))
Instances For
Instances For
Elaborator for the calc term mode variant.