structure Lean.Meta.Simp.Result : Type

• expr : Lean.Expr
• proof? : Option Lean.Expr
• dischargeDepth : Nat

instance Lean.Meta.Simp.instInhabitedResult : Inhabited Lean.Meta.Simp.Result

@[inline, reducible]

abbrev Lean.Meta.Simp.Cache : Type

@[inline, reducible]

abbrev Lean.Meta.Simp.CongrCache : Type

structure Lean.Meta.Simp.Context : Type

• config : Lean.Meta.Simp.Config
• simpTheorems : Lean.Meta.SimpTheoremsArray
• congrTheorems : Lean.Meta.SimpCongrTheorems
• parent? : Option Lean.Expr
• dischargeDepth : Nat

instance Lean.Meta.Simp.instInhabitedContext : Inhabited Lean.Meta.Simp.Context

def Lean.Meta.Simp.Context.isDeclToUnfold (ctx : Lean.Meta.Simp.Context) (declName : Lake.Name) : Bool

def Lean.Meta.Simp.Context.mkDefault : Lean.MetaM Lean.Meta.Simp.Context

@[inline, reducible]

abbrev Lean.Meta.Simp.UsedSimps : Type

structure Lean.Meta.Simp.State : Type

• cache : Lean.Meta.Simp.Cache
• congrCache : Lean.Meta.Simp.CongrCache
• usedTheorems : Lean.Meta.Simp.UsedSimps
• numSteps : Nat

@[inline, reducible]

abbrev Lean.Meta.Simp.SimpM (α : Type) : Type

instance Lean.Meta.Simp.instMonadBacktrackSavedStateSimpM : Lean.MonadBacktrack Lean.Meta.SavedState Lean.Meta.SimpM

inductive Lean.Meta.Simp.Step : Type

• visit: Lean.Meta.Simp.Result → Lean.Meta.Simp.Step
• done: Lean.Meta.Simp.Result → Lean.Meta.Simp.Step

instance Lean.Meta.Simp.instInhabitedStep : Inhabited Lean.Meta.Simp.Step

def Lean.Meta.Simp.Step.result : Lean.Meta.Simp.Step → Lean.Meta.Simp.Result

def Lean.Meta.Simp.Step.updateResult : Lean.Meta.Simp.Step → Lean.Meta.Simp.Result → Lean.Meta.Simp.Step

structure Lean.Meta.Simp.Methods : Type

• pre : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
• post : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
• discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)

instance Lean.Meta.Simp.instInhabitedMethods : Inhabited Lean.Meta.Simp.Methods

@[inline, reducible]

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

def Lean.Meta.Simp.pre (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Step

def Lean.Meta.Simp.post (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Step

def Lean.Meta.Simp.discharge? (e : Lean.Expr) : Lean.Meta.Simp.M (Option Lean.Expr)

def Lean.Meta.Simp.getConfig : Lean.Meta.Simp.M Lean.Meta.Simp.Config

@[inline]

def Lean.Meta.Simp.withParent {α : Type} (parent : Lean.Expr) (f : Lean.Meta.Simp.M α) : Lean.Meta.Simp.M α

def Lean.Meta.Simp.getSimpTheorems : Lean.Meta.Simp.M Lean.Meta.SimpTheoremsArray

def Lean.Meta.Simp.getSimpCongrTheorems : Lean.Meta.Simp.M Lean.Meta.SimpCongrTheorems

@[inline]

def Lean.Meta.Simp.withSimpTheorems {α : Type} (s : Lean.Meta.SimpTheoremsArray) (x : Lean.Meta.Simp.M α) : Lean.Meta.Simp.M α

def Lean.Meta.Simp.recordSimpTheorem (thmId : Lean.Meta.Origin) : Lean.Meta.SimpM Unit