updates to reference documentation

docs/reference/bag.rst

@@ -0,0 +1,99 @@
+Bags
+====
+
+For any :doc:`type <types>` ``T``, ``Bag(T)`` is the type of *finite
+bags* with elements of type ``T``.  A bag is like a :doc:`set` (and
+unlike a :doc:`list`) in that it doesn't care about the order of the
+elements; however, unlike a :doc:`set`, a bag cares *how many copies*
+of each element there are.
+
+* The built-in ``bag`` function can be used to convert other
+  collections (*e.g.* :doc:`sets <set>` or :doc:`lists <list>`) to bags.
+
+    ::
+
+       Disco> bag([])
+       ⟅⟆
+       Disco> bag({1,2,3})
+       ⟅1, 2, 3⟆
+       Disco> bag("hello")
+       ⟅'e', 'h', 'l' # 2, 'o'⟆
+
+* Notice how single elements are simply listed by themselves, but
+  elements occuring more than once are written with a ``#`` followed
+  by a natural number.  You can write bags this way yourself:
+
+    ::
+
+       Disco> ⟅'a' # 2, 'b' # 3⟆
+       ⟅'a' # 2, 'b' # 3⟆
+       Disco> ⟅'a' # 2, 'b' # 1⟆
+       ⟅'a' # 2, 'b'⟆
+       Disco> ⟅'a' # 0, 'b' # 1⟆
+       ⟅'b'⟆
+
+* Of course, entering the ``⟅⟆`` characters can be difficult, so you
+  can also just stick with entering bags via the ``bag`` function.
+
+* One common place where bags show up is in the output of the ``factor``
+  function (from the ``num`` standard library module) for representing
+  the prime factorization of a natural number.  In a prime
+  factorization, the *order* of the prime factors does not matter (since
+  multiplication is commutative), but it matters how many copies there
+  are of each factor.
+
+    ::
+
+       Disco> import num
+       Disco> factor(10)
+       ⟅2, 5⟆
+       Disco> factor(12)
+       ⟅2 # 2, 3⟆
+       Disco> factor(64)
+       ⟅2 # 6⟆
+
+* Just as with :doc:`lists <list>` and :doc:`sets <set>`, an
+  :doc:`ellipsis <ellipsis>` can be used to generate a range of
+  elements in a bag.  For example,
+
+    ::
+
+       Disco> ⟅'a' .. 'e'⟆
+       ⟅'a', 'b', 'c', 'd', 'e'⟆
+       Disco> ⟅1, 3 .. 9⟆
+       ⟅1, 3, 5, 7, 9⟆
+
+* :doc:`Comprehension <comprehension>` notation can also be used,
+  for example:
+
+    ::
+
+       Disco> ⟅ abs(x - 5) | x in ⟅1 .. 10⟆, x^2 > 5 ⟆
+       ⟅0, 1 # 2, 2 # 2, 3, 4, 5⟆
+
+* The order of elements in a bag does not matter, but the number of
+  copies of each element does matter.  Two bags with the same elements
+  in a different order are considered the same, whereas two bags with
+  the same elements but a different number of copies of each are
+  considered different.  For example,
+
+    ::
+
+       Disco> ⟅1,2,3⟆ == ⟅1,3,2⟆
+       T
+       Disco> ⟅1,2,3⟆ == ⟅1,1,2,3⟆
+       F
+
+* To check whether a bag contains a given element at least once, one can
+  use the ``elem`` operator (also written ``∈``):
+
+    ::
+
+       Disco> 2 elem ⟅1,2,3⟆
+       T
+       Disco> 5 elem ⟅1,2,3⟆
+       F
+       Disco> 2 ∈ ⟅1,2,3⟆
+       T
+
+XXX operations on bags: intersection, union, power

docs/reference/bool.rst

@@ -2,8 +2,8 @@ Booleans
 ========
 
 The type of *booleans* is written ``Bool`` or ``Boolean``.  There are
-exactly two values of type ``Boolean``: ``false`` and ``true`` (which
-can also be written ``False`` and ``True``).
+exactly two values of type ``Boolean``: ``F`` and ``T`` (which
+can also be written ``False`` and ``True``, or ``false`` and ``true``).
 
 :doc:`Logical operators <logic-ops>` can be used to manipulate
 ``Boolean`` values, and expressions of type ``Boolean`` can be used as

docs/reference/compare.rst

@@ -15,7 +15,7 @@ can be compared:
 ::
 
    Disco> {(3, "hi"), (4, "there"), (6, "world")} < {(10, "what")}
-   true
+   T
 
 See the individual pages about each type for more information on how
 comparison works on values of that type.
@@ -36,9 +36,9 @@ many.
     ::
 
        Disco> 3 == 5
