The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

 > 
 > Yes, all the elements (proofs) of an inductive type are finite objects.
 > 

This confusing statement has appeared several times in the last few
days.

The elements of an inductive type are well founded.  But such objects
can be infinite in at least two ways:

- They may contain infinite objects at the leaves, i.e. packaged
inside constructors.

- Some constructors may be infinitely branching, e.g. the datatype of
ordinals.

Randy