[Agda] collections/containers/finite sets

[Nils Anders Danielsson]

On 2011-11-11 11:49, Ramana Kumar wrote:
> Are there any example files available on how to use Data.AVL.Sets?
> I'm getting this kind of error
> Set !=<
> (.Relation.Binary.IsStrictTotalOrder
>   .Relation.Binary.Core.Dummy._≡_ _79)
> of type Set₁
> when checking that the expression Formula has type
> .Relation.Binary.IsStrictTotalOrder .Relation.Binary.Core.Dummy._≡_
> _79
> which presumably means I need to show I have a strict total order on
> the type of elements of the sets.
> I don't know how to do that concretely in Agda... (theoretically it
> should be easy for my type though)

I just added some examples showing how the AVL tree module can be used:

   http://www.cse.chalmers.se/~nad/listings/lib/README.AVL.html

Note that these examples use the current development version of the
library, in which the AVL tree interface has changed.

-- 
/NAD