From bc260cdfa7b309820594b7caf14f62be8343358e Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Sun, 7 Aug 2022 19:08:32 +0100 Subject: Switch to HTML only --- doc/sources/Tutorial.md | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'doc/sources') 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 + ``` -- cgit v1.2.3