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
              Equations
                Instances For
                  Equations
                    Instances For

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

                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For

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

                                  Equations
                                    Instances For
                                      Equations
                                        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
                                            Instances For
                                              Instances For

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

                                                Equations
                                                  Instances For

                                                    Returns true if thmName is an equational theorem.

                                                    Equations
                                                      Instances For

                                                        Returns equation theorems for the given declaration.

                                                        Equations
                                                          Instances For

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

                                                            Equations
                                                              Instances For
                                                                Equations
                                                                  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
                                                                      Instances For
                                                                        def Lean.Meta.getUnfoldEqnFor? (declName : Name) (nonRec : Bool := false) :

                                                                        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
                                                                          Instances For