[Agda] collections/containers/finite sets

Andreas Abel andreas.abel at ifi.lmu.de
Thu Nov 10 23:22:33 CET 2011


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.

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/


More information about the Agda mailing list