Should `universe u v` generate an error?

Stream: lean4

[Alex Zani]

When I type universe u v I get the following error:

expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term

Is that expected? The line universe u v appears in the docs here: https://leanprover.github.io/lean4/doc/dep.html and universe u v w which generates the same error appears here: https://leanprover.github.io/lean4/doc/autobound.html

[Alex Zani]

I am using lean4 in emacs with lean-mode. The status line does tell me it's lean 4, I'm happy to run other diagnostics if it would help.

[Sebastian Reichelt]

Are you possibly on an old version of Lean 4? The syntax was changed from universes u v to universe u v somewhat recently.

[Alex Zani]

@Sebastian Reichelt Maybe... $ lean --version Lean (version 4.0.0-m2, commit 26dda3f63d88, Release)

[Alex Zani]

OK, it looks like universes was removed in June, so that's probably it. Thanks!