[Agda] Level not an inductive type

[Andrea Vezzosi]

Hi,

Welcome to Agda!

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.

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.

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.

Cheers,
Andrea


On Thu, Feb 6, 2014 at 5:38 PM, F.Lockwood Morris <flmorris at syr.edu> wrote:

>  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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140206/236e9427/attachment.html