Switch to HTML only

1 files changed, 15 insertions, 5 deletions

diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md
index dc7dc71..f143d45 100644
--- a/doc/sources/Tutorial.md
+++ b/doc/sources/Tutorial.md
@@ -1,11 +1,21 @@
-# Tutorial: setoids
-A _setoid_ is a type equipped with an equivalence relation
-
 ```idris hide
 module Tutorial
 ```
+# Tutorial: Setoids
+
+A _setoid_ is a type equipped with an equivalence relation. Setoids come up when
+you need types with a better behaved equality relation, or when you want the
+equality relation to carry additional information. After completing this
+tutorial you will:
+
+1. Know the user interface to the `setoid` package.
+2. Know two different applications in which it can be used:
+  + constructing types with an equality relation that's better behaved than
+    Idris's built-in `Equal` type.
 
+  + types with an equality relation that carries additional information
+
+## Basic interface
 ```idris
-Example1 : Nat
-Example1 = 0
+
 ```