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} [inst : BEq α] [inst : Hashable α] (s : Lean.PHashSet α) :
List α
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
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.

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

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

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.

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.

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.

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.

Construct a SimpTheorems from a list of names. (i.e. as with simp only).

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

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→ 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.

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.