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

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

instance Lean.Meta.Simp.instToFormatSimpTheorems_mathlib : Lean.ToFormat Lean.Meta.SimpTheorems

Equations

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

def Lean.Meta.Simp.Result.ofTrue (r : Lean.Meta.Simp.Result) : Lean.MetaM (Option Lean.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 : Lean.MetaM (Array Lean.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 : optParam (List Lean.Name) []) (simpOnly : optParam Bool false) : Lean.MetaM Lean.Meta.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 : optParam (List Lean.Name) []) (simpOnly : optParam Bool false) (config : optParam 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 := false }) : Lean.MetaM Lean.Meta.Simp.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.simpOnlyNames (lemmas : List Lean.Name) (e : Lean.Expr) (config : optParam 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 := false }) : Lean.MetaM Lean.Meta.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 : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result) (e : Lean.Expr) (type? : optParam (Option Lean.Expr) none) : Lean.MetaM Lean.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 : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result) (type : Lean.Expr) (pf : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.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 : Lean.Meta.SimpTheorems) (declName : Lean.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 true) || d.isDeclToUnfold declName)

def Lean.Meta.isInSimpSet (simpAttr : Lean.Name) (decl : Lean.Name) : Lean.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 : Lean.Name) : Lean.CoreM (List Lean.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 : Lean.Name) : Lean.CoreM (Array Lean.Name)

Gets all simp-attributes given to declaration decl.

Equations

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