-
Notifications
You must be signed in to change notification settings - Fork 297
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix(data/finsupp/basic): add missing
decidable
arguments in lemma s…
…tatements (#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 `classical` tactic in proofs * Using `by haveI := _; exact` in definitions, as `by classical; exact` leaks classicality up to the end of the next section. In a few places this means that `variables` lines have to be repeated on `def`s 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.
- Loading branch information
1 parent
68cc421
commit 2445c98
Showing
3 changed files
with
169 additions
and
94 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.