<br><div class="gmail_quote">On Fri, Sep 25, 2009 at 6:30 PM, Benja Fallenstein <span dir="ltr"><<a href="mailto:benja.fallenstein@gmail.com">benja.fallenstein@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi Ulf,<br>
<div class="im"><br></div><div class="im">
> At present there is no way to lift types from one level to another, that<br>
> is, there is no function<br>
> lift : {i : Level} -> Set i -> Set (suc i)<br>
> This is likely to change at some point.<br>
<br>
</div>Does that mean that doing it manually using levels in data<br>
declarations is not / not yet possible? I.e.,<br>
<br>
data Lift {i : Level} (X : Set i) : (Set (suc i)) where<br>
lift : X -> Lift X<br>
<br>
Or does it just mean there's no built-in support?</blockquote><div><br></div><div>No built-in support. You can define the Lift datatype above.</div><div><br></div><div>/ Ulf</div></div>