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

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

      Instances For

        Return all propositions in the local context.

        Instances For

          If ctx == false, the config argument is assumed to have type Meta.Simp.Config, and Meta.Simp.ConfigCtx otherwise. If ctx == false, the discharge option must be none

          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.

            Instances For

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

              Instances For

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

                Instances For

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

                  Instances For

                    Construct a SimpTheorems from a list of names.

                    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 := true, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true }) :

                      Construct a Simp.Context from a list of names.

                      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 := true, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true }) :

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

                        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.

                          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.

                            Instances For

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

                              Instances For

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

                                Instances For

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

                                  Instances For

                                    Gets all simp-attributes given to declaration decl.

                                    Instances For