-       false
+       F
        Disco> "hi" == "hi"
-       true
+       T
 
   Equality is one critical point where Disco syntax has to deviate
   from standard mathematical notation: be sure to keep in mind the

docs/reference/comprehension.rst

@@ -24,10 +24,10 @@ Examples
 
    Disco> {x | x in {1..5}}   -- same as {1..5}
    {1, 2, 3, 4, 5}
-   
+
    Disco> {3x | x in {1..5}}  -- multiply each element of {1..5} by 3
    {3, 6, 9, 12, 15}
-   
+
    -- Pick out the elements of {1..10} that satisfy the condition
    Disco> {x | x in {1 .. 10}, x^2 + 20 == 9x}
    {4, 5}
@@ -50,7 +50,7 @@ Details
 Each *qualifier* in a comprehension can be either
 
 * a *variable binding* of the form ``<variable> in <set>``, *e.g.* ``x
-  in {1 .. 10}`` or ``b in {false, true}``, or
+  in {1 .. 10}`` or ``b in {F, T}``, or
 * a *guard*, which can be any :doc:`boolean <bool>` expression.
 
 A variable binding locally defines a variable and causes it to "loop" through

docs/reference/divides.rst

@@ -9,20 +9,20 @@ example:
 ::
 
    Disco> 3 divides 6
-   true
+   T
    Disco> 6 divides 3
-   false
+   F
    Disco> 3 divides (-6)
-   true
+   T
    Disco> 5 divides 5
-   true
+   T
    Disco> 4 divides 6
-   false
+   F
    Disco> 0 divides 10
-   false
+   F
    Disco> 10 divides 0
-   true
+   T
    Disco> 0 divides 0
-   true
+   T
    Disco> 1/2 divides 3/2
-   true
+   T

docs/reference/expression.rst

@@ -25,5 +25,5 @@ Examples of things which are *not* expressions include:
    Be careful not to confuse ``x = 3`` (a :doc:`definition <definition>`
    of the :doc:`variable <variable>` ``x``) with ``x == 3`` (a
    :doc:`comparison <compare>` expression which has a value of either
-   ``true`` or ``false`` depending on whether ``x`` is equal to ``3`` or
+   ``T`` or ``F`` depending on whether ``x`` is equal to ``3`` or
    not).  See :doc:`def-vs-test`.

docs/reference/list.rst

@@ -0,0 +1,88 @@
+Lists
+=====
+
+For any :doc:`type <types>` ``T``,  ``List(T)`` is the type of *finite lists* with
+elements of type ``T``.  A list is an arbitrary *sequence*; that is, a
+list is a collection of ``T`` values where the order matters.
+
+In general, lists are written with square brackets.
+
+* The empty list is written ``[]``.
+* A list with specific elements can be written like this: ``[1, 2, 3]``.
+* An :doc:`ellipsis <ellipsis>` can be used to generate a range of
+  elements.  For example,
+
+    ::
+
+       Disco> [1 .. 5]
+       [1, 2, 3, 4, 5]
+       Disco> [1, 3 .. 9]
+       [1, 3, 5, 7, 9]
+
+* :doc:`List comprehension <comprehension>` notation can also be used,
+  for example:
+
+    ::
+
+       Disco> [ abs(x - 5) | x in [1 .. 10], x^2 > 5]
+       [2, 1, 0, 1, 2, 3, 4, 5]
+
+* The built-in ``list`` function can be used to convert other
+  collections (*e.g.* :doc:`sets <set>` or :doc:`bags <bag>`) to lists:
+
+    ::
+
+       Disco> list({1, 2, 3})
+       [1, 2, 3]
+       Disco> import num
+       Disco> list(factor(12))
+       [2, 2, 3]
+
+* The built-in `append` function can be used to append two lists.
+
+    ::
+
+       Disco> import list
+       Disco> :type append
+       append : List(a) × List(a) → List(a)
+       Disco> append([1,2,3], [5,6])
+       [1, 2, 3, 5, 6]
+
+* Strings (written in double quotes) are really just lists of characters.
+
+    ::
+
+       Disco> |"hello"|
+       5
+       Disco> append("hello", "world")
+       "helloworld"
+       Disco> [(c,1) | c in "hello"]
+       [('h', 1), ('e', 1), ('l', 1), ('l', 1), ('o', 1)]
+
+* The order of elements in a list matters.  Two lists with elements in a
+  different order, or different number of copies of the elements, are
+  not the same.  For example,
+
+    ::
+
+       Disco> [1,2,3] == [1,3,2]
+       F
+       Disco> [1,2,3] == [1,1,2,3]
+       F
+
+* To check whether a list contains a given element, one can use the
+  ``elem`` operator (also written ``∈``):
+
+    ::
+
+       Disco> 2 elem [1,2,3]
+       T
+       Disco> 5 elem [1,2,3]
+       F
+       Disco> 2 ∈ [1,2,3]
+       T
+
+Inductive definition of lists
+-----------------------------
+
+Write more here.

