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
elaboratesf a b
as a binary operator with two operandsa
andb
, and each operand participates in the protocol.binop_lazy% f a b
is likebinop%
but elaborates asf a (fun () => b)
.unop% f a
elaboratesf a
as a unary operator with one operanda
, which participates in the protocol.leftact% f a b
elaboratesf a b
as a left action (thea
operand "acts upon" theb
operand). Onlyb
participates in the protocol sincea
can have an unrelated type, for example scalar multiplication of vectors.rightact% f a b
elaboratesf a b
as a right action (theb
operand "acts upon" thea
operand). Onlya
participates in the protocol sinceb
can have an unrelated type. This is used byHPow
since, for example, there are bothReal > Nat > Real
andReal > Real > Real
exponentiation functions, and we prefer the former in the case ofx ^ 2
, butbinop%
would choose the latter. (#2220) There are also
binrel%
andbinrel_no_prop%
(see the docstring forelabBinRelCore
).
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 atbinop%
elaboration time. This was not the case in the old elaborator. For example, an instance, such asHAdd Int ?m ?n
, could be created when executing thebinop%
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
andy : Matrix Real 4 8
, there is no coercionMatrix Real 5 4
fromMatrix Real 4 8
and viceversa, butx * y
is elaborated successfully and has typeMatrix Real 5 8
. 
The
leftact%
andrightact%
elaborators are to handle binary operations where only one of the arguments participates in the protocol. For example, in2 ^ n + y
withn : Nat
andy : Real
, we do not want to coercen
to be a real as well, but we do want to elaborate2 : 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
elaboratesR x y
using thebinop%/...
expression trees in bothx
andy
. It is similar to howbinop% R x y
elaborates but with a significant difference: it does not use the expected type when computing the types of the operads.binrel_no_prop% R x y
elaboratesR x y
likebinrel% R x y
, but if the resulting type forx
andy
isProp
they are coerced toBool
. This is used for relations such as==
which do not supportProp
, 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.