Zulip Chat Archive

Stream: lean4

Topic: universe options

András Kovács (Jul 22 2021 at 12:59):

Hi everyone! Is there are any way right now in Lean 4 to turn off universe checking? Or at least get impredicative base universe? I'd like to get Church-encoded data for benchmarking purposes.

Sebastian Ullrich (Jul 22 2021 at 13:12):

Hi András, I'm afraid there isn't. You can kind of circumvent it by unsafeCasting e.g. to NonScalar, but that's not very pretty.

András Kovács (Jul 24 2021 at 07:38):

Thanks. It turns out I can define everything I need predicatively.

Last updated: Dec 20 2023 at 11:08 UTC