The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 12 Mar 2007, mulhern wrote:

> Secretly, my inductive constructor actually is like this:
>
> Inductive mytype : Set :=
> | Ground : mytype
> | Cons : {x : list mytype | length (A := mytype) x = bound} -> mytype
> .
>
> And it's that implicit occurence of mytype that is causing all the trouble.

I had exactly the same problem.  See the ``Defintion of Term'' section in 
my paper at <http://r6.ca/Goedel/goedel1.html#FOCL>.  I end up useing 
mutually inductive types, but later I learn that one can use Vectors and 
define your own elimination scheme using nested fixed point.  By using 
Vectors you can reuse the existing Vector library.

Many people complain that using Vectors is difficult.  It is true if you 
are doing things like concatinating lists.  For my purposes they worked 
fine because I never have to do these sorts of operations.  All I do is 
make sure that the correct number of arguments to functions of a given 
arity.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''