Zulip Chat Archive

Stream: lean4

Topic: pp.beta


view this post on Zulip Sebastian Reichelt (Mar 21 2021 at 17:40):

Does Lean 4 have something equivalent to set_option pp.beta true in Lean 3? It would be very useful for me. Some other pp options work, but I haven't been able to find a list.

view this post on Zulip Bryan Gin-ge Chen (Mar 21 2021 at 18:03):

You can generate a list of the options using this snippet (maybe something built-in has been added to Lean 4 since then, not sure).

view this post on Zulip Sebastian Reichelt (Mar 21 2021 at 18:44):

Thank you! Interestingly, pp.beta does appear in your list, but when I try it, I get "unknown option pp.beta" (with current nightly).

view this post on Zulip Bryan Gin-ge Chen (Mar 21 2021 at 19:21):

It seems that it was removed since Lean 4.0.0-m1. Here's the output from the latest nightly.


Last updated: May 18 2021 at 23:14 UTC