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&#39;s an injection from your type to Fin n, for some n. Or you could provide a complete enumeration of your type&#39;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&#39;ve written some Agda code encoding statements about finiteness, but it&#39;s nothing I&#39;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">&lt;<a href="mailto:rk436@cam.ac.uk" target="_blank">rk436@cam.ac.uk</a>&gt;</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>