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} [BEq α] [Hashable α] (s : PHashSet α) :
List α
Equations
    Instances For

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

      Equations
        Instances For

          Return all propositions in the local context.

          Equations
            Instances For

              Construct a SimpTheorems from a list of names.

              Equations
                Instances For
                  def Lean.Meta.Simp.Context.ofNames (lemmas : List Name := []) (simpOnly : Bool := false) (config : Config := { }) :

                  Construct a Simp.Context from a list of names.

                  Equations
                    Instances For
                      def Lean.Meta.simpOnlyNames (lemmas : List Name) (e : Expr) (config : Simp.Config := { }) :

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

                      Equations
                        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
                            Instances For
                              def Lean.Meta.simpEq (S : ExprMetaM Simp.Result) (type pf : Expr) :

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

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

                                  Equations
                                    Instances For
                                      def Lean.Meta.isInSimpSet (simpAttr decl : Name) :

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

                                      Equations
                                        Instances For

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

                                          Equations
                                            Instances For

                                              Gets all simp-attributes given to declaration decl.

                                              Equations
                                                Instances For