2b55144c3f
This PR adds `SymExtension`, a typed extensible state mechanism for `SymM`, following the same pattern as `Grind.SolverExtension`. Extensions are registered at initialization time via `registerSymExtension` and provide typed `getState`/`modifyState` accessors. Extension state persists across `simp` invocations within a `sym =>` block and is re-initialized on each `SymM.run`. This enables modules (e.g., the upcoming arithmetic normalizer) to register persistent state without modifying `Sym.State` directly. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
20 lines
500 B
Text
20 lines
500 B
Text
/-
|
|
Declare a SymExtension and register it.
|
|
-/
|
|
module
|
|
public import Lean.Meta.Sym.SymM
|
|
open Lean Meta Sym
|
|
|
|
/-- Simple counter state for testing. -/
|
|
public structure MyExtState where
|
|
counter : Nat := 0
|
|
deriving Inhabited
|
|
|
|
initialize myExt : SymExtension MyExtState ←
|
|
registerSymExtension (return {})
|
|
|
|
public def getMyCounter : SymM Nat := do
|
|
return (← myExt.getState).counter
|
|
|
|
public def incrementMyCounter : SymM Unit := do
|
|
myExt.modifyState fun s => { s with counter := s.counter + 1 }
|