The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

On Mon, 12 Mar 2007, mulhern wrote:

> 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.

note that, with Cons:list mytype->mytype, coq outputs no error but does not 
generate the good induction principle. this is because coq does not recognize 
list as a monotone type constructor and hence the occurrence of mytype in 
(list mytype) as a positive occurrence. you can however redefine it. see 
http://color.loria.fr/doc/Rewriting.Term.Varyadic.VTerm.html for an example of 
re-definition. http://color.loria.fr/doc/Rewriting.Term.WithArity.ATerm.html 
uses the same trick with vector instead of list. unfortunately, this does not 
seem possible in your case since coq outputs an error. by the way, you may be 
interested in a library on vectors. see 
http://color.loria.fr/doc/Rewriting.Util.Vector.VecUtil.html.