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 α

@[implicit_reducible]

instance Lean.Meta.Simp.instToFormatSimpTheorems_mathlib : ToFormat SimpTheorems

def Lean.Meta.Simp.Result.ofTrue (r : Result) : MetaM (Option Expr)

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

def Lean.Meta.Simp.getPropHyps : MetaM (Array FVarId)

Return all propositions in the local context.

def Lean.Meta.simpTheoremsOfNames (lemmas : List Name := []) (simpOnly : Bool := false) : MetaM SimpTheorems

Construct a SimpTheorems from a list of names.

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

Construct a Simp.Context from a list of names.

def Lean.Meta.Simp.Context.ofArgs (args : TSyntax `Lean.Parser.Tactic.simpArgs) (config : Config := { }) : Elab.Tactic.TacticM Context

Construct a Simp.Context, following the same algorithm that would be done in a "simp" run: look up all the simp-lemmas in the library, and adjust (add/erase) as specified by the provided simpArgs list.

def Lean.Meta.simpOnlyNames (lemmas : List Name) (e : Expr) (config : Simp.Config := { }) : MetaM Simp.Result

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

def Lean.Meta.simpType (S : Expr → MetaM Simp.Result) (e : Expr) (type? : Option Expr := none) : MetaM Expr

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.

def Lean.Meta.simpEq (S : Expr → MetaM Simp.Result) (type pf : Expr) : MetaM (Expr × 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.

def Lean.Meta.SimpTheorems.contains (d : SimpTheorems) (declName : Name) : Bool

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

def Lean.Meta.isInSimpSet (simpAttr decl : Name) : CoreM Bool

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

def Lean.Meta.getAllSimpDecls (simpAttr : Name) : CoreM (List Name)

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

def Lean.Meta.getAllSimpAttrs (decl : Name) : CoreM (Array Name)

Gets all simp-attributes given to declaration decl.