The largest universe

Stream: lean4

[Mario Carneiro]

def foo := Sort 33

maximum universe level offset threshold (32) has been reached, you can increase the limit using option set_option maxUniverseOffset <limit>, but you are probably misusing universe levels since offsets are usually small natural numbers

I feel like I've been told off :oops:

[Johan Commelin]

Why would you ever want to use Sort 33 :stuck_out_tongue_wink: :rofl: ?

[Johan Commelin]

The message says "probably", and I agree with that.

[Mario Carneiro]

Interestingly I can use Type 32

[Gabriel Ebner]

You can also use Sort (32+1)

[Kevin Buzzard]

Great that we have a workaround

[Mac]

Johan Commelin said:

Why would you ever want to use Sort 33 :stuck_out_tongue_wink: :rofl: ?

I concur with this. I am extremely curious as to the circumstances under which you discovered this. Why would Sort 33 ever be a thing you encountered?

[Mario Carneiro]

I just saw it while browsing the source. There was once a zulip topic about someone causing lean 3 to get really slow (much worse than expectation) on large universes (Lean 3 has no such limiter) and I think Type 600 came up there

[Chris B]

This is an evergreen:
https://twitter.com/derKha/status/1164846192888598528?s=20

theory vs practice https://twitter.com/derKha/status/1164846192888598528/photo/1

- Sebastian Ullrich (@derKha)

[Damiano Testa]

This reminds me of a famous adage: “In theory, theory and practice are the same. In practice, they are not.”