Skip to content

feat: add register_sym_simp command and SymSimpVariant infrastructure#13034

Merged
leodemoura merged 1 commit intomasterfrom
lean-sym-interactive-5
Mar 22, 2026
Merged

feat: add register_sym_simp command and SymSimpVariant infrastructure#13034
leodemoura merged 1 commit intomasterfrom
lean-sym-interactive-5

Conversation

@leodemoura
Copy link
Copy Markdown
Member

This PR adds the register_sym_simp command for declaring named Sym.simp
variants with pre/post simproc chains and optional config overrides.

register_sym_simp myVariant where
  pre  := telescope
  post := ground >> rewrite [thm1, thm2] with self
  maxSteps := 50000
  • SymSimpVariant structure storing pre?/post? syntax (elaborated at use
    time in GrindTacticM) and Config overrides
  • SimpleScopedEnvExtension for persistent cross-module variant storage
  • register_sym_simp command syntax with sym_simp_field category
  • Command elaborator with syntax quotation matching and duplicate field detection
  • getSymSimpVariant? lookup function
  • deriving Inhabited on Simp.Config for extension support

…ture

This PR adds the `register_sym_simp` command for declaring named `Sym.simp`
variants with `pre`/`post` simproc chains and optional config overrides.

- `SymSimpVariant` structure storing `pre`/`post` syntax (elaborated at use
  time) and `Config` overrides
- `SimpleScopedEnvExtension` for persistent cross-module variant storage
- `register_sym_simp` command syntax with `sym_simp_field` category
- Command elaborator parsing fields and registering variants
- `getSymSimpVariant?` lookup function
- `deriving Inhabited` on `Simp.Config` for extension support

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@leodemoura leodemoura requested a review from kim-em as a code owner March 22, 2026 04:21
@leodemoura leodemoura added changelog-language Language features and metaprograms changelog-tactics User facing tactics and removed changelog-language Language features and metaprograms labels Mar 22, 2026
@leodemoura leodemoura enabled auto-merge March 22, 2026 04:22
@leodemoura leodemoura added this pull request to the merge queue Mar 22, 2026
Merged via the queue into master with commit 13f8ce8 Mar 22, 2026
31 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