From 8766649eea2c006faa130e6245fc35763bde36f0 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Thu, 18 Jul 2024 22:43:42 -0400
Subject: [PATCH] bit more cleanup and add missing documentation

---
 docs/reference/collections.rst |  4 ++++
 docs/reference/sum-pattern.rst | 25 +++++++++++++++++++++++++
 docs/reference/syntax.rst      |  2 +-
 docs/reference/type-annot.rst  | 28 ++++++++++++++++++++++++++++
 docs/reference/types.rst       |  1 -
 docs/reference/void.rst        |  7 +++++++
 6 files changed, 65 insertions(+), 2 deletions(-)
 create mode 100644 docs/reference/sum-pattern.rst
 create mode 100644 docs/reference/type-annot.rst
 create mode 100644 docs/reference/void.rst

diff --git a/docs/reference/collections.rst b/docs/reference/collections.rst
index cebe4005..e0a2fdf4 100644
--- a/docs/reference/collections.rst
+++ b/docs/reference/collections.rst
@@ -9,6 +9,10 @@ used on them.
 
 .. toctree::
 
+   list
+   string
+   set
+   bag
    size
    cp
    ellipsis
diff --git a/docs/reference/sum-pattern.rst b/docs/reference/sum-pattern.rst
new file mode 100644
index 00000000..186f19b3
--- /dev/null
+++ b/docs/reference/sum-pattern.rst
@@ -0,0 +1,25 @@
+Sum patterns
+============
+
+A sum :doc:`pattern <pattern>` consists of a value of a :doc:`sum type
+<sum-type>` used as a pattern, that is, either ``left(P)`` or
+``right(P)``, where ``P`` is some pattern.  For example,
+
+::
+
+   f : (N + List(Char)) -> N
+   f(left(n))    = n
+   f(right(str)) = |str|
+
+This is how we can write a function that takes an input with multiple
+possibilities, and decides what to do with each possibility.
+
+The arguments to ``left`` and ``right`` can themselves be any pattern,
+not just variables.  For example,
+
+::
+
+   f : (N + Q) -> N
+   f(left(2n+1)) = 17
+   f(left(2n)) = 18
+   f(right(q)) = abs(floor(q))
diff --git a/docs/reference/syntax.rst b/docs/reference/syntax.rst
index e1762f67..14563bbe 100644
--- a/docs/reference/syntax.rst
+++ b/docs/reference/syntax.rst
@@ -18,4 +18,4 @@ grammar", that is, the various ways to write valid Disco programs.
    case
    comment
    docs
-   tydef
+   typedef
diff --git a/docs/reference/type-annot.rst b/docs/reference/type-annot.rst
new file mode 100644
index 00000000..567834b5
--- /dev/null
+++ b/docs/reference/type-annot.rst
@@ -0,0 +1,28 @@
+Type annotations
+================
+
+A *type annotation* is like a :doc:`type signature <type-sig>`, but
+instead of being on a line by itself, a type annotation is part of an
+:doc:`expression <expression>`.  After any expression we can put a
+colon and a type to indicate to Disco what type we want that
+expression to be.  For example, if we ask Disco for the type of ``2 +
+3``, Disco infers it to be a natural number.
+
+::
+
+   Disco> :type 2 + 3
+   2 + 3 : ℕ
+
+However, if we use a type annotation to specify that the ``2`` should
+specifically be thought of as an integer, then Disco infers that the
+whole expression is also an integer:
+
+::
+
+   Disco> :type (2 : Z) + 3
+   (2 : ℤ) + 3 : ℤ
+
+Often, type annotations are useful as documentation: putting a
+type annotation on one part of a complex expression helps you better
+express your intent, and helps Disco potentially generate better error
+messages if you make a mistake.
diff --git a/docs/reference/types.rst b/docs/reference/types.rst
index 4b97333a..466ece6e 100644
--- a/docs/reference/types.rst
+++ b/docs/reference/types.rst
@@ -34,6 +34,5 @@ is a :doc:`subtype <subtypes>` of the one it was expecting.
    type-annot
    algebraic-types
    typedef
-   collection-types
    prop
    subtypes
diff --git a/docs/reference/void.rst b/docs/reference/void.rst
new file mode 100644
index 00000000..4dc9466d
--- /dev/null
+++ b/docs/reference/void.rst
@@ -0,0 +1,7 @@
+Void type
+=========
+
+``Void`` is a special built-in type with *no* values.
+
+This is not very useful on its own, but is included for completeness;
+it can also come in handy in some more advanced situations.