<div dir="ltr">Hi,<div><br></div><div>Welcome to Agda!</div><div><br></div><div>I think you need to get a more recent version of Agda though, since the support for universe levels changed a bit in the recent releases.</div>
<div><br></div><div>The {-# OPTIONS --universe-polymorphism #-} pragma would appear at the top of your file, before the module header, but that flag is now the default behavior so you won&#39;t need it once you upgrade, and it is indeed the same feature as the Levels approach.</div>
<div><br></div><div>Also in the past you were supposed to define Level as an inductive type with lzero and lsucc as constructors (so just peano naturals) and then implement _⊔_ by recursion, but now we use postulates like in the code you pasted to keep it an abstract type.</div>
<div><br></div><div>Cheers,</div><div>Andrea</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Feb 6, 2014 at 5:38 PM, F.Lockwood Morris <span dir="ltr">&lt;<a href="mailto:flmorris@syr.edu" target="_blank">flmorris@syr.edu</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">




<div dir="ltr">
<div name="divtagdefaultwrapper" style="font-size:12pt;margin:0;font-family:Calibri,Arial,Helvetica,sans-serif">
Hello all,<br>
<br>
I am a complete Agda newbie (but longtime HOL user), trying to learn from<br>
the Agda Wiki, without any direct human instruction. After getting some<br>
little way with &quot;Dependent Types at Work&quot; I had switched to Jan<br>
Malakhovski&#39;s &quot;Brutal (Meta-)Introduction&quot;, which I treasure for its<br>
clear explanation of such matters as how to use goals. I was getting on<br>
fine until reaching the end of his &quot;throwaway&quot; stuff and starting to try<br>
to carry out his library development. I made a file called lib.agda<br>
which, in its entirety, was<br>
<br>
&lt;&lt; copy of file follows: &gt;&gt;<br>
<br>
module lib where<br>
 module Level where<br>
  -- Universe levels<br>
  postulate Level : Set<br>
  postulate lzero : Level<br>
  postulate lsucc : Level → Level<br>
  -- input for ⊔ is \sqcup<br>
  postulate _⊔_   : Level → Level → Level<br>
<br>
  infixl 5 _⊔_<br>
<br>
  -- Make them work<br>
  {-# BUILTIN LEVEL     Level #-}<br>
  {-# BUILTIN LEVELZERO lzero #-}<br>
  {-# BUILTIN LEVELSUC  lsucc #-}<br>
  {-# BUILTIN LEVELMAX  _⊔_   #-}<br>
<br>
&lt;&lt; end of copied file &gt;&gt;<br>
<br>
(right arrows and square cups in appropriate places, in case they are not<br>
showing up)<br>
<br>
but on loading received the error message &quot;Level is not an inductive type&quot;,<br>
which doesn&#39;t mean much to me. Can anyone explain to me what the trouble<br>
is here, and how to get around it?<br>
<div><br>
(Possibly related: at some points in my struggles, I have been hit with a<br>
message &quot;use --universe-polymorphism&quot;, which I think calls for the pragma<br>
<br>
{-# OPTIONS --universe-polymorphism #-}<br>
<br>
to appear somewhere. But where? (Not to mention why?) And is this<br>
something I need additional to the Malakhovskian Levels approach, or an<br>
alternative to it?)<br>
<br>
Many thanks to anyone who can get me started in the right direction.<br>
<br>
Lockwood<br>
<br>
<br>
<div><font><span style="font-size:10pt">
<div>|-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-<br>
Lockwood Morris  <a href="mailto:flmorris@syr.edu" target="_blank">flmorris@syr.edu</a>  <a href="tel:%28315%29443-3046" value="+13154433046" target="_blank">(315)443-3046</a>  Rm. 4-125 CST<br>
EECS  Syracuse University   111 College Place   Syracuse NY 13244-4100</div>
</span></font></div>
</div>
</div>
</div>

<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>