Commit 2022-07-01 15:19 ecd37441
View on Github →fix: make (command|...) produce correct type ([#297](https://github.com/leanprover-community/mathlib4/pull/297)) Apparently the elaborated type of a syntax quotation depends on the kind name, which needs to be command.quotso that we get ``TSyntaxcommand``.