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

        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, index := true, implicitDefEqProofs := 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, index := true, implicitDefEqProofs := 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 as well as casting if the proof is not definitional Eq.mp.

              The optional argument type?, if present, must be definitionally equal to the type of e. When it is specified we simplify this type rather than the inferred type of e.

              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