Commit 2025-04-12 23:52 b39e9ff7

View on Github →

fix: remove undercover open Classicals (#23750) attribute [local instance] Classical.propDecidable is much worse than open scoped Classical, as it introduces the instance with a default priority that overrides other better decidable instances.

Estimated changes

modified theorem PFunctor.M.ext
modified theorem PFunctor.M.nth_of_bisim
modified theorem Not.imp_symm
modified theorem and_iff_not_or_not
modified theorem and_or_imp
modified theorem beq_eq_decide
modified theorem by_contradiction
modified theorem iff_not_comm
modified theorem imp_iff_not_or
modified theorem imp_iff_or_not
modified theorem imp_iff_right_iff
modified theorem imp_or'
modified theorem imp_or
modified theorem not_and_not_right
modified theorem not_and_or
modified theorem not_forall_not
modified theorem not_forall₂
modified theorem not_iff
modified theorem not_iff_comm
modified theorem not_iff_not
modified theorem not_imp
modified theorem not_imp_comm
modified theorem not_imp_not
modified theorem not_imp_self
modified theorem not_or_of_imp
modified theorem of_not_imp
modified theorem or_congr_right'
modified theorem or_iff_not_and_not
modified theorem or_not_of_imp
modified theorem peirce
modified theorem le_iff_lt_or_eq
modified theorem lt_or_eq_of_le