[Agda] Strictly positive types

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Thu Aug 23 22:48:54 CEST 2012

On Wed, Aug 22, 2012 at 9:40 AM, Nils Anders Danielsson <nad at chalmers.se>wrote:

> On 2012-08-21 23:09, Andrés Sicard-Ramírez wrote:
>> Yes, the type _≡_ can also be defined in Coq, but I don't see its
>> relation to the head type constraints (as described in the Coq'Art).
> I don't know what constraints you are referring to.

>From Coq'Art, p. 379:

The type of constructors of an inductive type T has the following form:

t₁ → t₂ → ... t_l → T a₁ ... a_k.

The type T cannot appear among the arguments a₁ ... a_k. For
example, the following definition is rejected

Inductive T : Set → Set := c : T (T nat).
Error: Non strictly positive occurrence of "T" in "T (T nat)"

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120823/d31a93ac/attachment.html

More information about the Agda mailing list