@@ -1,6 +1,5 @@
1module TypeFun.Data.Peano
1module TypeFun.Data.Peano
@@ -8,24 +7,14 @@ module TypeFun.Data.Peano
11−import Data.Typeable
10+import Data.Typeable
12−import GHC.Generics (Generic)
11+import GHC.Generics (Generic)
13−import GHC.TypeLits
12+import GHC.TypeLits
15data N = Z | S N
14data N = Z | S N
16 deriving ( Eq, Ord, Read, Show
15 deriving ( Eq, Ord, Read, Show
17 , Generic, Typeable )
16 , Generic, Typeable )
20−class KnownPeano (p :: N) where
21− peanoVal :: proxy p -> Integer
23−instance KnownPeano Z where
26−instance (KnownPeano n) => KnownPeano (S n) where
27− peanoVal _ = succ $ peanoVal (Proxy :: Proxy n)
29type family ToNat (a :: N) :: Nat where
18type family ToNat (a :: N) :: Nat where
30 ToNat Z = 0
19 ToNat Z = 0
31 ToNat (S a) = 1 + (ToNat a)
20 ToNat (S a) = 1 + (ToNat a)