variables v subtype

Stream: lean4

[Kevin Buzzard]

universe u

variable {A : Type u} -- fine

variables {B : Type u} {n : Nat} -- expected '//'
-- error on `u`, presumably subtype notation?

Workaround: use variable not variables when declaring implicit variables.

[Yakov Pechersky]

I think there is only variable now, and you don't have to declare universe u.

[Yakov Pechersky]

https://leanprover.github.io/lean4/doc/sections.html?highlight=variable#variables-and-sections
https://leanprover.github.io/lean4/doc/autobound.html

[Leonardo de Moura]

We have fixed the error message. We now get "expected command" at variables.

[Kevin Buzzard]

I'm sorry for the noise! I was actually looking at some lean 4 files written by maths undergraduates here and they had used variables but their code was giving me an error with the most recent nightly.

[Leonardo de Moura]

There is no variables command in Lean 4. We should always use variable.
In my last comment, I was pointing out that the error message is now "sane". If one uses variables or another invalid command, we get "error: command expected" at the right position.