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 n can also be seen as the datatype version of
Next: finite set elimination | Prev: natural numbers | Up: contents