The Coq mailing list

[Ali Assaf <ali.assaf AT inria.fr>]

The non-parameter arguments can be different for each constructor. They can 
be variables or more complicated terms. In fact notice that the number of 
"a"s is n and it can be different for each constructor, while the number of 
"t"s is q, which *must* be the same for all constructors since r + q must be 
equal to the number of arguments of the inductive type I. As an example, look 
at the definition of polymorphic vectors:

Inductive vector (A : Type) : nat -> Type :=
| vnil : vector A 0
| vcons : forall n, A -> vector A n -> vector A (S n).

There is one inductive parameter which is A and one real argument which is of 
type nat. The constructor vnil has type

  forall (A : Type), vector A 0

while the constructor vcons has type

  forall (A : Type) (n : nat), A -> vector A n -> vector A (S n).

The constructor vcons takes more arguments than vnil. The constructor vnil 
uses 0 as a real argument while vcons uses (S n) (which is not a variable).

Hope this helps!


Ali Assaf

----- Original Message -----
> From: "lars rasmusson" 
> <lars.rasmusson AT sics.se>
> To: 
> coq-club AT inria.fr
> Sent: Friday, November 14, 2014 5:49:54 PM
> Subject: [Coq-Club] About Inductive parameters in the Reference Manual
> 
> On page 120 of the Reference Manual
> https://coq.inria.fr/distrib/V8.4pl3/files/Reference-Manual.pdf
> 
> here (see http://oi61.tinypic.com/11juk41.jpg for a extract from the page)
> it says
> 
>    C == forall p_1...p_r, forall a_1...a_n, (I p1 ... p_r t_1 ... t_q)
> 
> Should it be the following?
> 
>    C == forall p_1...p_r, forall a_1...a_n, (I p1 ... p_r a_1 ... a_n)
> 
> 
> 
> Best regards,
> /Lars
>