decidable/classical

Stream: mathlib4

[Johan Commelin]

Did something fundamental change between Lean 3 / Lean 4 with respect to decidability?

What is going on with https://github.com/leanprover-community/mathlib4/pull/1753/files#diff-1d6e9102ebec04f1d702ffef68445fa574ac5c8b80c9a9e9c577c6b47a5e6625R132-R141 (Order.OrderIsoNat)

Also in https://github.com/leanprover-community/mathlib4/pull/1807 (Data.Finsupp.Defs) there are simp/rw lemmas that aren't triggering because of decidability issues.

[Eric Wieser]

This is almost certainly because the classical tactic leaks in lean3

[Eric Wieser]

That is, using it in one proof can have the effect of seeming like it was used in all later proofs within the section

[Eric Wieser]

I have no idea whether the lean 4 tactic has inherited this behavior