# Auxiliary elaboration functions: AKA custom elaborators #

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

The elaborator for expression trees of `binop%`

, `binop_lazy%`

, `leftact%`

, `rightact%`

, and `unop%`

terms.

At a high level, the elaborator tries to solve for a type that each of the operands in the expression tree can be coerced to, while taking into account the expected type for the entire expression tree. Once this type is computed (and if it exists), it inserts coercions where needed.

Here are brief descriptions of each of the operator types:

`binop% f a b`

elaborates`f a b`

as a binary operator with two operands`a`

and`b`

, and each operand participates in the protocol.`binop_lazy% f a b`

is like`binop%`

but elaborates as`f a (fun () => b)`

.`unop% f a`

elaborates`f a`

as a unary operator with one operand`a`

, which participates in the protocol.`leftact% f a b`

elaborates`f a b`

as a left action (the`a`

operand "acts upon" the`b`

operand). Only`b`

participates in the protocol since`a`

can have an unrelated type, for example scalar multiplication of vectors.`rightact% f a b`

elaborates`f a b`

as a right action (the`b`

operand "acts upon" the`a`

operand). Only`a`

participates in the protocol since`b`

can have an unrelated type. This is used by`HPow`

since, for example, there are both`Real -> Nat -> Real`

and`Real -> Real -> Real`

exponentiation functions, and we prefer the former in the case of`x ^ 2`

, but`binop%`

would choose the latter. (#2854)- There are also
`binrel%`

and`binrel_no_prop%`

(see the docstring for`elabBinRelCore`

).

The elaborator works as follows:

1- Expand macros.
2- Convert `Syntax`

object corresponding to the `binop%/...`

term into a `Tree`

.
The `toTree`

method visits nested `binop%/...`

terms and parentheses.
3- Synthesize pending metavariables without applying default instances and using the
`(mayPostpone := true)`

.
4- Tries to compute a maximal type for the tree computed at step 2.
We say a type α is smaller than type β if there is a (nondependent) coercion from α to β.
We are currently ignoring the case we may have cycles in the coercion graph.
If there are "uncomparable" types α and β in the tree, we skip the next step.
We say two types are "uncomparable" if there isn't a coercion between them.
Note that two types may be "uncomparable" because some typing information may still be missing.
5- We traverse the tree and inject coercions to the "maximal" type when needed.

Recall that the coercions are expanded eagerly by the elaborator.

Properties:

a) Given `n : Nat`

and `i : Nat`

, it can successfully elaborate `n + i`

and `i + n`

. Recall that Lean 3
fails on the former.

b) The coercions are inserted in the "leaves" like in Lean 3.

c) There are no coercions "hidden" inside instances, and we can elaborate

```
axiom Int.add_comm (i j : Int) : i + j = j + i
example (n : Nat) (i : Int) : n + i = i + n := by
rw [Int.add_comm]
```

Recall that the `rw`

tactic used to fail because our old `binop%`

elaborator would hide
coercions inside of a `HAdd`

instance.

Remarks:

In the new

`binop%`

and related elaborators the decision whether a coercion will be inserted or not is made at`binop%`

elaboration time. This was not the case in the old elaborator. For example, an instance, such as`HAdd Int ?m ?n`

, could be created when executing the`binop%`

elaborator, and only resolved much later. We try to minimize this problem by synthesizing pending metavariables at step 3.For types containing heterogeneous operators (e.g., matrix multiplication), step 4 will fail and we will skip coercion insertion. For example,

`x : Matrix Real 5 4`

and`y : Matrix Real 4 8`

, there is no coercion`Matrix Real 5 4`

from`Matrix Real 4 8`

and vice-versa, but`x * y`

is elaborated successfully and has type`Matrix Real 5 8`

.The

`leftact%`

and`rightact%`

elaborators are to handle binary operations where only one of the arguments participates in the protocol. For example, in`2 ^ n + y`

with`n : Nat`

and`y : Real`

, we do not want to coerce`n`

to be a real as well, but we do want to elaborate`2 : Real`

.

## Equations

## Equations

- Lean.Elab.Term.Op.elabOp stx expectedType? = do let __do_lift ← Lean.Elab.Term.Op.toTree stx Lean.Elab.Term.Op.toExpr __do_lift expectedType?

## Instances For

## Instances For

## Instances For

## Instances For

## Instances For

## Instances For

Elaboration functions for `binrel%`

and `binrel_no_prop%`

notations.
We use the infrastructure for `binop%`

to make sure we propagate information between the left and right hand sides
of a binary relation.

`binrel% R x y`

elaborates`R x y`

using the`binop%/...`

expression trees in both`x`

and`y`

. It is similar to how`binop% R x y`

elaborates but with a significant difference: it does not use the expected type when computing the types of the operands.`binrel_no_prop% R x y`

elaborates`R x y`

like`binrel% R x y`

, but if the resulting type for`x`

and`y`

is`Prop`

they are coerced to`Bool`

. This is used for relations such as`==`

which do not support`Prop`

, but we still want to be able to write`(5 > 2) == (2 > 1)`

for example.

## Equations

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

## Instances For

If `noProp == true`

and `e`

has type `Prop`

, then coerce it to `Bool`

.

## Equations

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

## Instances For

## Instances For

## Equations

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