Definitional Simplifier for SymM

DSimp mirrors Sym.Simp but does not produce proof terms. Every rewrite must hold by definitional equality, so the kernel checks e ≡ e' at the use site and we only need to return the simplified expression.

structure Lean.Meta.Sym.DSimp.Config : Type

Configuration options for the definitional simplifier.

• maxSteps : Nat

  Maximum number of steps that can be performed by the simplifier.

@[implicit_reducible]

instance Lean.Meta.Sym.DSimp.instInhabitedConfig : Inhabited Config

inductive Lean.Meta.Sym.DSimp.Result : Type

The result of definitionally simplifying an expression e.

The done flag controls whether simplification should continue after this result:

• done = false (default): Continue with subsequent simplification steps. If a pre/post method returns .step e' false, dsimp recurses on e'.
• done = true: Stop processing, return this result as final.

Unlike Sym.Simp.Result, this carries no proof term and no contextDependent flag.

• rfl (done : Bool := false) : Result

  No change. If done = true, skip remaining simplification steps for this term.

• step (e' : Expr) (done : Bool := false) : Result

  Simplified to e'. If done = true, skip recursive simplification of e'.

@[implicit_reducible]

instance Lean.Meta.Sym.DSimp.instInhabitedResult : Inhabited Result

def Lean.Meta.Sym.DSimp.MethodsRef : Type

instance Lean.Meta.Sym.DSimp.instNonemptyMethodsRef : Nonempty MethodsRef

structure Lean.Meta.Sym.DSimp.Context : Type

Read-only context for the definitional simplifier.

• config : Config

  Simplifier configuration options.

@[reducible, inline]

abbrev Lean.Meta.Sym.DSimp.Cache : Type

Cache mapping expressions (by pointer equality) to their simplified results.

structure Lean.Meta.Sym.DSimp.State : Type

Mutable state for the definitional simplifier.

• numSteps : Nat

  Number of steps performed so far.

• cache : Cache

  Cache for simplification results. Survives across binder entry.

@[reducible, inline]

abbrev Lean.Meta.Sym.DSimp.DSimpM (α : Type) : Type

Monad for the definitional simplifier, layered on top of SymM.

@[implicit_reducible]

instance Lean.Meta.Sym.DSimp.instInhabitedDSimpM {α : Type} : Inhabited (DSimpM α)

@[reducible, inline]

abbrev Lean.Meta.Sym.DSimp.DSimproc : Type

structure Lean.Meta.Sym.DSimp.Methods : Type

• pre : DSimproc
• post : DSimproc

@[implicit_reducible]

instance Lean.Meta.Sym.DSimp.instInhabitedMethods : Inhabited Methods

unsafe def Lean.Meta.Sym.DSimp.Methods.toMethodsRefImpl (m : Methods) : MethodsRef

@[implemented_by Lean.Meta.Sym.DSimp.Methods.toMethodsRefImpl]

opaque Lean.Meta.Sym.DSimp.Methods.toMethodsRef (m : Methods) : MethodsRef

@[reducible, inline]

unsafe abbrev Lean.Meta.Sym.DSimp.MethodsRef.toMethodsImpl (m : MethodsRef) : Methods

@[implemented_by Lean.Meta.Sym.DSimp.MethodsRef.toMethodsImpl]

opaque Lean.Meta.Sym.DSimp.MethodsRef.toMethods (m : MethodsRef) : Methods

def Lean.Meta.Sym.DSimp.getMethods : DSimpM Methods

def Lean.Meta.Sym.DSimp.DSimpM.run {α : Type} (x : DSimpM α) (methods : Methods := { }) (config : Config := { }) (s : State := { }) : SymM (α × State)

Runs a DSimpM computation with the given methods, configuration, and state. The cache and numSteps from s are preserved (cache entries persist across invocations because results are not context-dependent).

def Lean.Meta.Sym.DSimp.DSimpM.run' {α : Type} (x : DSimpM α) (methods : Methods := { }) (config : Config := { }) : SymM α

Runs a DSimpM computation with the given methods and configuration.

@[extern lean_sym_dsimp]

opaque Lean.Meta.Sym.DSimp.dsimp : DSimproc

def Lean.Meta.Sym.DSimp.getConfig : DSimpM Config

@[reducible, inline]

abbrev Lean.Meta.Sym.DSimp.pre : DSimproc

@[reducible, inline]

abbrev Lean.Meta.Sym.DSimp.post : DSimproc

@[reducible, inline]

abbrev Lean.Meta.Sym.dsimp (e : Expr) (methods : DSimp.Methods := { }) (config : DSimp.Config := { }) : SymM Expr