Skip to content

chore: remove redundant sepBy1 in subst parser #15029

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mhuisi wants to merge 2 commits into
base: master
Choose a base branch
from
+2 −2
Open

chore: remove redundant sepBy1 in subst parser #15029

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b26ed67
chore: remove redundant `sepBy1` in `subst` parser
mhuisi Jun 11, 2026
416684f
chore: request stage0 update
mhuisi Sep 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Lean/Parser/Term.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -977,7 +977,7 @@ See the Chapter "Quantifiers and Equality" in the manual
"Theorem Proving in Lean" for additional information.
-/
@[builtin_term_parser] def subst := trailing_parser:75
" ▸ " >> sepBy1 (termParser 75) " ▸ "
" ▸ " >> termParser 75

def bracketedBinderF := bracketedBinder -- no default arg
instance : Coe (TSyntax ``bracketedBinderF) (TSyntax ``bracketedBinder) where coe s := ⟨s⟩
Expand Down
2 changes: 1 addition & 1 deletion stage0/src/stdlib_flags.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#include "util/options.h"

// [ ] Check box to force CI to test stage 2 and run update-stage0 on PR merge
// [x] Check box to force CI to test stage 2 and run update-stage0 on PR merge
// (any other change to this file will do the same; ALL changes should be made to the stage0/ copy)

namespace lean {
Expand Down
Loading