Decompose `e`

into `(r, a, b)`

.

Remark: it assumes the last two arguments are explicit.

## Equations

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

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

## Equations

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

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.

`_ < 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 ← StateT.run' (Lean.Elab.Term.annotateFirstHoleWithType.go type t.raw) true pure { raw := __do_lift }

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

Lean.Elab.TermElabM (Lean.TSyntax `calcStep)

## Equations

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

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

Lean.Elab.TermElabM (Array (Lean.TSyntax `calcStep))

## Equations

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

## Equations

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

Elaborator for the `calc`

term mode variant.

## Equations

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