From 301ea49797a57dc9e433f205628a814f60e8c705 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Fri, 24 Apr 2015 21:54:16 +0200
Subject: [PATCH] doc: small crosscutting changes while tutoring sort
---
doc/options.rst | 4 ++--
doc/purescala.rst | 13 +++++++------
doc/tutorial.rst | 29 ++++++++++++++++++-----------
3 files changed, 27 insertions(+), 19 deletions(-)
diff --git a/doc/options.rst b/doc/options.rst
index b4462aa13..82f52a7ff 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -1,7 +1,7 @@
.. _cmdlineoptions:
-Command Line Options
-====================
+Command Line
+============
Here is an overview of the command-line options that Leon recognizes:
diff --git a/doc/purescala.rst b/doc/purescala.rst
index b8236f09e..7c9f7e6ce 100644
--- a/doc/purescala.rst
+++ b/doc/purescala.rst
@@ -3,12 +3,13 @@
Pure Scala
==========
-The input to Leon is a purely functional subset of Scala,
-which we call **Pure Scala**. Constructs specific for Leon
-are defined inside Leon's libraries in package `leon` and
-its subpackages. Leon invokes standard `scalac` compiler on
-the input file, then performs additional checks to ensure
-that the given program belongs to Pure Scala.
+The input to Leon is a purely functional **subset** of Scala
+(http://www.scala-lang.org/), which we call
+**Pure Scala**. Constructs specific for Leon are defined inside
+Leon's libraries in package `leon` and its subpackages. Leon
+invokes standard `scalac` compiler on the input file, then
+performs additional checks to ensure that the given program
+belongs to Pure Scala.
Pure Scala supports two kinds of top-level declarations:
diff --git a/doc/tutorial.rst b/doc/tutorial.rst
index f4dce6b95..0e83c638a 100644
--- a/doc/tutorial.rst
+++ b/doc/tutorial.rst
@@ -92,8 +92,8 @@ parameters, such as
def test1 = sort2(30, 4)
-Hovering over the definition of test1 should display
-the computed tuple `(4,30)`.
+Hovering over `test1` should display the computed result
+`(4,30)`. From :ref:`cmdlineoptions`, use `--eval`.
This shows that Leon's evaluator can also execute `choose`
constructs. In other words, it supports programming
@@ -136,16 +136,23 @@ Depending on the particular run, Leon may also produce a solution such as
This code performs some unnecessary case analysis, but still
satisfies our specification. In this case, the specification
-is unambiguous, so all programs that one can synthesize
-compute the same results for all inputs.
+of the program output is unambiguous, so all programs that
+one can synthesize compute the same results for all inputs.
-Defining Unbounded Lists
-------------------------
+Defining Lists and Their Properties
+-----------------------------------
-Let us now consider sorting of any number of elements.
+We next consider sorting an unbounded number of elements.
-For this purpose, we define the data structure of lists of
-(big) integers. Leon has a built-in data type of
-polymorphic lists, see :ref:`Leon Library <library>`, but
-here we define our own variant.
+For this purpose, we define a data structure for lists of
+integers. Leon has a built-in data type of parametric
+lists, see :ref:`Leon Library <library>`, but here we define
+our own variant instead. We use a recursive algebraic data type
+definition, expressed using Scala's **case classes**.
+
+.. code-block:: scala
+
+ sealed abstract class List
+ case object Nil extends List
+ case class Cons(head: BigInt, tail: List) extends List
--
GitLab