Auxiliary elaboration functions: AKA custom elaborators #

source

def Lean.Elab.Term.elabForIn :

Lean.Elab.Term.TermElab

Equations

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

Instances For

source

def Lean.Elab.Term.elabForIn' :

Lean.Elab.Term.TermElab

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. (#2220)
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.

source

instance Lean.Elab.Term.Op.instBEqBinOpKind :

BEq Lean.Elab.Term.Op.BinOpKind

Equations

Lean.Elab.Term.Op.instBEqBinOpKind = { beq := Lean.Elab.Term.Op.beqBinOpKind✝ }

source

def Lean.Elab.Term.Op.elabOp :

Lean.Elab.Term.TermElab

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

source

def Lean.Elab.Term.Op.elabBinOp :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.Op.elabBinOp = Lean.Elab.Term.Op.elabOp

Instances For

source

def Lean.Elab.Term.Op.elabBinOpLazy :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.Op.elabBinOpLazy = Lean.Elab.Term.Op.elabOp

Instances For

source

def Lean.Elab.Term.Op.elabLeftact :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.Op.elabLeftact = Lean.Elab.Term.Op.elabOp

Instances For

source

def Lean.Elab.Term.Op.elabRightact :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.Op.elabRightact = Lean.Elab.Term.Op.elabOp

Instances For

source

def Lean.Elab.Term.Op.elabUnOp :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.Op.elabUnOp = Lean.Elab.Term.Op.elabOp

Instances For

source

def Lean.Elab.Term.Op.elabBinRelCore (noProp : Bool) (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) :

Lean.Elab.TermElabM Lean.Expr

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 operads.
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.