Decompose `e`

into `(r, a, b)`

.

Remark: it assumes the last two arguments are explicit.

## Equations

## Instances For

## Equations

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

## 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 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 }

## Instances For

View of a `calcStep`

.

- ref : Lean.Syntax
- term : Lean.Term
A relation term like

`a ≤ b`

- proof : Lean.Term
A proof of

`term`

## Instances For

## Equations

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

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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.

Elaborator for the `calc`

term mode variant.

## Equations

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