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 : Lean.PHashSet α) :
List α
Equations
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.

Return all propositions in the local context.

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

Construct a SimpTheorems from a list of names.

Equations
  • One or more equations did not get rendered due to their size.
def Lean.Meta.Simp.Context.ofNames (lemmas : List Lean.Name := []) (simpOnly : Bool := false) (config : 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 := true }) :

Construct a Simp.Context from a list of names.

Equations
  • One or more equations did not get rendered due to their size.
def Lean.Meta.simpOnlyNames (lemmas : List Lean.Name) (e : Lean.Expr) (config : 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 := true }) :

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.

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.

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.

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

Equations

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.

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.

Gets all simp-attributes given to declaration decl.

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