Skip to content

fix: make FirstTokens.seq (.optTokens _) .unknown return .unkown#13205

Merged
Kha merged 2 commits into
leanprover:masterfrom
Rob23oba:tokens-seq-fix
Apr 1, 2026
Merged

fix: make FirstTokens.seq (.optTokens _) .unknown return .unkown#13205
Kha merged 2 commits into
leanprover:masterfrom
Rob23oba:tokens-seq-fix

Conversation

@Rob23oba
Copy link
Copy Markdown
Contributor

@Rob23oba Rob23oba commented Mar 31, 2026

This PR fixes FirstTokens.seq (.optTokens s) .unknown to return .unknown. This occurs e.g. when an optional (with first tokens .optTokens s) is followed by a parser category (with first tokens .unknown). Previously FirstTokens.seq returned .optTokens s, ignoring the fact that the optional may be empty and then the parser category may have any first token. The correct behavior here is to return .unknown, which indicates that the first token may be anything.

Closes #13203

@Rob23oba Rob23oba marked this pull request as ready for review March 31, 2026 09:31
@github-actions github-actions Bot added the changelog-language Language features and metaprograms label Mar 31, 2026
@Kha
Copy link
Copy Markdown
Member

Kha commented Mar 31, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 31, 2026

Benchmark results for 99a7d7f against 4786e08 are in. There are no significant changes. @Kha

  • build//instructions: -1.0G (-0.01%)

No significant changes detected.

@Kha Kha added this pull request to the merge queue Apr 1, 2026
Merged via the queue into leanprover:master with commit 8b52f4e Apr 1, 2026
21 of 22 checks passed
volodeyka pushed a commit that referenced this pull request Apr 16, 2026
…13205)

This PR fixes `FirstTokens.seq (.optTokens s) .unknown` to return
`.unknown`. This occurs e.g. when an optional (with first tokens
`.optTokens s`) is followed by a parser category (with first tokens
`.unknown`). Previously `FirstTokens.seq` returned `.optTokens s`,
ignoring the fact that the optional may be empty and then the parser
category may have any first token. The correct behavior here is to
return `.unknown`, which indicates that the first token may be anything.

Closes #13203
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms

Projects

None yet

Development

Successfully merging this pull request may close these issues.

(docComment)? before custom syntax category breaks parsing

3 participants