diff options
Diffstat (limited to 'src/Data/INat.hs')
| -rw-r--r-- | src/Data/INat.hs | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/Data/INat.hs b/src/Data/INat.hs index f7523ee..7a495ca 100644 --- a/src/Data/INat.hs +++ b/src/Data/INat.hs @@ -43,7 +43,7 @@ pattern SINat' <- (snatKnown -> Dict) where SINat' = inatSing -- | A 'KnownINat' dictionary is just a singleton natural, so we can create --- evidence of 'KnownNat' given an 'SINat'. +-- evidence of 'KnownINat' given an 'SINat'. snatKnown :: SINat n -> Dict KnownINat n snatKnown SZ = Dict snatKnown (SS n) | Dict <- snatKnown n = Dict @@ -72,6 +72,11 @@ type family FromINat n where FromINat Z = 0 FromINat (S n) = 1 + FromINat n +-- | Convert a "GHC.TypeLits" 'G.Nat' to a 'INat'. +type family ToINat n where + ToINat 0 = Z + ToINat n = S (ToINat (n - 1)) + -- | If an inductive 'INat' is known, then the corresponding "GHC.TypeLits" -- 'G.Nat' is also known. knownNatFromINat :: KnownINat n => Proxy n -> Dict KnownNat (FromINat n) |