Documentation

Lean.Meta.Eqns

These options affect the generation of equational theorems in a significant way. For these, their value at definition time, not realization time, should matter.

This is implemented by

  • eagerly realizing the equations when they are set to a non-default value
  • when realizing them lazily, reset the options to their default
Equations
Instances For

    Environment extension for storing which declarations are recursive. This information is populated by the PreDefinition module, but the simplifier uses when unfolding declarations.

    Marks the given declaration as recursive.

    Equations
    Instances For

      Returns true if declName was defined using well-founded recursion, or structural recursion.

      Equations
      Instances For

        Returns true if s is of the form eq_<idx>

        Equations
        Instances For

          Throw an error if names for equation theorems for declName are not available.

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

            Registers 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
              Equations

              Returns some declName if thmName is an equational theorem for declName.

              Equations
              Instances For

                Returns equation theorems for the given declaration.

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

                  If any equation theorem affecting option is not the default value, create the equations now.

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

                    Registers 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

                      Returns an "unfold" theorem (f.eq_def) for the given declaration. By default, we do 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