The Coq mailing list

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

 Hi,

 I have read the description of the positivity conditions required
 for an indutive definition, but I can't understand why in Coq the next
 definition is valid:

  Inductive t : Type := k : (List t) -> t.

 where List is defined as usual as

  Inductive List [T:Type] : Type :=
     nil : (List T)
   | cons : T -> (List T) -> (List T).

 Accordingly to the manual, t should appear only strictly positively in
 (List t), but it doesn't.

 Is Coq's implementation different from the theory or have I missed something?

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