<div dir="ltr">its a special Thing that just uses Integer internally, but because it doenst provide a PEANO api, we can't do computations on it :'(<div><br></div><div><br></div></div><div class="gmail_extra"><br><br>

<div class="gmail_quote">On Sun, Mar 16, 2014 at 10:37 AM, Henning Thielemann <span dir="ltr"><<a href="mailto:lemming@henning-thielemann.de" target="_blank">lemming@henning-thielemann.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

Am 16.03.2014 14:35, schrieb Carter Schonwald:<div class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
You can't with type lits. The solver can only decide concrete values :"""(<br>
</blockquote>
<br></div>
I hoped that with type-level natural numbers all my dreams would become true. :-)<br>
<br>
I'd be also happy if I could manually provide the proof for 1<=n+1 and more complicated statements like n+n=2*n and n>0 && m>0 => n*m>0.<div class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
You'll have to use a concrete peano Nats type instead.<br>
</blockquote>
<br></div>
That is, I may as well stay with the existing type-level number packages?<div class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I've been toying with the idea that the type lits syntax should be just<br>
that, a type level analogue of from integer that you can give to user<br>
land types, but I'm not going to suggest that till 7.8 is fully released.<br>
</blockquote>
<br></div>
Seems reasonable. By the way, is the GHC Nat kind defined by data promotion or is it a special kind with an efficient internal representation?<br>
<br>
</blockquote></div><br></div>