[Agda] collections/containers/finite sets

[Ramana Kumar]

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)

On Thu, Nov 10, 2011 at 10:31 PM, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> On Thu, Nov 10, 2011 at 10:22 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>> On 10.11.11 4:59 PM, Ramana Kumar wrote:
>>>
>>> Is there an Agda library defining a type of finite set-like
>>> collections of elements of any type?
>>
>> If you are not worried about complexity, you can use
>>
>>  List A
>>
>> as finite collection of elements of type A.  Otherwise, if you want an
>> efficient implementation, you can have a look the the AVL trees of the
>> standard library or Julien Oster's red-black trees.
>
> Ah I didn't realize that AVL trees were in the standard library,
> because they're not linked to from the README (I found them just now
> by first clicking "Everything" from the README, then scanning down for
> AVL). Thanks.
>
> AVL trees will probably suit me, but I'm curious whether it makes
> sense to write some Agda code to just the interface for finite sets
> without specifying exactly how they're implemented. Is that possible?
> I think in Coq you could achieve that (with MSets) by writing your
> code as the body of a functor parameterised by something matching the
> MSetsInterface.
>
>>
>> https://bitbucket.org/anyfoo/agda-std-trees/src
>>
>> Cheers,
>> Andreas
>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>>
>> andreas.abel at ifi.lmu.de
>> http://www2.tcs.ifi.lmu.de/~abel/
>>
>