|
| 1 | +{-# LANGUAGE CPP #-} |
1 | 2 | {-# LANGUAGE DataKinds #-} |
2 | 3 | {-# LANGUAGE DeriveDataTypeable #-} |
3 | 4 | {-# LANGUAGE FlexibleContexts #-} |
|
8 | 9 | {-# LANGUAGE TypeFamilies #-} |
9 | 10 | {-# LANGUAGE TypeOperators #-} |
10 | 11 | {-# LANGUAGE UndecidableInstances #-} |
| 12 | +#if MIN_VERSION_base(4,8,0) |
| 13 | +{-# LANGUAGE Safe #-} |
| 14 | +#else |
| 15 | +{-# LANGUAGE Trustworthy #-} |
| 16 | +#endif |
11 | 17 | -- | Binary natural numbers. @DataKinds@ stuff. |
12 | 18 | module Data.Type.Bin ( |
13 | 19 | -- * Singleton |
@@ -43,17 +49,18 @@ module Data.Type.Bin ( |
43 | 49 | Bin0, Bin1, Bin2, Bin3, Bin4, Bin5, Bin6, Bin7, Bin8, Bin9, |
44 | 50 | ) where |
45 | 51 |
|
46 | | -import Data.Bin (Bin (..), BinP (..)) |
47 | | -import Data.Nat (Nat (..)) |
48 | | -import Data.Proxy (Proxy (..)) |
49 | | -import Data.Type.Equality ((:~:) (..), TestEquality (..)) |
50 | | -import Data.Typeable (Typeable) |
51 | | -import Numeric.Natural (Natural) |
52 | | -import Data.Type.BinP (SBinP (..), SBinPI (..)) |
| 52 | +import Data.Bin (Bin (..), BinP (..)) |
| 53 | +import Data.Nat (Nat (..)) |
| 54 | +import Data.Proxy (Proxy (..)) |
| 55 | +import Data.Type.BinP (SBinP (..), SBinPI (..)) |
| 56 | +import Data.Typeable (Typeable) |
| 57 | +import Numeric.Natural (Natural) |
53 | 58 |
|
54 | | -import qualified Data.Type.Nat as N |
55 | | -import qualified GHC.TypeLits as GHC |
56 | 59 | import qualified Data.Type.BinP as BP |
| 60 | +import qualified Data.Type.Nat as N |
| 61 | +import qualified GHC.TypeLits as GHC |
| 62 | + |
| 63 | +import TrustworthyCompat |
57 | 64 |
|
58 | 65 | -- $setup |
59 | 66 | -- >>> :set -XDataKinds |
@@ -288,7 +295,7 @@ type family Mult2Plus1 (b :: Bin) :: BinP where |
288 | 295 | -- >>> :kind! Succ Bin5 |
289 | 296 | -- Succ Bin5 :: Bin |
290 | 297 | -- = 'BP ('B0 ('B1 'BE)) |
291 | | --- |
| 298 | +-- |
292 | 299 | -- @ |
293 | 300 | -- `Succ` :: 'Bin' -> 'Bin' |
294 | 301 | -- `Succ'` :: 'Bin' -> 'BinP' |
|
0 commit comments