<div dir="ltr"><br><div class="gmail_quote"><div dir="ltr">Hi All,<div><br></div><div>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 .</div><div><br></div><div>To illustrate  -The following code from the library by Ulf Norell for the OPLSS -</div><div><br></div><div><div><i><b>{-# OPTIONS --universe-polymorphism #-}</b></i></div><div><i><b><br></b></i></div><div><i><b>module Lib.Level where</b></i></div><div><i><b><br></b></i></div><div><i><b>module LEVEL where</b></i></div><div><i><b><br></b></i></div><div><i><b>  data Level : Set where</b></i></div><div><i><b>    Z : Level</b></i></div><div><i><b>    S : Level -&gt; Level</b></i></div><div><i><b><br></b></i></div><div><i><b>  max : Level -&gt; Level -&gt; Level</b></i></div><div><i><b>  max  Z     m     = m</b></i></div><div><i><b>  max (S n)  Z     = S n</b></i></div><div><i><b>  max (S n) (S m)  = S (max n m)</b></i></div><div><i><b><br></b></i></div><div><i><b>  {-# BUILTIN LEVEL     Level #-}</b></i></div><div><i><b>  {-# BUILTIN LEVELZERO Z  #-}</b></i></div><div><i><b>  {-# BUILTIN LEVELSUC  S   #-}</b></i></div><div><i><b>  {-# BUILTIN LEVELMAX max #-}</b></i></div><div><i><b><br></b></i></div><div><i><b>  record Lift {a b} (A : Set a) : Set (max a b) where</b></i></div><div><i><b>    constructor lift</b></i></div><div><i><b>    field lower : A</b></i></div><div><i><b><br></b></i></div><div><i><b>  open Lift public</b></i></div><div><i><b>  </b></i></div><div><i><b>open LEVEL public </b></i></div><div><i><b>  using (Z ; S ; lift ; lower ; Level) </b></i></div><div><i><b><br></b></i></div></div><div><br></div><div>Throws errors -</div><div>1) The argument to BUILTIN LEVEL must be a postulated name</div><div>when checking the pragma BUILTIN LEVEL Level</div><div><br></div><div>2)Builtin LEVELZERO must be bound to a function</div><div>when checking the pragma BUILTIN LEVELZERO Z</div><div><br></div><div>Can some body explain me the issue here ... I have tried commenting the pragmas but in some cases ( different example from the &quot;Brutal agda&quot; ) the error vanishes and the universes work fine ... Sorry but not sure whats happening here.</div><div><br></div><div>Thanks <span class="HOEnZb"><font color="#888888"><br></font>-- <font color="#888888"><br></font></span></div></div></div><div class="gmail_signature">Regards,<br>Ashish Mishra<br>Graduate Student,<br>Computer Science and Automation Department,IISc<br>Cell : +91-9611194714<br>Mailto : <a href="mailto:ashishmishra@csa.iisc.ernet.in" target="_blank">ashishmishra@csa.iisc.ernet.in</a><br><br></div>
</div>