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