8b52f4e8f7
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
10 lines
172 B
Text
10 lines
172 B
Text
import Lean.Elab.Command
|
|
|
|
open Lean Elab Command
|
|
|
|
declare_syntax_cat myKeyword
|
|
syntax "foo" : myKeyword
|
|
|
|
elab (docComment)? myKeyword ident : command => pure ()
|
|
|
|
foo hello
|