Documentation

Lean.Meta.Eqns

Register a new function for retrieving equation theorems. We generate equations theorems on demand, and they are generated by more than one module. For example, the structural and well-founded recursion modules generate them. Most recent getters are tried first.

A getter returns an Option (Array Name). The result is none if the getter failed. Otherwise, it is a sequence of theorem names where each one of them corresponds to an alternative. Example: the definition

def f (xs : List Nat) : List Nat :=
  match xs with
  | [] => []
  | x::xs => (x+1)::f xs

should have two equational theorems associated with it

f [] = []

and

(x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Return equation theorems for the given declaration. By default, we not create equation theorems for nonrecursive definitions. You can use nonRec := true to override this behavior, a dummy rfl proof is created on the fly.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Register a new function for retrieving a "unfold" equation theorem.

      We generate this kind of equation theorem on demand, and it is generated by more than one module. For example, the structural and well-founded recursion modules generate it. Most recent getters are tried first.

      A getter returns an Option Name. The result is none if the getter failed. Otherwise, it is a theorem name. Example: the definition

      def f (xs : List Nat) : List Nat :=
        match xs with
        | [] => []
        | x::xs => (x+1)::f xs
      

      should have the theorem

      (xs : Nat) →
        f xs =
          match xs with
          | [] => []
          | x::xs => (x+1)::f xs
      
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Return a "unfold" theorem for the given declaration. By default, we not create unfold theorems for nonrecursive definitions. You can use nonRec := true to override this behavior.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For