[Agda] collections/containers/finite sets

[Daniel Peebles]

Fin n is a set that has n inhabitants, and it also happens to also look
like a natural number. Nothing says you have to treat it as one, though.

For a more general statements about finiteness, you probably want to say
there's an injection from your type to Fin n, for some n. Or you could
provide a complete enumeration of your type's elements in a list or a
vector and prove that all elements of your type are present in it (this is
roughly the injection into Fin n, in disguise). I've written some Agda code
encoding statements about finiteness, but it's nothing I'd call a library
at this point.

The main thing I can think of in the Agda standard library is the eq?
function (
http://www.cse.chalmers.se/~nad/listings/lib/Data.Fin.Props.html#4847),
which gives you a decision procedure for equality of your type, if you have
an injection into Fin.

- dan

On Thu, Nov 10, 2011 at 10:59 AM, Ramana Kumar <rk436 at cam.ac.uk> wrote:

> Is there an Agda library defining a type of finite set-like
> collections of elements of any type?
>
> Fin seems to be just for sets of numbers. What about sets of another
> type (or even a newly defined type)?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111110/379106b0/attachment.html