From 7ea0c1c1005d84d961dd7eb27c5b48f554cf39b8 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 20 Dec 2016 22:04:13 +0100
Subject: [PATCH] Create tutorial.md
---
src/doc/tutorial.md | 42 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 42 insertions(+)
create mode 100644 src/doc/tutorial.md
diff --git a/src/doc/tutorial.md b/src/doc/tutorial.md
new file mode 100644
index 000000000..bb629c561
--- /dev/null
+++ b/src/doc/tutorial.md
@@ -0,0 +1,42 @@
+Tutorial
+========
+
+Let us consider the problem of checking whether the following size function on a list is always greater or equal to 0.
+```scala
+def size[T](list: List[T]): BigInt = list match {
+ case Cons(x, xs) => 1 + size(xs)
+ case Nil() => 0
+}
+```
+
+Note that verifying this property requires the use of induction, something Inox does not deal with explicitly.
+However, Inox provides all the tools necessary to enable inductive reasonning, as we will see shortly.
+
+Let us start by setting up some useful imports:
+```scala
+import inox._
+import inox.trees._
+import inox.trees.dsl._
+```
+
+## ADT Definitions
+
+The dsl we just imported provides us with the following helper methods to define ADTs (see
+the [Definitions](/src/doc/API.md#definitions) section in the API documentation for more details):
+
+1. For ADT sort definitions
+```scala
+def mkSort(id: Identifier)
+ (tpNames: String*)
+ (cons: Seq[Identifier]): ADTSort
+```
+
+2. For ADT constructor definitions
+```scala
+def mkConstructor(id: Identifier)
+ (tpNames: String*)
+ (sort: Option[Identifier])
+ (fieldBuilder: Seq[TypeParameter] => Seq[ValDef]): ADTConstructor
+```
+
+We therefore start by
--
GitLab