Commit 2022-09-30 18:32 c240bdfb
View on Github →feat: add an unset_option command (#422) Adds a user command to unset options, returning them to their default state, this is either a convenience feature, or can be used for the slightly rare instance where unset options behave differently to any particular setting (e.g. pp.proofs). This didn't exist in Lean 3.