Keywords in a syntax category are reserved everywhere?

Stream: lean4

[Chris Wong]

If I add a keyword to a syntax category, Lean seems to reserve it everywhere, such that I can't use it as an identifier at all. Is this intended behavior?

import Mathlib

inductive Animal where | dog

declare_syntax_cat animal
-- Uncomment this line to break the code below
-- syntax "dog" : animal

open Animal in
#check dog

open Animal in
example : Animal := dog

example (a : Animal) : True := by
  cases a
  case dog => trivial

The #xy is that I created a Tetris DSL, and discovered that I can't write case O anymore. I can probably change the syntax to match general idents instead but I'm curious why Lean works this way.

[Robin Arnez]

I think this is intended, you can add (behavior := both) or (behavior := symbol) to the end of your syntax category declaration and it will not reserve keywords everywhere.

[Chris Wong]

Nice, thanks!

The doc comment for that option sounds like my use case.

I've added (behavior := symbol) to my code and that seems to fix it.