<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
This is from the command line<br>
<br>
$ agda --version<br>
Agda version 2.2.7<br>
<br>
$ agda NSP.agda <br>
Checking NSP (/home/florent/work/agda/NSP.agda).<br>
<br>
No error. What's going on with my version?<br>
-- Florent<br>
<br>
<br>
Thorsten Altenkirch wrote:
<blockquote
cite="mid:9988F41A-BA26-42DB-947C-035599FE9492@cs.nott.ac.uk"
type="cite">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">record NSP : Set where
field
nsp : (NSP -> Top) -> Top
</pre>
</blockquote>
<pre wrap=""><!---->
</pre>
</blockquote>
<br>
</body>
</html>