Zulip Chat Archive

Stream: lean4

Topic: variable/variables/universe/universes


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Julian Berman (Mar 07 2021 at 02:54):

Hm, in what context? I see:

#check Type u      unknown universe level 'u'

view this post on Zulip Julian Berman (Mar 07 2021 at 02:54):

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

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 03:00):

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

view this post on Zulip Julian Berman (Mar 07 2021 at 03:01):

Thanks, missed that page.

view this post on Zulip 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