tests/lean/syntaxPrec.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            syntax "foo" term <|> "bar" term : term  -- should not compile

            
            set_option trace.Elab.command true

            
            syntax "foo" ("*" <|> term,+) : term
	syntax "foo" term <\|> "bar" term : term -- should not compile
	set_option trace.Elab.command true
	syntax "foo" ("*" <\|> term,+) : term