variable/variables/universe/universes

Stream: lean4

[Julian Berman]

In lean3 there's variable and variables, and universe and universes, with the singular forms taking 1 thing to define and the plural taking many.

In lean4 variable (no s) accepts multiple variables, and the plural form has disappeared, but both universe and universes still exist with the lean3 semantics (that universe accepts only 1 universe). Is there a particular reason for the difference?

[Yakov Pechersky]

You'll also notice that you don't even have to say universe u for things like Type u to work

[Julian Berman]

Hm, in what context? I see:

#check Type u     ■ unknown universe level 'u'

[Julian Berman]

Oh interesting, but def foo (n : Type u) := 12 works

[Yakov Pechersky]

https://leanprover.github.io/lean4/doc/autobound.html

[Julian Berman]

Thanks, missed that page.

[Kevin Buzzard]

This looks like a recipe for chaos :-) I'm really glad there's the option to switch it off :-) It might just be one of those things which looks frightening but after a while you realise that once you've not made any typos then it makes for super clean code