blob: ae77959937493f5a3bf81983f8219d5f2967448d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
<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>
<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>
|
