Change Simplifier Options Globally

Stream: lean4

[David E. Narváez]

Some recent changes in the default configuration of the simplifier broke most of the proofs we had. Is there a way to configure the simplifier "globally" so that we do not have to change every use via simp (config := {...})?

[Kyle Miller]

Could you please give more details about what broke and what configuration you're wanting to set?

[David E. Narváez]

This change set the default for zetaDetla to false and we need it set back to true.

[Kyle Miller]

Option 1: write simp +zetaDelta when you need it (no need for the whole (config := { zetaDelta := true }) these days)

[Kyle Miller]

Option 2: define your own simp tactic, like

declare_simp_like_tactic zsimp "zsimp " +zetaDelta

and then replace failing simps with zsimps.

[Kyle Miller]

Option 3: (big hack, not recommended) make a macro to insert +zsimp in simp when it's not already present.

[Kyle Miller]

But to answer your question, no, there's no way to set the global simp configuration, except for this hack in option 3.