lift (Index i) = sigE [| (Index i) |] (decIndexT (fromIntegerT (undefined :: nT)))
decIndexT :: Integer -> Q Type
decIndexT n = appT (conT (''Index)) (decLiteralT n)
fromNaturalT :: ( NaturalT n
lift (Index i) = sigE [| (Index i) |] (decIndexT (fromIntegerT (undefined :: nT)))
decIndexT :: Integer -> Q Type
decIndexT n = appT (conT (''Index)) (decLiteralT n)
fromNaturalT :: ( NaturalT n
- | n > fromIntegerT (undefined :: nT) =
- error $ "Num.fromInteger{Index " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to make Index larger than " ++ show (fromIntegerT (undefined :: nT)) ++ ", n: " ++ show n
+ | n >= fromIntegerT (undefined :: nT) =
+ error $ "Num.fromInteger{Index " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to make Index larger than " ++ show (fromIntegerT (undefined :: nT) - 1) ++ ", n: " ++ show n
a `quotRem` b =
let (quot, rem) = toInteger a `quotRem` toInteger b
in (fromInteger quot, fromInteger rem)
a `quotRem` b =
let (quot, rem) = toInteger a `quotRem` toInteger b
in (fromInteger quot, fromInteger rem)