From bc260cdfa7b309820594b7caf14f62be8343358e Mon Sep 17 00:00:00 2001
From: Ohad Kammar <ohad.kammar@ed.ac.uk>
Date: Sun, 7 Aug 2022 19:08:32 +0100
Subject: Switch to HTML only

---
 doc/Tutorial.html | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

(limited to 'doc/Tutorial.html')

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>
-- 
cgit v1.2.3