structure Lean.Meta.SimpAll.Entry : Type

• fvarId : Lean.FVarId
• userName : Lake.Name
• id : Lean.Meta.Origin
• origType : Lean.Expr
• type : Lean.Expr
• proof : Lean.Expr

instance Lean.Meta.SimpAll.instInhabitedEntry : Inhabited Lean.Meta.SimpAll.Entry

structure Lean.Meta.SimpAll.State : Type

• modified : Bool
• mvarId : Lean.MVarId
• entries : Array Lean.Meta.SimpAll.Entry
• ctx : Lean.Meta.Simp.Context
• usedSimps : Lean.Meta.Simp.UsedSimps

@[inline, reducible]

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

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

def Lean.Meta.simpAll (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.UsedSimps)