its a special Thing that just uses Integer internally, but because it doenst provide a PEANO api, we can't do computations on it :'(
On Sun, Mar 16, 2014 at 10:37 AM, Henning Thielemann < lemm...@henning-thielemann.de> wrote: > 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? > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
