diff options
Diffstat (limited to 'src/Data/Nat.hs')
| -rw-r--r-- | src/Data/Nat.hs | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs index 5dacc8a..b154f67 100644 --- a/src/Data/Nat.hs +++ b/src/Data/Nat.hs @@ -44,6 +44,10 @@ unSNat :: SNat n -> Natural unSNat SZ = 0 unSNat (SS n) = 1 + unSNat n +-- | Convert an 'SNat' to an integer. +unSNat' :: SNat n -> Int +unSNat' = fromIntegral . unSNat + -- | A 'KnownNat' dictionary is just a singleton natural, so we can create -- evidence of 'KnownNat' given an 'SNat'. snatKnown :: SNat n -> Dict KnownNat n @@ -68,3 +72,16 @@ gknownNat (Proxy @n) = go (knownNat @n) go :: SNat m -> Dict G.KnownNat (GNat m) go SZ = Dict go (SS n) | Dict <- go n = Dict + +-- * Some type-level naturals + +type N0 = Z +type N1 = S N0 +type N2 = S N1 +type N3 = S N2 +type N4 = S N3 +type N5 = S N4 +type N6 = S N5 +type N7 = S N6 +type N8 = S N7 +type N9 = S N8 |