diff options
Diffstat (limited to 'doc/sources')
| -rw-r--r-- | doc/sources/Tutorial.md | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md index dc7dc71..f143d45 100644 --- a/doc/sources/Tutorial.md +++ b/doc/sources/Tutorial.md @@ -1,11 +1,21 @@ -# Tutorial: setoids -A _setoid_ is a type equipped with an equivalence relation - ```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 -Example1 : Nat -Example1 = 0 + ``` |