positive type-level naturals

[Henning Thielemann]

Am 16.03.2014 14:35, schrieb Carter Schonwald:

> You can't with type lits. The solver can only decide concrete values :"""(

I hoped that with type-level natural numbers all my dreams would become 
true. :-)

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.

> You'll have to use a concrete peano Nats type instead.

That is, I may as well stay with the existing type-level number packages?

> I've been toying with the idea that the type lits syntax should be just
> that, a type level analogue of from integer that you can give to user
> land types, but I'm not going to suggest that till 7.8 is fully released.

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?