[Agda] Using Data.Sets

[Darin Morrison]

On Nov 24, 2008, at 12:41 PM, J.Burton at brighton.ac.uk wrote:

> Hi, how do I use the Sets library? I want to work with sets of Chars
> and other types, but if I try, e.g., fromList [ 1 ]
>
> (List ℕ) !=< .Relation.Binary.DecTotalOrder
> when checking that the expression [ 1 ] has type
> .Relation.Binary.DecTotalOrder
>
> So do I need to define the order before I can make a <Set> of a
> datatype? I got lost looking for the definition of DecTotalOrder...
> If this isn't the way this module is intended to be used I suppose I
> should cook my own following the example of examples/simple-lib/Lib/Eq
> for polymorphism & equality...?

Here's another short example :)

module Sets where

open import Data.List
open import Data.Nat
open import Data.Sets

open module NatSet = Sets₁ decTotalOrder

exampleSet : NatSet.<Set>
exampleSet = NatSet.fromList [ 1 ]

So yes, you need to either define a decidable total order of your own  
or use an existing one.  In the above code, I just use the  
decTotalOrder from Data.Nat and I create a new concrete module NatSet  
by applying the inner module Data.Sets.Set₁ to decTotalOrder.

Hope that helps.

Regards,
Darin