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.<div><br></div><div>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.</div>
<div><br></div><div>The main thing I can think of in the Agda standard library is the eq? function (<a href="http://www.cse.chalmers.se/~nad/listings/lib/Data.Fin.Props.html#4847" target="_blank">http://www.cse.chalmers.se/~nad/listings/lib/Data.Fin.Props.html#4847</a>), which gives you a decision procedure for equality of your type, if you have an injection into Fin.</div>
<div><br></div><div>- dan<br><br><div class="gmail_quote">On Thu, Nov 10, 2011 at 10:59 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:rk436@cam.ac.uk" target="_blank">rk436@cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is there an Agda library defining a type of finite set-like<br>
collections of elements of any type?<br>
<br>
Fin seems to be just for sets of numbers. What about sets of another<br>
type (or even a newly defined type)?<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>