Documentation

Lean.Elab.Extra

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:

      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:

      Equations
      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
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For