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


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

for the inductive definition of < as `strict subterm ordering'.


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


Conor's Work Page