Hello Troels,
there is no solver included with ghc 7.6, if you wish to experiment with
equational reasoning with the type level nats, you'll have to look into the
ghc type-lits branch which includes a solver.
(yes, confusng, but true)
On Tue, Oct 2, 2012 at 2:54 PM, Troels Henriksen wrote:
> Co
Consider the following definition of lists with a statically determined
minimum length.
data Nat' = Z | S Nat'
data NList (n::Nat') a where
Rest :: [a] -> NList Z a
(:>) :: a -> NList n a -> NList (S n) a
uncons :: NList (S n) a -> (a, NList n a)
uncons (x :> xs) = (x, xs)
This works fine.
