type-natural 0.7.0.0 → 0.7.1.0

raw patch · 2 files changed

+14/−14 lines, 2 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

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

@@ -3,7 +3,7 @@ -- | Module providing the same API as 'Data.Type.Ordinal' but specialised to --   GHC's builtin @'Nat'@. --   ---   Since 0.7.0.0+--   Since 0.7.1.0 module Data.Type.Ordinal.Builtin        ( -- * Data-types and pattern synonyms          Ordinal, pattern OLt, pattern OZ, pattern OS,@@ -15,14 +15,14 @@          unsafeFromInt, inclusion, inclusion',          -- * Ordinal arithmetics          (@+), enumOrdinal,-         -- * Elimination rules for @'Ordinal' 'Z'@.+         -- * Elimination rules for @'Ordinal' 0'@.          absurdOrd, vacuousOrd        ) where import           Data.Kind-import           Data.Singletons.Prelude      (POrd (..), SingI, Sing (..))+import           Data.Singletons.Prelude      (POrd (..), Sing (..)) import           Data.Singletons.Prelude.Enum (PEnum (..)) import qualified Data.Type.Ordinal            as O-import           Data.Type.Natural+import           GHC.TypeLits import           Language.Haskell.TH.Quote    (QuasiQuoter) import           Data.Type.Monomorphic @@ -30,7 +30,7 @@ -- -- > n = {0, 1, ..., n-1} ----- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@.+-- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 0@ is isomorphic to @Void@. -- This module exports a variant of polymorphic @'Data.Type.Ordinal.Ordinal'@ -- specialised to GHC's builtin numeral @'Nat'@. --   @@ -50,13 +50,13 @@ --    --   Since 0.7.0.0 pattern OZ :: forall  (n :: Nat). ()-           => ('Z :< n) ~ 'True => O.Ordinal n+           => (0 :< n) ~ 'True => O.Ordinal n pattern OZ = O.OZ  -- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. --    --   Since 0.7.0.0-pattern OS :: forall (t :: Nat). (SingI t)+pattern OS :: forall (t :: Nat). (KnownNat t)            => () => O.Ordinal t -> O.Ordinal (Succ t) pattern OS n = O.OS n @@ -90,7 +90,7 @@ -- | 'sNatToOrd'' with @n@ inferred. --    --   Since 0.7.0.0-sNatToOrd :: (SingI n, (m :< n) ~ 'True) => Sing m -> Ordinal n+sNatToOrd :: (KnownNat n, (m :< n) ~ 'True) => Sing m -> Ordinal n sNatToOrd = O.sNatToOrd {-# INLINE sNatToOrd #-} @@ -101,7 +101,7 @@ ordToInt = O.ordToInt {-# INLINE ordToInt #-} -unsafeFromInt :: SingI n+unsafeFromInt :: KnownNat n               => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n unsafeFromInt = O.unsafeFromInt {-# INLINE unsafeFromInt #-}@@ -123,7 +123,7 @@ -- | Ordinal addition. -- --   Since 0.7.0.0-(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+(@+) :: (KnownNat n, KnownNat m) => Ordinal n -> Ordinal m -> Ordinal (n + m) (@+) = (O.@+) {-# INLINE (@+) #-} @@ -134,16 +134,16 @@ enumOrdinal = O.enumOrdinal {-# INLINE enumOrdinal #-} --- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value.+-- | Since @Ordinal 0@ is logically not inhabited, we can coerce it to any value. -- --   Since 0.7.0.0-absurdOrd :: Ordinal 'Z -> a+absurdOrd :: Ordinal 0 -> a absurdOrd = O.absurdOrd {-# INLINE absurdOrd #-}  -- | @'absurdOrd'@ for values in 'Functor'. -- --   Since 0.7.0.0-vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a+vacuousOrd :: Functor f => f (Ordinal 0) -> f a vacuousOrd = O.vacuousOrd {-# INLINE vacuousOrd #-}

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.7.0.0+version:             0.7.1.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties.                      .