diff options
| -rw-r--r-- | src/Data/INat.hs | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/src/Data/INat.hs b/src/Data/INat.hs index 7a495ca..2d65c53 100644 --- a/src/Data/INat.hs +++ b/src/Data/INat.hs @@ -13,9 +13,10 @@ module Data.INat where import Data.Proxy +import Data.Type.Equality ((:~:) (Refl)) import Numeric.Natural import GHC.TypeLits - +import Unsafe.Coerce (unsafeCoerce) -- | Evidence for the constraint @c a@. data Dict c a where @@ -73,10 +74,29 @@ type family FromINat n where FromINat (S n) = 1 + FromINat n -- | Convert a "GHC.TypeLits" 'G.Nat' to a 'INat'. -type family ToINat n where +type family ToINat (n :: Nat) where ToINat 0 = Z ToINat n = S (ToINat (n - 1)) +lemInjectiveFromINat :: n :~: ToINat (FromINat n) +lemInjectiveFromINat = unsafeCoerce Refl + +lemSuccFromINat :: Proxy n -> 1 + FromINat n :~: FromINat (S n) +lemSuccFromINat _ = unsafeCoerce Refl + +lemAddFromINat :: Proxy m -> Proxy n + -> FromINat m + FromINat n :~: FromINat (m +! n) +lemAddFromINat _ = unsafeCoerce Refl + +lemInjectiveToINat :: n :~: FromINat (ToINat n) +lemInjectiveToINat = unsafeCoerce Refl + +lemSuccToINat :: Proxy n -> ToINat (1 + n) :~: S (ToINat n) +lemSuccToINat _ = unsafeCoerce Refl + +lemAddToINat :: Proxy m -> Proxy n -> ToINat (m + n) :~: ToINat m +! ToINat n +lemAddToINat _ _ = unsafeCoerce Refl + -- | 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) |