Documentation

Mathlib.Lean.Meta.Simp

Helper functions for using the simplifier. #

[TODO] Needs documentation, cleanup, and possibly reunification of mkSimpContext' with core.

def Lean.PHashSet.toList {α : Type u_1} [BEq α] [Hashable α] (s : Lean.PHashSet α) :
List α
Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.

    Constructs a proof that the original expression is true given a simp result which simplifies the target to True.

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

      Return all propositions in the local context.

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

        Similar to mkSimpTheoremsFromConst except that it also returns the names of the generated lemmas. Remark: either the length of the arrays is the same, or the length of the first one is 0 and the length of the second one is 1.

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

          Similar to addSimpTheorem except that it returns an array of all auto-generated simp-theorems.

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

            Similar to AttributeImpl.add in mkSimpAttr except that it doesn't require syntax, and returns an array of all auto-generated lemmas.

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

              Similar to AttributeImpl.add in mkSimpAttr except that it returns an array of all auto-generated lemmas.

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

                Construct a SimpTheorems from a list of names.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Lean.Meta.Simp.Context.ofNames (lemmas : optParam (List Lean.Name) []) (simpOnly : optParam Bool false) (config : optParam Lean.Meta.Simp.Config { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := Lean.Meta.EtaStructMode.all, iota := true, proj := true, decide := false, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true, ground := false, unfoldPartialApp := false, zetaDelta := false }) :

                  Construct a Simp.Context from a list of names.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Lean.Meta.simpOnlyNames (lemmas : List Lean.Name) (e : Lean.Expr) (config : optParam Lean.Meta.Simp.Config { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := Lean.Meta.EtaStructMode.all, iota := true, proj := true, decide := false, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true, ground := false, unfoldPartialApp := false, zetaDelta := false }) :

                    Simplify an expression using only a list of lemmas specified by name.

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

                      Given a simplifier S : Expr → MetaM Simp.Result, and an expression e : Expr, run S on the type of e, and then convert e into that simplified type, using a combination of type hints and Eq.mp.

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

                        Independently simplify both the left-hand side and the right-hand side of an equality. The equality is allowed to be under binders. Returns the simplified equality and a proof of it.

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

                          Checks whether declName is in SimpTheorems as either a lemma or definition to unfold.

                          Equations
                          Instances For

                            Tests whether decl has simp-attribute simpAttr. Returns false is simpAttr is not a valid simp-attribute.

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

                              Returns all declarations with the simp-attribute simpAttr. Note: this also returns many auxiliary declarations.

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

                                Gets all simp-attributes given to declaration decl.

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