1. Preface
4. 1. Languages
5. 2. Propositional Logic
6. 1. 2.1. Syntax
   2. 2.2. Bare Code
   3. 2.3. Examples
   4. 2.4. Semantics
   5. 2.5. Interpretations
7. 3. Model Theory
8. 1. 3.1. Models
   2. 3.2. Truth Tables
   3. 3.3. Counterexamples
   4. 3.4. Propertiesx
   5. 3.5. Validity
9. 4. Arithmetic
10. 1. 4.1. Domain
    2. 4.2. Syntax
    3. 4.3. Semantics
    4. 4.4. Induction
    5. 4.5. Examples
11. 5. Theory Extensions
12. 1. 5.1. Domain
    2. 5.2. Syntax
    3. 5.3. Semantics
    4. 5.4. Examples
    5. 5.5. Satisfiability Modulo Theories
13. 6. Induction
14. 7. Mathlib
15. 8. (Higher-Order) Predicate Logic
16. 1. 8.1. Introduction
    2. 8.2. Propositions as Data Types
    3. 8.3. Propositions as Logical Types
    4. 8.4. Classical Reasoning
    5. 8.5. Predicates
    6. 8.6. Quantifiers
    7. 1. 8.6.1. For All
       2. 8.6.2. Exists
    8. 8.7. Dependent Type Theory
17. 9. Sets and Relations
18. 1. 9.1. Sets
    2. 9.2. Relations
    3. 9.3. Equality
    4. 9.4. Properties
19. 10. Abstract Algebra
20. 1. 10.1. Groups
    2. 10.2. Actions
    3. 10.3. Torsors over Groups
    4. 10.4. Modules and Vector Spaces
    5. 10.5. Affine Spaces
    6. 10.6. n-Dimensional Spaces
21. 11. Library
22. 1. 11.1. Scalar
    2. 11.2. Tuple
    3. 11.3. Vector
    4. 11.4. Point
    5. 11.5. Torsor
    6. 11.6. Affine
23. 12. Type Heterogeneity
24. 1. 12.1. Heterogeneous Collections
    2. 12.2. Custom Dynamic Types
    3. 12.3. Existential Wrappers
    4. 12.4. Heterogeneous Signatures
    5. 12.5. Heterogeneous Lists
    6. 12.6. Heterogeneous Vectors
    7. 12.7. Sigma Chains
27. Set Up for This Course
28. Learning Resources