blob: 20678f2e6a76efafad0df6bee28296c4dbc56921 (
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
|
<style>
.IdrisData {
color: darkred
}
.IdrisType {
color: blue
}
.IdrisBound {
color: black
}
.IdrisFunction {
color: darkgreen
}
.IdrisKeyword {
text-decoration: underline;
}
.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">F</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Nat</span><br />
<span class="IdrisFunction">F</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">0</span><br />
</code>
|
