1 module Data.HList.Number
17 import Language.Haskell.TH
24 data HZero = HZero deriving Show
32 data HSucc n = HSucc n deriving Show
34 instance HNat n => HNat (HSucc n)
36 hSucc :: HNat n => n -> HSucc n
39 hPred :: HNat n => HSucc n -> n
43 hNatLiteralT :: Integral n => n -> Q Type
45 | n == 0 = conT (mkName "HZero")
46 | otherwise = appT (conT (mkName "HSucc"))
47 (hNatLiteralT (n - 1))
49 hNatLiteralE :: Integral n => n -> Q Exp
51 | n == 0 = varE (mkName "hZero")
52 | otherwise = appE (varE (mkName "hSucc"))
53 (hNatLiteralE (n - 1))
55 hNatLiteralP :: Integral n => n -> Q Pat
57 | n == 0 = varP (mkName "HZero")
58 | otherwise = conP (mkName "HSucc") [hNatLiteralP n]