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


            
            syntax "foo " (" bar " ident)? : tactic


            macro_rules

            
              -- should not complain about `$id` not being a valid command and create a snapshot for it

            
              | `(tactic| foo $[bar $id]) => sorry
	syntax "foo " (" bar " ident)? : tactic

	macro_rules
	-- should not complain about `$id` not being a valid command and create a snapshot for it
	\| `(tactic\| foo $[bar $id]) => sorry