Declaring new syntax for greater universes

Stream: lean4

[Gabriel Ebner]

I would have expected this to work (and it works if I swap term and level). Am I doing something wrong or is this a bug?

syntax "frob " term : level
-- unknown attribute [levelParser]

[Mario Carneiro]

syntax "frob" : level doesn't work either. I guess level isn't a syntax category?

[Patrick Massot]

mathlib4 is moving faster than I thought. I'd never think we'd already be doing Frobenius morphisms.

[Kevin Buzzard]

this is great news, because we're having trouble with them in Lean 3...

[Sebastian Ullrich]

Mario Carneiro said:

I guess level isn't a syntax category?

It is a category for builtin parsers only. Changing that wouldn't immediately be of any help because it does not have support for macros or elaborators (probably unnecessary?) either yet.

[Gabriel Ebner]

What I want is similar to Type (← frob). The ← frob is then lifted before expansion, so I wouldn't even need level macros.

[Gabriel Ebner]

For now I can live with the following workaround, but it would be really great if the level parsers were extensible.

syntax "Type" "(" "←" term ")" : term
syntax "Sort" "(" "←" term ")" : term