Zulip Chat Archive

Stream: new members

Topic: Not, false and empty.


view this post on Zulip Pedro Minicz (Jun 11 2020 at 00:42):

Why not has type Prop → Prop and not Sort* → Prop? I believe inferring the universe level should be doable is almost every case.

view this post on Zulip Jalex Stark (Jun 11 2020 at 00:47):

does not : Sort* \to Prop have useful lemmas?

view this post on Zulip Jalex Stark (Jun 11 2020 at 00:49):

i guess Q \imp P \imp (\not P \imp \not Q) works for this sort of not

view this post on Zulip Jalex Stark (Jun 11 2020 at 00:49):

but where would you use it?

view this post on Zulip Pedro Minicz (Jun 11 2020 at 00:55):

Say I have an uncountable type α, i.e. there isn't a bijection between α and the naturals, then I could express that by ¬denumerable α.

view this post on Zulip Pedro Minicz (Jun 11 2020 at 04:21):

¬ nonempty (encodable ℝ)

view this post on Zulip Pedro Minicz (Jun 11 2020 at 04:21):

How does the universe hierarchy work in Lean?

view this post on Zulip Johan Commelin (Jun 11 2020 at 11:34):

@Pedro Minicz Not sure what you mean, but you have Type u := Sort (u+1), and for universe levels, you basically have a succ function, and max.

view this post on Zulip Reid Barton (Jun 11 2020 at 12:12):

And it's noncumulative, so each (fully elaborated) type belongs to just one universe

view this post on Zulip Pedro Minicz (Jun 11 2020 at 14:51):

I see. Sort 0 is an impredicative universe, right?

view this post on Zulip Johan Commelin (Jun 11 2020 at 14:51):

I think it is (-;


Last updated: May 13 2021 at 20:13 UTC