blob: f143d459055f4b298bf473320284837e93719480 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
```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
```
|