docs/reference/logic-ops.rst

@@ -4,8 +4,8 @@ Logical operations
 Disco has various standard operations for manipulating :doc:`Boolean
 values <bool>`.
 
-* Logical negation is written ``not``; it inverts ``true`` to
-  ``false`` and vice versa.
+* Logical negation is written ``not``; it inverts ``T`` to
+  ``F`` and vice versa.
 * Logical conjunction, aka AND, is written ``/\``, ``and``, or
   ``&&``.  It has the following truth table:
 

docs/reference/prop.rst

@@ -4,12 +4,12 @@ Propositions
 ``Prop`` is the type of *propositions*.  A proposition is a statement
 that could be true or false.  ``Prop`` is very similar to ``Bool``;
 the main difference is that whereas any ``Bool`` can always be
-evaluated to see if it is ``true`` or ``false``, this may not be
+evaluated to see if it is ``T`` or ``F``, this may not be
 possible for a ``Prop`` due to the use of quantifiers (``forall`` and
 ``exists``).
 
 Any :doc:`Boolean <bool>` expression can be used as a proposition.
-For example, ``true``, ``x > 5``, and ``(x < y) -> ((x == 2) \/ (x ==
+For example, ``T``, ``x > 5``, and ``(x < y) -> ((x == 2) \/ (x ==
 3))`` can all be used as propositions.
 
 However, unlike Boolean expressions, propositions can use :doc:`quantifiers
@@ -23,12 +23,12 @@ whether a proposition is true or false, you have two options:
 - The built-in ``holds`` function tries its best to determine whether
   a proposition is true or false.  If it returns a value at all, it is
   definitely correct.  For example,
-    - ``holds ((5 < 3) \/ ((2 < 1) -> false))`` yields ``true``
+    - ``holds ((5 < 3) \/ ((2 < 1) -> F))`` yields ``T``
     - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p))``
-      yields ``true``
+      yields ``T``
     - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q))``
-      yields ``false``
-    - ``holds (forall n:N. n < 529)`` yields ``false``
+      yields ``F``
+    - ``holds (forall n:N. n < 529)`` yields ``F``
   However, sometimes it may simply get stuck in an infinite loop.  For
   example, ``holds (forall n:N. n >= 0)`` will simply get stuck. Even
   though it is obvious to us that this proposition is true, ``holds``
@@ -38,7 +38,7 @@ whether a proposition is true or false, you have two options:
 - One can also use the ``:test`` command.  This command makes a best
   effort to evaluate a proposition, but only trying a finite number of
   examples for infinite domains.  Additionally, in many cases it can
-  output much more information than a simple ``true`` or ``false``,
+  output much more information than a simple ``T`` or ``F``,
   for example, showing a counterexample if a ``forall`` is false, or a
   witness if an ``exists`` is true.  For example,
     - ``:test forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q)``
@@ -48,8 +48,8 @@ whether a proposition is true or false, you have two options:
 
              - Certainly false: ∀p. ∀q. p \/ q <-> p /\ q
                Counterexample:
-                 p = false
-                 q = true
+                 p = F
+                 q = T
 
     - However, ``:test forall n:N. n < 529`` prints
 

docs/reference/set-ops.rst

@@ -34,9 +34,9 @@ You can check whether one set is a subset of another using the
 ::
 
    Disco> {2,3,4} subset {1 .. 10}
-   true
+   T
    Disco> {7 .. 11} subset {1 .. 10}
-   false
+   F
 
 Note that Disco does not support the set complement operation, since
 the complement of a finite set is infinite whenever the domain is

docs/reference/set.rst

@@ -49,11 +49,11 @@ To check whether a set contains a given element, one can use the
 ::
 
    Disco> 2 elem {1,2,3}
-   true
+   T
    Disco> 5 elem {1,2,3}
-   false
+   F
    Disco> 2 ∈ {1,2,3}
-   true
+   T
 
 Sets support various operations, including :doc:`size <size>`,
 :doc:`union <set-ops>`, :doc:`intersection <set-ops>`,

docs/reference/sum-type.rst

@@ -18,8 +18,8 @@ Sum types
 
        Disco> left(3) : N + Bool
        left(3)
-       Disco> right(false) : N + Bool
-       right(false)
+       Disco> right(F) : N + Bool
+       right(F)
 
 Note that the ``left`` or ``right`` ensures that ``A + B`` really does
 represent a *disjoint* union.  For example, although the usual