The Coq mailing list

[Hugo Herbelin <herbelin AT margaux.inria.fr>]

>  Thank you for the answer, but I still don't understand it.
> 
> > The constant X _occurs strictly positively_ in T in the
> > following cases:
> > 
> > -- T=(X t1 ... tn) and X does not occur in any of ti
> > -- T=(I a1 ... am t1 ... tn) where I is an inductive type not mutually
> > defined with m parameters and arity of length n, and X does not occur
> > in any of the ti but each constructor of I satisfies the weak
> > positivity condition after substituting the parameters by a_1 ...  a_n
> 
>  What does "each constructor of I satifies the weak positivity condition
>  after substituting the parameters by a_1 ... a_n" mean?

  It means, if I has constructors ci:(x1:T1;...;xm:Tm)Ui, that X must
occur weakly positively in each Ui where the x1...xm are replaced by
the a1...am.
 
>  Which name should respect the weak positivity condition in
>  the types of the constructors of I? If it is I (as we understand) then we
>  could not find an example in which the condition could be false. Moreover,
>  this example seem to respect the condition but is not accepted by Coq
>  (reasonable!):
> 
>    Inductive t : Set := k : (list (nat -> t)) -> t.

  In Coq V6.3.1, it _is_ accepted.
 
>  Accordingly to your definition, the weak positivity condition must hold on
> 
>   nil : (list (nat -> t))
>   cons: (nat -> t) -> (list (nat -> t)) -> (list (nat -> t))
> 
>  and we think it does (w.r.t. list).

  Yes it does : t occurs weakly positively in the instantiated types
of nil and cons.
 
                                                  Hugo