Zulip Chat Archive

Stream: new members

Topic: Not, false and empty.


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.

Jalex Stark (Jun 11 2020 at 00:47):

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

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

Jalex Stark (Jun 11 2020 at 00:49):

but where would you use it?

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 α.

Pedro Minicz (Jun 11 2020 at 04:21):

¬ nonempty (encodable ℝ)

Pedro Minicz (Jun 11 2020 at 04:21):

How does the universe hierarchy work in Lean?

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.

Reid Barton (Jun 11 2020 at 12:12):

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

Pedro Minicz (Jun 11 2020 at 14:51):

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

Johan Commelin (Jun 11 2020 at 14:51):

I think it is (-;


Last updated: Dec 20 2023 at 11:08 UTC