The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT students.cs.unibo.it>]

 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?

 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.

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

> -- T=(x:U)V and X does not occur in U but may occur strictly
> positively in V.
> 
> The constant X _satisfies the weak positivity condition_ in t either
> when t=[x:T]u and X occurs strictly positively in T and satisfies the
> weak positivity condition in u, or when X satisfies the positivity
> condition (defined as before) in t.

                                                Thank you in advance,
                                                        C.S.C.

-- 
-----------------------------------------
Real Name: Claudio Sacerdoti Coen
Address: via del Colle n.6
         S. Lazzaro di Savena (BO)
         Italy
e-mail:  
sacerdot AT cs.unibo.it
-----------------------------------------