[Agda] Strictly positive types

[Andrés Sicard-Ramírez]

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

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