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

• s.toList = List.map (fun (x : α × Unit) => x.fst) s.set.toList

instance Lean.Meta.Simp.instToFormatSimpTheorems_mathlib : ToFormat SimpTheorems

Equations

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

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.

Equations

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

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

Return all propositions in the local context.

Equations

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

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

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 Name := []) (simpOnly : Bool := false) (config : Config := { }) : MetaM Context

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

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

Equations

• d.contains declName = (d.isLemma (Lean.Meta.Origin.decl declName) || d.isDeclToUnfold declName)

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.

Equations

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

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

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.

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

Gets all simp-attributes given to declaration decl.

Equations

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