feat: add sym_simproc and sym_discharger DSL syntax categories#13026
Merged
leodemoura merged 1 commit intomasterfrom Mar 21, 2026
Merged
feat: add sym_simproc and sym_discharger DSL syntax categories#13026leodemoura merged 1 commit intomasterfrom
sym_simproc and sym_discharger DSL syntax categories#13026leodemoura merged 1 commit intomasterfrom
Conversation
This PR adds the infrastructure for simproc and discharger DSLs used to specify `pre`/`post` simproc chains and conditional rewrite dischargers in `Sym.simp` variants. Syntax categories: - `sym_simproc` with primitives (`ground`, `telescope`, `rewrite`, `self`, `none`) and combinators (`>>`, `<|>`) - `sym_discharger` with primitives (`self`, `none`) for the `with` clause of `rewrite` Elaboration attributes: - `builtin_sym_simproc` / `sym_simproc` mapping syntax to `Syntax → GrindTacticM Simproc` - `builtin_sym_discharger` / `sym_discharger` mapping syntax to `Syntax → GrindTacticM Discharger` Dispatchers: `elabSymSimproc`, `elabSymDischarger`, `elabWithClause`. Built-in elaborators for each primitive/combinator will follow in a subsequent PR after the stage0 update. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
leodemoura
added
changelog-language
leodemoura
added a commit
that referenced
this pull request
Mar 22, 2026
This PR adds the built-in elaborators for the `sym_simproc` and `sym_discharger` DSL syntax categories introduced in #13026. Simproc elaborators (`@[builtin_sym_simproc]`): - `ground` → `evalGround` - `telescope` → `simpTelescope` - `self` → `simp` (recursive simplification) - `none` → identity (no simplification) - `rewrite setName [with discharger]` → named theorem set rewriting - `rewrite [thm₁, ...] [with discharger]` → inline theorem rewriting - `>>` → `andThen` combinator - `<|>` → `orElse` combinator Discharger elaborators (`@[builtin_sym_discharger]`): - `self` → `dischargeSimpSelf` - `none` → `dischargeNone` Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
github-merge-queue bot
pushed a commit
that referenced
this pull request
Mar 22, 2026
…3031) This PR adds the built-in elaborators for the `sym_simproc` and `sym_discharger` DSL syntax categories introduced in #13026. Simproc elaborators (`@[builtin_sym_simproc]`): - `ground` → `evalGround` - `telescope` → `simpTelescope` - `self` → `simp` (recursive simplification) - `none` → identity (no simplification) - `rewrite setName [with discharger]` → named theorem set rewriting - `rewrite [thm₁, ...] [with discharger]` → inline theorem rewriting - `>>` → `andThen` combinator - `<|>` → `orElse` combinator Discharger elaborators (`@[builtin_sym_discharger]`): - `self` → `dischargeSimpSelf` - `none` → `dischargeNone` Note: `orElse` requires a fully-qualified attribute name (`Lean.Parser.Sym.Simp.orElse`) to avoid a name resolution conflict where the bare `orElse` resolves to a different syntax node kind. --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds the infrastructure for simproc and discharger DSLs used to specify
pre/postsimproc chains and conditional rewrite dischargers inSym.simpvariants.Syntax categories (
src/Init/Sym/Simp/SimprocDSL.lean):sym_simprocwith primitives (ground,telescope,rewrite,self,none) and combinators (>>,<|>)sym_dischargerwith primitives (self,none) for thewithclause ofrewriteElaboration attributes (
src/Lean/Elab/Tactic/Grind/SimprocDSL.lean):builtin_sym_simproc/sym_simprocmapping syntax toSyntax → GrindTacticM Simprocbuiltin_sym_discharger/sym_dischargermapping syntax toSyntax → GrindTacticM DischargerelabSymSimproc,elabSymDischarger, andelabWithClausedispatchersBuilt-in elaborators for each primitive/combinator will follow in a subsequent PR after the stage0 update.