Abstract simplifier API

inductive Lean.Meta.MonadSimp.Result : Type

• rfl : Result
• step (e h : Expr) : Result

def Lean.Meta.MonadSimp.instInhabitedResult.default : Result

Equations

• Lean.Meta.MonadSimp.instInhabitedResult.default = Lean.Meta.MonadSimp.Result.rfl

@[implicit_reducible]

instance Lean.Meta.MonadSimp.instInhabitedResult : Inhabited Result

Equations

• Lean.Meta.MonadSimp.instInhabitedResult = { default := Lean.Meta.MonadSimp.instInhabitedResult.default }

class Lean.Meta.MonadSimp (m : Type → Type) : Type 1

• withNewLemmas {α : Type} (xs : Array Expr) (k : m α) : m α
• dsimp : Expr → m Expr
• simp : Expr → m Result