Switch to HTML only

4 files changed, 32 insertions, 59 deletions

diff --git a/doc/Makefile b/doc/Makefile
index f180bbf..ac7e6e3 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -1,13 +1,13 @@
-all: Tutorial.md
+all: Tutorial.html
 
-.PHONY: all ttms
+.PHONY:
 
 ttms:
 	pack build setoid-doc.ipkg
 
-%.md: .PHONY
-	pack run katla markdown --config ./setoid-doc-style.dhall sources/$*.md ./build/ttc/$*.ttm > $*.md
-	pandoc $*.md -o $*.html
+%.html: .PHONY
+	pack run katla markdown --config ./setoid-doc-style.dhall sources/$*.md ./build/ttc/$*.ttm \
+  | pandoc -o $*.html
 
 install-deps:
 	pack install-deps setoid-doc.ipkg
diff --git a/doc/Tutorial.html b/doc/Tutorial.html
index 5aacc5f..ae77959 100644
--- a/doc/Tutorial.html
+++ b/doc/Tutorial.html
@@ -34,6 +34,15 @@
   background-color: whitesmoke;
 }
 </style>
-<h1 id="tutorial-setoids">Tutorial: setoids</h1>
-<p>A <em>setoid</em> is a type equipped with an equivalence relation</p>
-<p><code class="IdrisCode"> <span class="IdrisFunction">Example1</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Nat</span><br /> <span class="IdrisFunction">Example1</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">0</span><br /> </code></p>
+<h1 id="tutorial-setoids">Tutorial: Setoids</h1>
+<p>A <em>setoid</em> 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:</p>
+<ol type="1">
+<li>Know the user interface to the <code>setoid</code> package.</li>
+<li>Know two different applications in which it can be used:</li>
+</ol>
+<ul>
+<li><p>constructing types with an equality relation that’s better behaved than Idris’s built-in <code>Equal</code> type.</p></li>
+<li><p>types with an equality relation that carries additional information</p></li>
+</ul>
+<h2 id="basic-interface">Basic interface</h2>
+<p><code class="IdrisCode"> <br /> </code></p>
diff --git a/doc/Tutorial.md b/doc/Tutorial.md
deleted file mode 100644
index 8d9d9ff..0000000
--- a/doc/Tutorial.md
+++ /dev/null
@@ -1,46 +0,0 @@
-<style>
-.IdrisData {
-  color: darkred
-}
-.IdrisType {
-  color: blue
-}
-.IdrisBound {
-  color: black
-}
-.IdrisFunction {
-  color: darkgreen
-}
-.IdrisKeyword {
-  font-weight: bold;
-}
-.IdrisComment {
-  color: #b22222
-}
-.IdrisNamespace {
-  font-style: italic;
-  color: black
-}
-.IdrisPostulate {
-  font-weight: bold;
-  color: red
-}
-.IdrisModule {
-  font-style: italic;
-  color: black
-}
-.IdrisCode {
-  display: block;
-  background-color: whitesmoke;
-}
-</style>
-# Tutorial: setoids
-A _setoid_ is a type equipped with an equivalence relation
-
-
-
-<code class="IdrisCode">
-<span class="IdrisFunction">Example1</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Nat</span><br />
-<span class="IdrisFunction">Example1</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">0</span><br />
-</code>
-
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
+
 ```