fin 0.3.1 → 0.3.2

raw patch · 4 files changed

+39/−4 lines, 4 filesdep ~QuickCheckdep ~basedep ~inspection-testingPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: QuickCheck, base, inspection-testing, some

API changes (from Hackage documentation)

Files

• ChangeLog.md +4/−0
• fin.cabal +2/−2
• src/Data/Fin.hs +1/−1
• src/Data/Type/Nat.hs +32/−1

@@ -1,5 +1,9 @@ # Version history for fin +## 0.3.2++- Add `SS' :: SNat n -> SNat (S n)`, pattern synonym with explicit argument.+ ## 0.3.1  - Support GHC-8.6.5...9.10.1

@@ -1,6 +1,6 @@ cabal-version:      2.2 name:               fin-version:            0.3.1+version:            0.3.2 synopsis:           Nat and Fin: peano naturals and finite numbers category:           Data, Dependent Types, Singletons, Math description:@@ -94,7 +94,7 @@   build-depends:     , boring         ^>=0.2.2     , dec            ^>=0.0.6-    , hashable       ^>=1.4.4.0+    , hashable       ^>=1.4.4.0 || ^>=1.5.0.0     , QuickCheck     ^>=2.14.2  || ^>=2.15     , some           ^>=1.0.6     , universe-base  ^>=1.1.4

@@ -81,7 +81,7 @@ -- >>> import qualified Data.Universe.Helpers as U -- >>> import Data.EqP (eqp) -- >>> import Data.OrdP (comparep)--- >>> :set -XTypeApplications+-- >>> :set -XTypeApplications -XGADTs  ------------------------------------------------------------------------------- -- Type

@@ -3,6 +3,7 @@ {-# LANGUAGE EmptyCase            #-} {-# LANGUAGE GADTs                #-} {-# LANGUAGE KindSignatures       #-}+{-# LANGUAGE PatternSynonyms      #-} {-# LANGUAGE RankNTypes           #-} {-# LANGUAGE ScopedTypeVariables  #-} {-# LANGUAGE StandaloneDeriving   #-}@@ -10,6 +11,7 @@ {-# LANGUAGE TypeFamilies         #-} {-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns         #-} -- | 'Nat' numbers. @DataKinds@ stuff. -- -- This module re-exports "Data.Nat", and adds type-level things.@@ -23,7 +25,7 @@     explicitShow,     explicitShowsPrec,     -- * Singleton-    SNat(..),+    SNat(SZ,SS,SS'),     snatToNat,     snatToNatural,     -- * Implicit@@ -176,6 +178,35 @@ snatToNatural :: forall n. SNat n -> Natural snatToNatural SZ = 0 snatToNatural SS = unKonst (induction (Konst 0) (kmap succ) :: Konst Natural n)++-------------------------------------------------------------------------------+-- Explicit constructor+-------------------------------------------------------------------------------++data SNat_ (n :: Nat) where+    SZ_ :: SNat_ 'Z+    SS_ :: SNat n -> SNat_ ('S n)++snat_ :: SNat n -> SNat_ n+snat_ SZ = SZ_+snat_ SS = SS_ snat++-- | A pattern with explicit argument+--+-- >>> let predSNat :: SNat (S n) -> SNat n; predSNat (SS' n) = n+-- >>> predSNat (SS' (SS' SZ))+-- SS+--+-- >>> reflect $ predSNat (SS' (SS' SZ))+-- 1+--+--+-- @since 0.3.2+pattern SS' :: () => (m ~ 'S n) => SNat n -> SNat m+pattern SS' n <- (snat_ -> SS_ n)+  where SS' n = withSNat n SS++{-# COMPLETE SZ, SS' #-}  ------------------------------------------------------------------------------- -- Equality