[Agda] Using Data.Sets

[J.Burton at brighton.ac.uk]

At Mon, 24 Nov 2008 13:00:38 -0500,
Darin Morrison wrote:
> 
> 
[snip]
> 
> Here's another short example :)
>

Thanks Darin! 

The first place I looked for this information was the Sets module,
could an example like this go in the comments? Or on the wiki/in the
manual, but I know these are works in progress...you're going to need
them I think -- the Agda community has been doing a good job
publicising itself so you are going to get more like me :-)

Jim
 
> 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
> 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081124/01d5965d/attachment.html