Skip to content

feat: add extensible state mechanism for SymM#13080

Merged
leodemoura merged 1 commit intomasterfrom
lean-sym-arith
Mar 24, 2026
Merged

feat: add extensible state mechanism for SymM#13080
leodemoura merged 1 commit intomasterfrom
lean-sym-arith

Conversation

@leodemoura
Copy link
Copy Markdown
Member

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

This PR add `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.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@leodemoura leodemoura added changelog-language Language features and metaprograms changelog-tactics User facing tactics and removed changelog-language Language features and metaprograms labels Mar 24, 2026
@leodemoura leodemoura enabled auto-merge March 24, 2026 03:46
@leodemoura leodemoura added this pull request to the merge queue Mar 24, 2026
Merged via the queue into master with commit 2b55144 Mar 24, 2026
33 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant