<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'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"><<a href="mailto:flmorris@syr.edu" target="_blank">flmorris@syr.edu</a>></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 "Dependent Types at Work" I had switched to Jan<br>
Malakhovski's "Brutal (Meta-)Introduction", 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 "throwaway" 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>
<< copy of file follows: >><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>
<< end of copied file >><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 "Level is not an inductive type",<br>
which doesn'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 "use --universe-polymorphism", 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>