diff options
Diffstat (limited to 'doc/Tutorial.html')
| -rw-r--r-- | doc/Tutorial.html | 15 |
1 files changed, 12 insertions, 3 deletions
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> |