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