doc: FAQ is separate now

doc/faq.rst

+.. _faq:
+
+Frequently Asked Questions
+==========================
+
+If you have a question, we suggest you post it at http://stackoverflow.com
+(ty `searching for the leon tag <http://stackoverflow.com/questions/tagged/leon?sort=newest>`_)
+or contact one of the authors of this documentation.
+
+Below we collect answers to some questions that came up.
+
+Proving properties of size
+^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+I have defined a size function on my algebraic data type.
+
+.. code-block:: scala
+
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+  def size(l: List) : Int = (l match {
+    case Nil => 0
+    case Cons(_, t) => 1 + size(t)
+  }) ensuring(_ >= 0)
+
+Leon neither proves nor gives a counterexample. Why?
+
+**Answer:** You should consider using `BigInt`, which
+denotes unbounded mathematical integers, instead of `Int`,
+which denotes 32-bit integers. If you replace `Int` with
+`BigInt` in the result type of `size`, the function should
+verify. Note that algebraic data types can be arbitrarily
+large, so, if the input list had the size `Int.MaxValue + 1`
+(which is 2^32) then the addition `1 + size(t)` would wrap
+around and produce `Int.MinValue` (that is, -2^31), so the
+`ensuring` clause would not hold.
+

doc/gettingstarted.rst

@@ -96,11 +96,3 @@ be used directly from the shell, see
 :ref:`installation`.  In addition to invoking `./leon --help` you
 may wish to consult :ref:`cmdlineoptions`.
 
-
-Asking Questions
-----------------
-
-We are active on http://stackoverflow.com. 
-
-Try `searching for the leon tag <http://stackoverflow.com/questions/tagged/leon?sort=newest>`_.
-

doc/index.rst

@@ -15,6 +15,7 @@ Contents:
    gettingstarted
    installation
    tutorial
+   faq
    purescala
    library
    xlang

doc/tutorial.rst

@@ -217,15 +217,16 @@ definition, expressed using Scala's **case classes**.
   case object Nil extends List
   case class Cons(head: BigInt, tail: List) extends List
 
-We can read the definition as follows: List is defined
-by applying the following two rules finitely many times:
+We can read the definition as follows: the set of lists is
+defined as the least set that satisfies them:
 
   * empty list `Nil` is a list
   * if `head` is an integer and `tail` is a `List`, then
     `Cons(head,tail)` is a `List`.
 
-A list containing elements 5, 2, and 7, in that order, can
-be written as
+Each list is constructed by applying the above two rules
+finitely many times.  A concrete list containing elements 5,
+2, and 7, in that order, is denoted
 
 .. code-block:: scala