Commit 2023-01-20 18:38 2445c98aView on Github →
fix(data/finsupp/basic): add missing
decidable arguments in lemma statements (#18241)
The resulting lemmas are more general than they were before.
In order to ensure that this doesn't regress again,
open_locale classical is now also removed from these files.
Instead, we use the approach of:
- Using the
classicaltactic in proofs
by haveI := _; exactin definitions, as
by classical; exactleaks classicality up to the end of the next section. In a few places this means that
variableslines have to be repeated on
defs as Lean doesn't look inside tactic blocks to work out which variables are used. I also switched some anonymous constructors for named constructors in order to make the proof / data distinction a little easier to see.