<br><div class="gmail_quote">On Fri, Sep 25, 2009 at 7:33 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cs.nott.ac.uk">nad@cs.nott.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On 2009-09-25 17:17, Ulf Norell wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
or set it in the emacs mode options.<br>
</blockquote>
<br></div>
How?</blockquote><div><br></div><div>Hm, I thought there was some way to give command line arguments in the emacs options, I guess I was wrong. </div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> The type Level is isomorphic to the unary natural numbers and should be<br>
specified using the BUILTINs LEVEL, LEVELZERO, and LEVELSUC:<br>
</blockquote>
<br></div>
Is there any reason not to bind LEVEL to ℕ?</blockquote><div><br></div><div>There are some special rules for checking equality between levels (for instance max i i = i) and I didn't want those interfering with normal programs with natural numbers. Also, keeping levels as a separate type will make it easier to change it if we wanted to. For instance, non-uniformity might be more trouble than it's worth.</div>
<div><br></div><div>Binding LEVEL to the same type as NATURAL will make things break spectacularly (I believe). There should be a check that you don't do that, but it's not implemented yet.</div><div><br></div><div>
/ Ulf</div></div>