[Agda] Error defining Universe Polymorphism

[Ashish Mishra]

Hi All,

I am new to Agda and am giving some tries to various available tutorials
for Agda. I am facing a pertinent issue while defining new LEVELS of
Universes using the BUILTIN pragmas of Agda .

To illustrate  -The following code from the library by Ulf Norell for the
OPLSS -

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

*module Lib.Level where*

*module LEVEL where*

*  data Level : Set where*
*    Z : Level*
*    S : Level -> Level*

*  max : Level -> Level -> Level*
*  max  Z     m     = m*
*  max (S n)  Z     = S n*
*  max (S n) (S m)  = S (max n m)*

*  {-# BUILTIN LEVEL     Level #-}*
*  {-# BUILTIN LEVELZERO Z  #-}*
*  {-# BUILTIN LEVELSUC  S   #-}*
*  {-# BUILTIN LEVELMAX max #-}*

*  record Lift {a b} (A : Set a) : Set (max a b) where*
*    constructor lift*
*    field lower : A*

*  open Lift public*

*open LEVEL public *
*  using (Z ; S ; lift ; lower ; Level) *


Throws errors -
1) The argument to BUILTIN LEVEL must be a postulated name
when checking the pragma BUILTIN LEVEL Level

2)Builtin LEVELZERO must be bound to a function
when checking the pragma BUILTIN LEVELZERO Z

Can some body explain me the issue here ... I have tried commenting the
pragmas but in some cases ( different example from the "Brutal agda" ) the
error vanishes and the universes work fine ... Sorry but not sure whats
happening here.

Thanks





-- 
Regards,
Ashish Mishra
Graduate Student,
Computer Science and Automation Department,IISc
Cell : +91-9611194714
Mailto : ashishmishra at csa.iisc.ernet.in
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151009/289f96a0/attachment-0001.html