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?