Resolve "Classical logic" ✨️
Closes #78 🐔️👍️ Approved-by:belazy <aarthuur01@gmail.com> Approved-by:
aalbert <augustin.albert@bleu-azure.fr> 🦀️
🍰 🦀️🍰 🦀️🍰 * chore(std): clarify separation of definitions across files + manual formatting * chore: define std folder and reorganise madeleine files structure * fixup: merge parts of contraposition and classical Two new files bool.mdln and connectives.mdln containing True, False, And, Or, Not. Also harmonized naming conventions: Prop and functions returning Prop (like And) start with a capital letter, lemmas (whose type is itself a Prop) are lowercased. * feat: Resolve "Classical logic" (#78) Add a classical.mdln file with three characterizations of excluded middle.
Showing
- examples/and.mdln 0 additions, 9 deletionsexamples/and.mdln
- examples/contraposition.mdln 0 additions, 4 deletionsexamples/contraposition.mdln
- examples/eq.mdln 2 additions, 21 deletionsexamples/eq.mdln
- examples/irrelevance.mdln 5 additions, 5 deletionsexamples/irrelevance.mdln
- examples/nat_eq.mdln 0 additions, 28 deletionsexamples/nat_eq.mdln
- proost/src/main.rs 1 addition, 1 deletionproost/src/main.rs
- std/eq.mdln 30 additions, 0 deletionsstd/eq.mdln
- std/nat.mdln 9 additions, 0 deletionsstd/nat.mdln
- std/prop/classical.mdln 106 additions, 0 deletionsstd/prop/classical.mdln
- std/prop/connectives.mdln 38 additions, 0 deletionsstd/prop/connectives.mdln
- std/prop/contraposition.mdln 6 additions, 0 deletionsstd/prop/contraposition.mdln
- std/prop/false.mdln 2 additions, 0 deletionsstd/prop/false.mdln
Loading
Please register or sign in to comment