23 Sep
2008
23 Sep
'08
12:31 a.m.
Try
n01 :: Nat One
-- ryan
On Mon, Sep 22, 2008 at 8:10 PM, Anatoly Yakovenko
type One = S Z type Two = S One etc.
why does:
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
type One = S Z n00 = Z n01::One = S n00
give me:
test.hs:10:11: Couldn't match expected type `One' against inferred type `Nat (S a)' In the expression: S n00 In a pattern binding: n01 :: One = S n00 Failed, modules loaded: none.
or better yet, how is type S Z different from, n01 :: forall a. Nat (S a) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe