bit more cleanup and add missing documentation

docs/reference/collections.rst

@@ -9,6 +9,10 @@ used on them.
 
 .. toctree::
 
+   list
+   string
+   set
+   bag
    size
    cp
    ellipsis

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))

docs/reference/syntax.rst

@@ -18,4 +18,4 @@ grammar", that is, the various ways to write valid Disco programs.
    case
    comment
    docs
-   tydef
+   typedef

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.

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

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.