DMT1/DMT1.lean at main · WontonCoder/DMT1 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
-- -- This module serves as the root of the `DMT1` library.
-- -- Import modules here that should be built as part of the library.

import DMT1.L00_deductiveReasoning.axiomsAndInference
import DMT1.L00_deductiveReasoning.theorems
import DMT1.L00_deductiveReasoning.preview

-- -- propositional logic
-- import DMT1.L02_propLogic.utilities
-- import DMT1.L02_propLogic.domain
-- import DMT1.L02_propLogic.syntax
-- import DMT1.L02_propLogic.interpretation
-- import DMT1.L02_propLogic.axioms
-- import DMT1.L02_propLogic.demo
-- import DMT1.L02_propLogic.identities

-- -- model theory
-- import DMT1.L03_modelTheory.models
-- import DMT1.L03_modelTheory.truthTable
-- import DMT1.L03_modelTheory.properties
-- import DMT1.L03_modelTheory.validity
-- import DMT1.L03_modelTheory.counterexamples

-- -- arithmetic
-- import DMT1.L04_natArithmetic.syntax
-- import DMT1.L04_natArithmetic.domain
-- import DMT1.L04_natArithmetic.semantics
-- import DMT1.L04_natArithmetic.induction
-- import DMT1.L04_natArithmetic.examples

-- -- theory extensions
-- import DMT1.L05_theoryExtensions.domain
-- import DMT1.L05_theoryExtensions.examples
-- import DMT1.L05_theoryExtensions.semantics
-- import DMT1.L05_theoryExtensions.syntax
-- import DMT1.L05_theoryExtensions

-- -- induction again
-- import DMT1.L06_induction.induction

-- -- predicate logic
-- import DMT1.L07_predicateLogic.00_introduction
-- import DMT1.L07_predicateLogic.01_propsAsCompTypes
-- import DMT1.L07_predicateLogic.02_propsAsLogicalTypes
-- import DMT1.L07_predicateLogic.03_classicalReasoning
-- import DMT1.L07_predicateLogic.04_predicates
-- import DMT1.L07_predicateLogic.05_quantifiers_all
-- import DMT1.L07_predicateLogic.06_quantifiers_exists
-- import DMT1.L07_predicateLogic.07_quantifiers

-- -- set theory
-- import DMT1.L08_setsRelationsFunctions.sets
-- import DMT1.L08_setsRelationsFunctions.relations
-- import DMT1.L08_setsRelationsFunctions.equality
-- import DMT1.L08_setsRelationsFunctions.properties
-- import DMT1.L08_setsRelationsFunctions.multisets