<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 -> Level</b></i></div><div><i><b><br></b></i></div><div><i><b> max : Level -> Level -> 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 "Brutal agda" ) the error vanishes and the universes work fine ... Sorry but not sure whats happening here.</div><div><br></div><div>Thanks <br><br></div><div><br></div><div><br></div><div><br clear="all"><div><br></div>-- <br><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></div>