The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

On Tue, Aug 02, 2011 at 11:04:43PM -0700, S3 wrote:
> 
> To illustrate that it enforces the constraint:
> Inductive constant3 (a: nat): list nat -> Prop :=
> | Cnil3: constant3 a nil
> | Ccons3: forall l, constant3 a l -> constant3 (S a) (a::l).
> 
> Error: Last occurrence of "constant3" must have "a" as 1st argument in
>  "forall l : list nat, constant3 a l -> constant3 (S a) (a :: l)".

The parameter a should be used as is in all conclusions of
you constructors. I.e. you can write:

Inductive constant3 (a: nat): list nat -> Prop :=
| Cnil3: constant3 a nil
| Ccons3: forall l, constant3 (S a) l -> constant3 a (a::l).

But you probably want the following one:

Inductive constant3: nat -> list nat -> Prop :=
| Cnil3: forall a, constant3 a nil
| Ccons3: forall a l, constant3 a l -> constant3 (S a) (a::l).


Hope this helps
Jean-Francois