<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style style="display: none;" id="owaParaStyle" type="text/css">P {margin-top:0;margin-bottom:0;}</style>
</head>
<body tabindex="0" aria-label="Message body" fpstyle="1" dir="ltr">
<div name="divtagdefaultwrapper" id="divtagdefaultwrapper" style="font-family: Calibri,Arial,Helvetica,sans-serif; font-size: 12pt; color: #000000; margin: 0">
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 class="BodyFragment"><font size="2"><span style="font-size:10pt;">
<div class="PlainText">|- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |-<br>
Lockwood Morris flmorris@syr.edu (315)443-3046 Rm. 4-125 CST<br>
EECS Syracuse University 111 College Place Syracuse NY 13244-4100</div>
</span></font></div>
</div>
</div>
</body>
</html>