Hi Café,
Can anyone explain why `add1` is rejected in the code below (which uses
the tfp package):
import Types.Data.Num
data A n
where
A :: NaturalT n = Int - A n
getA :: A n - Int
getA (A n) = n
add1 :: NaturalT (m:+:n) = A m - A n - A (m:+:n)
add1 (A a) (A b) = A (a+b)
add2 ::
I forgot to say that I'm using GHC 6.10.1.
Also, the code requires
{-# LANGUAGE FlexibleContexts, GADTs, TypeOperators #-}
/ Emil
Emil Axelsson skrev:
Hi Café,
Can anyone explain why `add1` is rejected in the code below (which uses
the tfp package):
import Types.Data.Num
data A n
