<div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote">On Thu, Nov 21, 2013 at 5:51 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda developers,<br>
I have the following problems.<br><br>
&gt; agda -V<br>
<br>
prints    Agda version 2.3.3<br>
<br>
But it cannot type-check anything:<br>
<br>
  module DPrelude<br>
  where<br>
  open import Level using (Level; suc; _⊔_)<br></blockquote><div><br></div><div>The syntax has changed slightly from version 2.3.2. You need to indent the</div><div>&quot;where&quot; or put it on the same line as &quot;module&quot;.</div>

<div><br></div><div>/ Ulf </div></div></div></div>