Helper functions for using the simplifier.

[TODO] Needs documentation, cleanup, and possibly reunification of mkSimpContext' with core.

def Lean.PHashSet.toList {α : Type u_1} [BEq α] [Hashable α] (s : Lean.PHashSet α) : List α

Equations

• Lean.PHashSet.toList s = List.map (fun x => x.fst) (Lean.PersistentHashMap.toList s.set)

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

Equations

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

def Lean.Meta.Simp.mkEqSymm (e : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.mkCast (r : Lean.Meta.Simp.Result) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Lean.Meta.Simp.mkCast r e = do let __do_lift ← Lean.Meta.Simp.Result.getProof r Lean.Meta.mkAppM `cast #[__do_lift, e]

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.Simp.mkSimpContext' (simpTheorems : Lean.Meta.SimpTheorems) (stx : Lean.Syntax) (eraseLocal : Bool) (kind : optParam Lean.Elab.Tactic.SimpKind Lean.Elab.Tactic.SimpKind.simp) (ctx : optParam Bool false) (ignoreStarArg : optParam Bool false) : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.MkSimpContextResult

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.

def Lean.Meta.Simp.mkSimpTheoremsFromConst' (declName : Lean.Name) (post : Bool) (inv : Bool) (prio : Nat) : Lean.MetaM (Array Lean.Name × Array Lean.Meta.SimpTheorem)

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.

def Lean.Meta.Simp.addSimpTheorem' (ext : Lean.Meta.SimpExtension) (declName : Lean.Name) (post : Bool) (inv : Bool) (attrKind : Lean.AttributeKind) (prio : Nat) : Lean.MetaM (Array Lean.Name)

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.

def Lean.Meta.Simp.addSimpAttr (declName : Lean.Name) (ext : Lean.Meta.SimpExtension) (attrKind : Lean.AttributeKind) (post : Bool) (prio : Nat) : Lean.MetaM (Array Lean.Name)

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.

def Lean.Meta.Simp.addSimpAttrFromSyntax (declName : Lean.Name) (ext : Lean.Meta.SimpExtension) (attrKind : Lean.AttributeKind) (stx : Lean.Syntax) : Lean.MetaM (Array Lean.Name)

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.

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 := true, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true }) : 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 := true, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true }) : Lean.MetaM Lean.Meta.Simp.Result

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

Equations

• Lean.Meta.simpOnlyNames lemmas e config = do let __do_lift ← Lean.Meta.Simp.Context.ofNames lemmas true config (fun x => x.fst) <$> Lean.Meta.simp e __do_lift none ∅

def Lean.Meta.simpType (S : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result) (e : Lean.Expr) : 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 and Eq.mp.

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

• Lean.Meta.SimpTheorems.contains d declName = (Lean.Meta.SimpTheorems.isLemma d (Lean.Meta.Origin.decl declName) || Lean.Meta.SimpTheorems.isDeclToUnfold d 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.