Skip to content

Commit

Permalink
stub out the rest of the gentle introduction
Browse files Browse the repository at this point in the history
  • Loading branch information
byorgey committed Dec 25, 2024
1 parent 4b57afe commit d3c5e13
Show file tree
Hide file tree
Showing 8 changed files with 72 additions and 0 deletions.
8 changes: 8 additions & 0 deletions docs/introduction/algebraic.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
Algebraic data types
====================

.. admonition:: To be written

- Sum types
- Type definitions
- Recursive types (lists, trees)
13 changes: 13 additions & 0 deletions docs/introduction/booleans.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@

Booleans and Logic
==================

.. admonition:: To be written

- Introduce type `Bool`, values `T` and `F`
- Introduce logic operators (and, or, not, implies, iff)
- Mention `:table` command
- Introduce basic comparison operators
- Introduce basic tests
- Exercises:
- xor
7 changes: 7 additions & 0 deletions docs/introduction/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -24,3 +24,10 @@ more detail on some particular topic.
variables
arithmetic
functions
booleans
number-theory
pairs
sets
lists
polymorphism
algebraic
8 changes: 8 additions & 0 deletions docs/introduction/lists.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
Lists
=====

.. admonition:: To be written

- Literal lists, ellipsis notation
- List comprehensions
- Basic recursion patterns (motivate polymorphism)
14 changes: 14 additions & 0 deletions docs/introduction/number-theory.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
Number Theory
=============

.. admonition:: To be written

- Integer division
- Mod
- Divisibility
- Quantified tests
- Tests can start with `forall` or `exists`
- Explain syntax.
- `Prop` vs `Bool`.
- `holds`
- Exercises
7 changes: 7 additions & 0 deletions docs/introduction/pairs.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Pairs and pattern matching
==========================

.. admonition:: To be written

- Pairs, product type
- Basic pattern matching
6 changes: 6 additions & 0 deletions docs/introduction/polymorphism.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Polymorphism
============

.. admonition:: To be written

Polymorphic list functions
9 changes: 9 additions & 0 deletions docs/introduction/sets.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Sets
====

.. admonition:: To be written

- Basic literal sets
- Ellipsis notation
- Set operations (union, intersection, difference, size, cartesian product, power set)
- Set comprehensions

0 comments on commit d3c5e13

Please sign in to comment.