[Agda] Bug in the strictly positivity check

[Florent]

This is from the command line

$ agda --version
Agda version 2.2.7

$ agda NSP.agda
Checking NSP (/home/florent/work/agda/NSP.agda).

No error. What's going on with my version?
-- Florent


Thorsten Altenkirch wrote:
> Which version of Agda are you using?
>
> /Users/txa/current/NP.agda:5,8-11
> NSP is not strictly positive, because it occurs to the left of an
> arrow in the definition of NSP.
>
> Check you *ghci* buffer. Mine says
> 	Prelude> :set -package Agda-2.2.7
>
> Cheers,
> Thorsten
>
> On 29 Sep 2010, at 13:23, Florent Balestrieri wrote:
>
>   
>> record NSP : Set where
>>  field
>>    nsp : (NSP -> Top) -> Top
>>     
>
>
>   

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