mathlib3
bc72d903 - refactor(logic/basic): classical -> root, root -> decidable (#3812)

Commit
5 years ago
refactor(logic/basic): classical -> root, root -> decidable (#3812) This moves all logic lemmas with `decidable` instances into the `decidable` namespace, and moves or adds classical versions of these to the root namespace. This change hits a lot of files, mostly to remove the `classical.` prefix on explicit references to classical lemmas.
Author
Parents
Loading