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

Equations

• Lean.Meta.SimpAll.instInhabitedEntry = { default := { fvarId := default, userName := default, id := default, origType := default, type := default, proof := default } }

structure Lean.Meta.SimpAll.State : Type

• modified : Bool
• mvarId : Lean.MVarId
• entries : Array Lean.Meta.SimpAll.Entry
• ctx : Lean.Meta.Simp.Context
• simprocs : Lean.Meta.Simp.SimprocsArray
• usedTheorems : Lean.Meta.Simp.UsedSimps
• diag : Lean.Meta.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 : Lean.Meta.SimpAll.M (Option Lean.MVarId)

Equations

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

def Lean.Meta.simpAll (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) : Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.Stats)

Equations

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