structure Lean.Meta.SimpAll.Entry : Type

• fvarId : FVarId
• userName : Name
• id : Origin
• origType : Expr
• type : Expr
• proof : Expr

@[instance_reducible]

instance Lean.Meta.SimpAll.instInhabitedEntry : Inhabited Entry

Equations

• Lean.Meta.SimpAll.instInhabitedEntry = { default := Lean.Meta.SimpAll.instInhabitedEntry.default }

structure Lean.Meta.SimpAll.State : Type

• modified : Bool
• mvarId : MVarId
• entries : Array Entry
• ctx : Simp.Context
• simprocs : Simp.SimprocsArray
• usedTheorems : Simp.UsedSimps
• diag : Simp.Diagnostics

@[reducible, inline]

abbrev Lean.Meta.SimpAll.M (α : Type) : Type

Equations

• Lean.Meta.SimpAll.M = StateRefT' IO.RealWorld Lean.Meta.SimpAll.State Lean.MetaM

def Lean.Meta.SimpAll.main : M (Option MVarId)

Equations

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

def Lean.Meta.simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (stats : Simp.Stats := { }) : MetaM (Option MVarId × Simp.Stats)

Equations

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