type-natural 0.0.5.0 → 0.0.6.0

raw patch · 2 files changed

+14/−2 lines, 2 files

Files

• Data/Type/Ordinal.hs +13/−1
• type-natural.cabal +1/−1

@@ -7,7 +7,9 @@        ( -- * Data-types          Ordinal (..),          -- * Conversion from cardinals to ordinals.-         sNatToOrd', sNatToOrd, ordToInt, ordToSNat, unsafeFromInt,+         sNatToOrd', sNatToOrd, ordToInt, ordToSNat,+         ordToSNat', CastedOrdinal(..),+         unsafeFromInt,          -- * Ordinal arithmetics          (@+), enumOrdinal        ) where@@ -86,6 +88,16 @@ -- | 'sNatToOrd'' with @n@ inferred. sNatToOrd :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal n sNatToOrd = sNatToOrd' sing++data CastedOrdinal n where+  CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n++-- | Convert @Ordinal n@ into @SNat m@ with the proof of @S m :<<= n@.+ordToSNat' :: Ordinal n -> CastedOrdinal n+ordToSNat' OZ = CastedOrdinal sZ+ordToSNat' (OS on) =+  case ordToSNat' on of+    CastedOrdinal m -> CastedOrdinal (sS m)  -- | Convert @Ordinal n@ into monomorphic @SNat@ ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.0.5.0+version:             0.0.6.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties. homepage:            https://github.com/konn/type-natural