From 62c3d20065f2b345928fc75a17fdf1f9328fb87c Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Thu, 23 Apr 2015 16:03:40 +0200
Subject: [PATCH] Mostly started to talk about a tutorial
---
doc/index.rst | 1 +
doc/library.rst | 20 ++++++++++++++++++++
doc/purescala.rst | 4 ++--
doc/tutorial.rst | 32 ++++++++++++++++++++++++++++----
4 files changed, 51 insertions(+), 6 deletions(-)
create mode 100644 doc/library.rst
diff --git a/doc/index.rst b/doc/index.rst
index 2862cb2a4..34b763386 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -16,6 +16,7 @@ Contents:
tutorial
installation
purescala
+ library
xlang
verification
synthesis
diff --git a/doc/library.rst b/doc/library.rst
new file mode 100644
index 000000000..b49c3881b
--- /dev/null
+++ b/doc/library.rst
@@ -0,0 +1,20 @@
+.. _library:
+
+Leon Library
+============
+
+Leon defines its own versions of most data structures. One of the reasons is to ensure that these operations can be correctly mapped to mathematical functions and relations inside of SMT solvers, largely defined by the SMT-LIB standard (see http://www.smt-lib.org/).
+
+List
+^^^^
+
+Set
+^^^
+
+Option
+^^^^^^
+
+Map
+^^^
+
+
diff --git a/doc/purescala.rst b/doc/purescala.rst
index 2402c730f..3c10fd4bf 100644
--- a/doc/purescala.rst
+++ b/doc/purescala.rst
@@ -1,7 +1,7 @@
.. _purescala:
-Pure Scala
-=============================
+Pure Scala: Leon's Core Input Language
+======================================
Leon supports two kinds of top-level declarations:
diff --git a/doc/tutorial.rst b/doc/tutorial.rst
index 8a84a5db5..90ff3d572 100644
--- a/doc/tutorial.rst
+++ b/doc/tutorial.rst
@@ -1,7 +1,31 @@
.. _tutorial:
-Tutorial
-========
+Tutorials
+=========
+
+Sorting Lists
+-------------
+
+This tutorial shows how to define lists as algebraic data
+types, how to **verify** certain properties of an insertion
+sort, as well as how to use Leon to **synthesize**
+operations from specifications.
+
+Defining lists
+^^^^^^^^^^^^^^
+
+Leon has a built-in data type of polymorphic lists (see
+
+Let us start by specifying a function that sorts **two**
+mathematical integers.
+
+.. code-block:: scala
+
+ import leon.lang._
+ import leon.lang.synthesis._
+ object Sort {
+ def sort2(x : BigInt, y : BigInt) = choose{(res: (BigInt,BigInt)) =>
+ Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
+ }
+ }
-In this section, we will go through an extended tutorial to demonstrate basic
-usage of Leon.
--
GitLab