**fin** *n* is a type with *n* elements. There are no
elements in **fin 0**. Each time we increment the size, we embed
the old elements with **fs** and chuck in a new one with **fz**.

Note that the **fs** really takes two arguments, *n* and
*i*. I suppress the *n*, since it can easily be inferred.
(See Randy Pollack's work on implicit syntax...)

I use these types to represent the finite collections of free variables over which terms in a syntax may be constructed.

You can also view this type as computed by

**fin 0**=**empty**|**fin s***n*=**unit + fin***n*

**fin** *n* can also be seen as the datatype version of

- exists
*m*.*m***<***n*

Next: finite set elimination | Prev: natural numbers | Up: contents

Conor's Work Page