type-natural 0.6.1.1 → 0.7.0.0

raw patch · 7 files changed

+390/−58 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Type/Natural.hs +4/−18
• Data/Type/Natural/Builtin.hs +12/−4
• Data/Type/Natural/Class.hs +29/−3
• Data/Type/Ordinal.hs +44/−32
• Data/Type/Ordinal/Builtin.hs +149/−0
• Data/Type/Ordinal/Peano.hs +149/−0
• type-natural.cabal +3/−1

@@ -31,7 +31,7 @@                           -- * Conversion functions                           natToInt, intToNat, sNatToInt,                           -- * Quasi quotes for natural numbers-                          nat, snat,+                          snat,                           -- * Properties of natural numbers                           IsPeano(..),                           plusCong, plusCongR, plusCongL,@@ -279,23 +279,9 @@ -- * Quasi Quoter -------------------------------------------------- --- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type.------   for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@-nat :: QuasiQuoter-nat = QuasiQuoter { quoteExp = foldr appE (conE 'Z) . flip replicate (conE 'S) . read-                  , quotePat = foldr (\a b -> conP a [b]) (conP 'Z []) . flip replicate 'S . read-                  , quoteType = foldr appT (conT 'Z) . flip replicate (conT 'S) . read-                  , quoteDec = error "not implemented"-                  }---- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type.+-- | Quotesi-quoter for 'SNat'. This can be used for an expression. -----  For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@+--  For example: @[snat|12|] '%:+' [snat| 5 |]@. snat :: QuasiQuoter-snat = QuasiQuoter { quoteExp = foldr appE (conE 'SZ) . flip replicate (conE 'SS) . read-                   , quotePat = foldr (\a b -> conP a [b]) (conP 'SZ []) . flip replicate 'SS . read-                   , quoteType = appT (conT ''SNat) . foldr appT (conT 'Z) . flip replicate (conT 'S) . read-                   , quoteDec = error "not implemented"-                   }+snat = mkSNatQQ [t| Nat |] 

@@ -24,6 +24,8 @@          -- * Peano and commutative ring axioms for built-in @'GHC.TypeLits.Nat'@          IsPeano(..),          inductionNat,+         -- * QuasiQuotes+         snat        )        where import Data.Type.Natural.Class@@ -46,6 +48,7 @@ import           Data.Void                    (Void) import           GHC.TypeLits                 (type (+), type (<=), type (<=?)) import qualified GHC.TypeLits                 as TL+import           Language.Haskell.TH.Quote    (QuasiQuoter) import           Proof.Equational             (coerce, withRefl) import           Proof.Equational             (start, sym, (===), (=~=)) import           Proof.Equational             (because)@@ -276,8 +279,8 @@  -- | Induction scheme for built-in @'TL.Nat'@. inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n-inductionNat base step snat =-  case viewNat snat of+inductionNat base step sn =+  case viewNat sn of     IsZero -> base     IsSucc sl -> step (inductionNat base step sl) @@ -303,8 +306,8 @@   multAssoc _ _ _ = Refl   plusMultDistrib _ _ _ = Refl   multPlusDistrib _ _ _ = Refl-  induction base step snat =-    case viewNat snat of+  induction base step sn =+    case viewNat sn of       IsZero    -> base       IsSucc sl ->         withKnownNat sl $ step sing (induction base step sl)@@ -414,3 +417,8 @@   promote n = case toSing n of SomeSing k -> Monomorphic k   {-# INLINE promote #-} +-- | Quotesi-quoter for singleton types for @'GHC.TypeLits.Nat'@. This can be used for an expression.+--+--  For example: @[snat|12|] '%:+' [snat| 5 |]@.+snat :: QuasiQuoter+snat = mkSNatQQ [t| TL.Nat |]

@@ -1,7 +1,33 @@+{-# LANGUAGE TemplateHaskell #-} -- | Re-exports arithmetic and order structure for peano arithmetic.-module Data.Type.Natural.Class ( module Data.Type.Natural.Class.Arithmetic-                               , module Data.Type.Natural.Class.Order-                               ) where+module Data.Type.Natural.Class+       ( module Data.Type.Natural.Class.Arithmetic+       , module Data.Type.Natural.Class.Order+       , -- * Quasi quoters generator for naturals+         mkSNatQQ) where import Data.Type.Natural.Class.Arithmetic import Data.Type.Natural.Class.Order +import Data.Singletons.Prelude   (FromInteger, Sing, sing)+import Language.Haskell.TH+import Language.Haskell.TH.Quote++-- | Quasiquoter generateor for specific peano-types.+--+--   Since 0.7.0.0+mkSNatQQ :: TypeQ -> QuasiQuoter+mkSNatQQ t = QuasiQuoter+             { quoteExp = mkExpQuote+             , quotePat = error  "no pattern quoter for snats"+                          -- foldr (\a b -> conP a [b]) (conP 'SZ []) . flip replicate 'SS . read+             , quoteType = mkTypeQuote+             , quoteDec = error "not implemented"+             }+  where+    mkExpQuote ::  String -> ExpQ+    mkExpQuote s = [| sing :: $(mkTypeQuote s) |]++    mkTypeQuote :: String -> TypeQ+    mkTypeQuote s =+      let n = read s+      in [t| Sing $(sigT [t| FromInteger $(litT $ numTyLit n)|]  =<< t) |]

@@ -8,21 +8,21 @@ module Data.Type.Ordinal        ( -- * Data-types          Ordinal (..), pattern OZ, pattern OS, HasOrdinal,+         -- * Quasi Quoter+         -- $quasiquotes+         mkOrdinalQQ, odPN, odLit,          -- * Conversion from cardinals to ordinals.          sNatToOrd', sNatToOrd, ordToInt, ordToSing,-         ordToSing', CastedOrdinal(..),          unsafeFromInt, inclusion, inclusion',          -- * Ordinal arithmetics          (@+), enumOrdinal,          -- * Elimination rules for @'Ordinal' 'Z'@.-         absurdOrd, vacuousOrd, vacuousOrdM,-         -- * Quasi Quoter-         od+         absurdOrd, vacuousOrd        ) where-import           Control.Monad                (liftM) import           Data.Kind import           Data.List                    (genericDrop, genericTake) import           Data.Ord                     (comparing)+import           Data.Singletons.Decide import           Data.Singletons.Prelude import           Data.Singletons.Prelude.Enum import           Data.Type.Equality@@ -46,7 +46,7 @@ -- -- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. -----   Since 0.5.0.0+--   Since 0.6.0.0 data Ordinal (n :: nat) where   OLt :: (IsPeano nat, (n :< m) ~ 'True) => Sing (n :: nat) -> Ordinal m @@ -57,12 +57,16 @@   OLt n  -- | Pattern synonym representing the 0-th ordinal.+--+--   Since 0.6.0.0 pattern OZ :: forall nat (n :: nat). IsPeano nat            => (Zero nat :< n) ~ 'True => Ordinal n pattern OZ <- OLt Zero where   OZ = OLt sZero  -- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal.+--+--   Since 0.6.0.0 pattern OS :: forall nat (t :: nat). (PeanoOrder nat, SingI t)             => (IsPeano nat)             => Ordinal t -> Ordinal (Succ t)@@ -133,7 +137,8 @@             => Ordinal n -> [Ordinal n] enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n) -enumOrdinal :: (PeanoOrder nat, SingI n) => Sing (n :: nat) -> [Ordinal n]+-- | Enumerate all @'Ordinal'@s less than @n@.+enumOrdinal :: (PeanoOrder nat) => Sing (n :: nat) -> [Ordinal n] enumOrdinal (Succ n) = withSingI n $   withWitness (lneqZero n) $       OLt sZero : map succOrd (enumOrdinal n)@@ -162,7 +167,6 @@     sNatToOrd (sing :: Sing m)   {-# INLINE maxBound #-} - unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))               => MonomorphicRep (Sing :: nat -> *) -> Ordinal n unsafeFromInt n =@@ -192,14 +196,6 @@ sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n sNatToOrd = sNatToOrd' sing -data CastedOrdinal n where-  CastedOrdinal :: (m :< n) ~ 'True => Sing m -> CastedOrdinal n---- | Convert @Ordinal n@ into @Sing m@ with the proof of @'S m :<= n@.-ordToSing' :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> CastedOrdinal n-ordToSing' (OLt s) = CastedOrdinal s-{-# INLINE ordToSing' #-}- -- | Convert @Ordinal n@ into monomorphic @Sing@ -- -- Since 0.5.0.0@@ -216,11 +212,15 @@ {-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Integer #-}  -- | Inclusion function for ordinals.-inclusion' :: (n :< m) ~ 'True => Sing m -> Ordinal n -> Ordinal m+--+--   Since 0.7.0.0 (constraint was weakened since last released)+inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m inclusion' _ = unsafeCoerce {-# INLINE inclusion' #-}  -- | Inclusion function for ordinals with codomain inferred.+--+--   Since 0.7.0.0 (constraint was weakened since last released) inclusion :: ((n :<= m) ~ 'True) => Ordinal n -> Ordinal m inclusion on = unsafeCoerce on {-# INLINE inclusion #-}@@ -239,24 +239,36 @@ absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a absurdOrd (OLt n) = absurd $ lneqZeroAbsurd n Witness --- | 'absurdOrd' for the value in 'Functor'.+-- | @'absurdOrd'@ for value in 'Functor'. -- --   Since 0.2.3.0 vacuousOrd :: (PeanoOrder nat, Functor f) => f (Ordinal (Zero nat)) -> f a vacuousOrd = fmap absurdOrd --- | 'absurdOrd' for the value in 'Monad'.---   This function will become uneccesary once 'Applicative' (and hence 'Functor')---   become the superclass of 'Monad'.------   Since 0.2.3.0-vacuousOrdM :: (PeanoOrder nat, Monad m) => m (Ordinal (Zero nat)) -> m a-vacuousOrdM = liftM absurdOrd+{-$quasiquotes #quasiquoters# --- | Quasiquoter for ordinals-od :: QuasiQuoter-od = QuasiQuoter { quoteExp = foldr appE (conE 'OZ) . flip replicate (conE 'OS) . read-                 , quoteType = error "No type quoter for Ordinals"-                 , quotePat = foldr (\a b -> conP a [b]) (conP 'OZ []) . flip replicate 'OS . read-                 , quoteDec = error "No declaration quoter for Ordinals"-                 }+   This section provides QuasiQuoter and general generator for ordinals.+   Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT+   checks boundary; with @'od'@, we can use literal with+   boundary check.+   For example, with @-XQuasiQuotes@ language extension enabled,+   @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error,+   whilst @12 :: Ordinal 1@ compiles but raises run-time error.+   So, to enforce correctness, we recommend to use these quoters+   instead of bare @'Num'@ numerals.+-}++-- | Quasiquoter generator for ordinals+mkOrdinalQQ :: TypeQ -> QuasiQuoter+mkOrdinalQQ t =+  QuasiQuoter { quoteExp  = \s -> [| OLt $(quoteExp (mkSNatQQ t) s) |]+              , quoteType = error "No type quoter for Ordinals"+              , quotePat  = \s -> [p| OLt ((%~ $(quoteExp (mkSNatQQ t) s)) -> Proved Refl) |]+              , quoteDec  = error "No declaration quoter for Ordinals"+              }++odPN, odLit :: QuasiQuoter+-- | Quasiquoter for ordinal indexed by Peano numeral @'Data.Type.Natural.Nat'@.+odPN  = mkOrdinalQQ [t| PN.Nat |]+-- | Quasiquoter for ordinal indexed by built-in numeral @'GHC.TypeLits.Nat'@.+odLit = mkOrdinalQQ [t| TL.Nat |]

@@ -0,0 +1,149 @@+{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs    #-}+{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-}+-- | Module providing the same API as 'Data.Type.Ordinal' but specialised to+--   GHC's builtin @'Nat'@.+--   +--   Since 0.7.0.0+module Data.Type.Ordinal.Builtin+       ( -- * Data-types and pattern synonyms+         Ordinal, pattern OLt, pattern OZ, pattern OS,+         -- * Quasi Quoter+         -- $quasiquotes+         od,+         -- * Conversion from cardinals to ordinals.+         sNatToOrd', sNatToOrd, ordToInt,+         unsafeFromInt, inclusion, inclusion',+         -- * Ordinal arithmetics+         (@+), enumOrdinal,+         -- * Elimination rules for @'Ordinal' 'Z'@.+         absurdOrd, vacuousOrd+       ) where+import           Data.Kind+import           Data.Singletons.Prelude      (POrd (..), SingI, Sing (..))+import           Data.Singletons.Prelude.Enum (PEnum (..))+import qualified Data.Type.Ordinal            as O+import           Data.Type.Natural+import           Language.Haskell.TH.Quote    (QuasiQuoter)+import           Data.Type.Monomorphic++-- | Set-theoretic (finite) ordinals:+--+-- > n = {0, 1, ..., n-1}+--+-- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@.+-- This module exports a variant of polymorphic @'Data.Type.Ordinal.Ordinal'@+-- specialised to GHC's builtin numeral @'Nat'@.+--   +--   Since 0.7.0.0+type Ordinal (n :: Nat) = O.Ordinal n++-- | We provide specialised version of constructor @'O.OLt'@ as type synonym @'OLt'@.+--   In some case, GHC warns about incomplete pattern using pattern  @'OLt'@,+--   but it is due to the limitation of GHC's current exhaustiveness checker.+--   +--   Since 0.7.0.0+pattern OLt :: () => forall  (n1 :: Nat). ((n1 :< t) ~ 'True)+            => Sing n1 -> O.Ordinal t+pattern OLt n = O.OLt n++-- | Pattern synonym representing the 0-th ordinal.+--   +--   Since 0.7.0.0+pattern OZ :: forall  (n :: Nat). ()+           => ('Z :< 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)+           => () => O.Ordinal t -> O.Ordinal (Succ t)+pattern OS n = O.OS n++{-$quasiquotes #quasiquoters#++   This section provides QuasiQuoter for ordinals.+   Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT+   checks boundary; with @'od'@, we can use literal with+   boundary check.+   For example, with @-XQuasiQuotes@ language extension enabled,+   @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error,+   whilst @12 :: Ordinal 1@ compiles but raises run-time error.+   So, to enforce correctness, we recommend to use these quoters+   instead of bare @'Num'@ numerals.+-}++-- | Quasiquoter for ordinal indexed by GHC's built-n @'Data.Type.Natural.Nat'@.+--   +--   Since 0.7.0.0+od :: QuasiQuoter+od = O.odLit+{-# INLINE od #-}++-- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.+--   +--   Since 0.7.0.0+sNatToOrd' :: (m :< n) ~ 'True => Sing n -> Sing m -> Ordinal n+sNatToOrd' = O.sNatToOrd'+{-# INLINE sNatToOrd' #-}++-- | 'sNatToOrd'' with @n@ inferred.+--   +--   Since 0.7.0.0+sNatToOrd :: (SingI n, (m :< n) ~ 'True) => Sing m -> Ordinal n+sNatToOrd = O.sNatToOrd+{-# INLINE sNatToOrd #-}++-- | Convert ordinal into @Int@.+--   +--   Since 0.7.0.0+ordToInt :: Ordinal n -> Integer+ordToInt = O.ordToInt+{-# INLINE ordToInt #-}++unsafeFromInt :: SingI n+              => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n+unsafeFromInt = O.unsafeFromInt+{-# INLINE unsafeFromInt #-}++-- | Inclusion function for ordinals.+--+--   Since 0.7.0.0+inclusion :: (n :<= m) ~ 'True => Ordinal n -> Ordinal m+inclusion = O.inclusion+{-# INLINE inclusion #-}++-- | Inclusion function for ordinals with codomain inferred.+--+--   Since 0.7.0.0+inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m+inclusion' = O.inclusion'+{-# INLINE inclusion' #-}++-- | Ordinal addition.+--+--   Since 0.7.0.0+(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+(@+) = (O.@+)+{-# INLINE (@+) #-}++-- | Enumerate all @'Ordinal'@s less than @n@.+--+--   Since 0.7.0.0+enumOrdinal :: Sing n -> [Ordinal n]+enumOrdinal = O.enumOrdinal+{-# INLINE enumOrdinal #-}++-- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value.+--+--   Since 0.7.0.0+absurdOrd :: Ordinal 'Z -> 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 = O.vacuousOrd+{-# INLINE vacuousOrd #-}

@@ -0,0 +1,149 @@+{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleInstances, GADTs    #-}+{-# LANGUAGE KindSignatures, PatternSynonyms, TypeInType, TypeOperators #-}+-- | Module providing the same API as 'Data.Type.Ordinal' but specialised to+--   peano numeral @'Nat'@.+--   +--   Since 0.7.0.0+module Data.Type.Ordinal.Peano+       ( -- * Data-types and pattern synonyms+         Ordinal, pattern OLt, pattern OZ, pattern OS,+         -- * Quasi Quoter+         -- $quasiquotes+         od,+         -- * Conversion from cardinals to ordinals.+         sNatToOrd', sNatToOrd, ordToInt,+         unsafeFromInt, inclusion, inclusion',+         -- * Ordinal arithmetics+         (@+), enumOrdinal,+         -- * Elimination rules for @'Ordinal' 'Z'@.+         absurdOrd, vacuousOrd+       ) where+import           Data.Kind+import           Data.Singletons.Prelude      (POrd (..), SingI, Sing (..))+import           Data.Singletons.Prelude.Enum (PEnum (..))+import qualified Data.Type.Ordinal            as O+import           Data.Type.Natural+import           Language.Haskell.TH.Quote    (QuasiQuoter)+import           Data.Type.Monomorphic++-- | Set-theoretic (finite) ordinals:+--+-- > n = {0, 1, ..., n-1}+--+-- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@.+-- This module exports a variant of polymorphic @'Data.Type.Ordinal.Ordinal'@+-- specialised to Peano numeral @'Nat'@.+--   +--   Since 0.7.0.0+type Ordinal (n :: Nat) = O.Ordinal n++-- | We provide specialised version of constructor @'O.OLt'@ as type synonym @'OLt'@.+--   In some case, GHC warns about incomplete pattern using pattern  @'OLt'@,+--   but it is due to the limitation of GHC's current exhaustiveness checker.+--   +--   Since 0.7.0.0+pattern OLt :: () => forall  (n1 :: Nat). ((n1 :< t) ~ 'True)+            => Sing n1 -> O.Ordinal t+pattern OLt n = O.OLt n++-- | Pattern synonym representing the 0-th ordinal.+--   +--   Since 0.7.0.0+pattern OZ :: forall  (n :: Nat). ()+           => ('Z :< 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)+           => () => O.Ordinal t -> O.Ordinal (Succ t)+pattern OS n = O.OS n++{-$quasiquotes #quasiquoters#++   This section provides QuasiQuoter for ordinals.+   Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT+   checks boundary; with @'od'@, we can use literal with+   boundary check.+   For example, with @-XQuasiQuotes@ language extension enabled,+   @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error,+   whilst @12 :: Ordinal 1@ compiles but raises run-time error.+   So, to enforce correctness, we recommend to use these quoters+   instead of bare @'Num'@ numerals.+-}++-- | Quasiquoter for ordinal indexed by Peano numeral @'Data.Type.Natural.Nat'@.+--   +--   Since 0.7.0.0+od :: QuasiQuoter+od = O.odLit+{-# INLINE od #-}++-- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.+--   +--   Since 0.7.0.0+sNatToOrd' :: (m :< n) ~ 'True => Sing n -> Sing m -> Ordinal n+sNatToOrd' = O.sNatToOrd'+{-# INLINE sNatToOrd' #-}++-- | 'sNatToOrd'' with @n@ inferred.+--   +--   Since 0.7.0.0+sNatToOrd :: (SingI n, (m :< n) ~ 'True) => Sing m -> Ordinal n+sNatToOrd = O.sNatToOrd+{-# INLINE sNatToOrd #-}++-- | Convert ordinal into @Int@.+--   +--   Since 0.7.0.0+ordToInt :: Ordinal n -> Integer+ordToInt = O.ordToInt+{-# INLINE ordToInt #-}++unsafeFromInt :: SingI n+              => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n+unsafeFromInt = O.unsafeFromInt+{-# INLINE unsafeFromInt #-}++-- | Inclusion function for ordinals.+--+--   Since 0.7.0.0+inclusion :: (n :<= m) ~ 'True => Ordinal n -> Ordinal m+inclusion = O.inclusion+{-# INLINE inclusion #-}++-- | Inclusion function for ordinals with codomain inferred.+--+--   Since 0.7.0.0+inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m+inclusion' = O.inclusion'+{-# INLINE inclusion' #-}++-- | Ordinal addition.+--+--   Since 0.7.0.0+(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+(@+) = (O.@+)+{-# INLINE (@+) #-}++-- | Enumerate all @'Ordinal'@s less than @n@.+--+--   Since 0.7.0.0+enumOrdinal :: Sing n -> [Ordinal n]+enumOrdinal = O.enumOrdinal+{-# INLINE enumOrdinal #-}++-- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value.+--+--   Since 0.7.0.0+absurdOrd :: Ordinal 'Z -> 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 = O.vacuousOrd+{-# INLINE vacuousOrd #-}

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.6.1.1+version:             0.7.0.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties.                      .@@ -31,6 +31,8 @@     ghc-options:       -Wno-redundant-constraints   exposed-modules:     Data.Type.Natural                      , Data.Type.Ordinal+                     , Data.Type.Ordinal.Builtin+                     , Data.Type.Ordinal.Peano                      , Data.Type.Natural.Builtin                      , Data.Type.Natural.Class                      , Data.Type.Natural.Class.Arithmetic