## Stream: lean4

### Topic: variable/variables/universe/universes

#### Julian Berman (Mar 07 2021 at 02:38):

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 (Mar 07 2021 at 02:46):

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

#### Julian Berman (Mar 07 2021 at 02:54):

Hm, in what context? I see:

#check Type u     ■ unknown universe level 'u'


#### Julian Berman (Mar 07 2021 at 02:54):

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

#### Yakov Pechersky (Mar 07 2021 at 03:00):

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

#### Julian Berman (Mar 07 2021 at 03:01):

Thanks, missed that page.

#### Kevin Buzzard (Mar 07 2021 at 08:31):

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

Last updated: May 07 2021 at 12:15 UTC