[Agda] Level not an inductive type

[F.Lockwood Morris]

Hello all,

I am a complete Agda newbie (but longtime HOL user), trying to learn from
the Agda Wiki, without any direct human instruction. After getting some
little way with "Dependent Types at Work" I had switched to Jan
Malakhovski's "Brutal (Meta-)Introduction", which I treasure for its
clear explanation of such matters as how to use goals. I was getting on
fine until reaching the end of his "throwaway" stuff and starting to try
to carry out his library development. I made a file called lib.agda
which, in its entirety, was

<< copy of file follows: >>

module lib where
 module Level where
  -- Universe levels
  postulate Level : Set
  postulate lzero : Level
  postulate lsucc : Level ? Level
  -- input for ? is \sqcup
  postulate _?_   : Level ? Level ? Level

  infixl 5 _?_

  -- Make them work
  {-# BUILTIN LEVEL     Level #-}
  {-# BUILTIN LEVELZERO lzero #-}
  {-# BUILTIN LEVELSUC  lsucc #-}
  {-# BUILTIN LEVELMAX  _?_   #-}

<< end of copied file >>

(right arrows and square cups in appropriate places, in case they are not
showing up)

but on loading received the error message "Level is not an inductive type",
which doesn't mean much to me. Can anyone explain to me what the trouble
is here, and how to get around it?

(Possibly related: at some points in my struggles, I have been hit with a
message "use --universe-polymorphism", which I think calls for the pragma

{-# OPTIONS --universe-polymorphism #-}

to appear somewhere. But where? (Not to mention why?) And is this
something I need additional to the Malakhovskian Levels approach, or an
alternative to it?)

Many thanks to anyone who can get me started in the right direction.

Lockwood


|-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-  |-
Lockwood Morris  flmorris at syr.edu  (315)443-3046  Rm. 4-125 CST
EECS  Syracuse University   111 College Place   Syracuse NY 13244-4100
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140206/5b1decce/attachment.html