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

Equations

• Lean.Meta.Sym.DSimp.instInhabitedConfig = { default := Lean.Meta.Sym.DSimp.instInhabitedConfig.default }

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

Equations

• Lean.Meta.Sym.DSimp.instInhabitedResult = { default := Lean.Meta.Sym.DSimp.instInhabitedResult.default }

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

Equations

• Lean.Meta.Sym.DSimp.MethodsRef = Lean.Meta.Sym.DSimp.MethodsRefPointed✝.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.

Equations

• Lean.Meta.Sym.DSimp.Cache = Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.DSimp.Result

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.

Equations

• Lean.Meta.Sym.DSimp.DSimpM = ReaderT Lean.Meta.Sym.DSimp.MethodsRef (ReaderT Lean.Meta.Sym.DSimp.Context (StateRefT' IO.RealWorld Lean.Meta.Sym.DSimp.State Lean.Meta.Sym.SymM))

@[implicit_reducible]

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

Equations

• Lean.Meta.Sym.DSimp.instInhabitedDSimpM = { default := Lean.throwError (Lean.toMessageData "<default>") }

@[reducible, inline]

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

Equations

• Lean.Meta.Sym.DSimp.DSimproc = (Lean.Expr → Lean.Meta.Sym.DSimp.DSimpM Lean.Meta.Sym.DSimp.Result)

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

• pre : DSimproc
• post : DSimproc

@[implicit_reducible]

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

Equations

• Lean.Meta.Sym.DSimp.instInhabitedMethods = { default := Lean.Meta.Sym.DSimp.instInhabitedMethods.default }

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

Equations

• m.toMethodsRefImpl = unsafeCast m

@[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

Equations

• m.toMethodsImpl = unsafeCast m

@[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

Equations

• Lean.Meta.Sym.DSimp.getMethods = do let __do_lift ← read pure __do_lift.toMethods

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).

Equations

• x.run methods config s = (x methods.toMethodsRef { config := config }).run { cache := s.cache }

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.

Equations

• x.run' methods config = (x methods.toMethodsRef { config := config }).run' { }

@[extern lean_sym_dsimp]

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

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

Equations

• Lean.Meta.Sym.DSimp.getConfig = do let __do_lift ← readThe Lean.Meta.Sym.DSimp.Context pure __do_lift.config

@[reducible, inline]

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

Equations

• Lean.Meta.Sym.DSimp.pre e = do let __do_lift ← Lean.Meta.Sym.DSimp.getMethods __do_lift.pre e

@[reducible, inline]

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

Equations

• Lean.Meta.Sym.DSimp.post e = do let __do_lift ← Lean.Meta.Sym.DSimp.getMethods __do_lift.post e

@[reducible, inline]

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

Equations

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