packages feed

type-natural 0.0.1.1 → 0.0.2.0

raw patch · 2 files changed

+15/−4 lines, 2 filesdep +monomorphicPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: monomorphic

API changes (from Hackage documentation)

+ Data.Type.Natural: instance Monomorphicable Nat (Sing Nat)
- Data.Type.Natural: (%:*) :: Sing t_a3Zb -> forall (t_a3Zc :: Nat). Sing t_a3Zc -> Sing (:* t_a3Zb t_a3Zc)
+ Data.Type.Natural: (%:*) :: Sing t_a3ZM -> forall (t_a3ZN :: Nat). Sing t_a3ZN -> Sing (:* t_a3ZM t_a3ZN)
- Data.Type.Natural: (%:+) :: Sing t_a3Z7 -> forall (t_a3Z8 :: Nat). Sing t_a3Z8 -> Sing (:+ t_a3Z7 t_a3Z8)
+ Data.Type.Natural: (%:+) :: Sing t_a3ZI -> forall (t_a3ZJ :: Nat). Sing t_a3ZJ -> Sing (:+ t_a3ZI t_a3ZJ)
- Data.Type.Natural: (%:-) :: Sing t_a3Z9 -> forall (t_a3Za :: Nat). Sing t_a3Za -> Sing (:- t_a3Z9 t_a3Za)
+ Data.Type.Natural: (%:-) :: Sing t_a3ZK -> forall (t_a3ZL :: Nat). Sing t_a3ZL -> Sing (:- t_a3ZK t_a3ZL)
- Data.Type.Natural: (%:<<=) :: Sing t_a4B2 -> forall (t_a4B3 :: Nat). Sing t_a4B3 -> Sing (:<<= t_a4B2 t_a4B3)
+ Data.Type.Natural: (%:<<=) :: Sing t_a4BD -> forall (t_a4BE :: Nat). Sing t_a4BE -> Sing (:<<= t_a4BD t_a4BE)
- Data.Type.Natural: sMax :: Sing t_a3NE -> forall (t_a3NF :: Nat). Sing t_a3NF -> Sing (Max t_a3NE t_a3NF)
+ Data.Type.Natural: sMax :: Sing t_a3Of -> forall (t_a3Og :: Nat). Sing t_a3Og -> Sing (Max t_a3Of t_a3Og)
- Data.Type.Natural: sMin :: Sing t_a3NC -> forall (t_a3ND :: Nat). Sing t_a3ND -> Sing (Min t_a3NC t_a3ND)
+ Data.Type.Natural: sMin :: Sing t_a3Od -> forall (t_a3Oe :: Nat). Sing t_a3Oe -> Sing (Min t_a3Od t_a3Oe)
- Data.Type.Natural: sS :: Sing n_a3wY -> Sing (S n_a3wY)
+ Data.Type.Natural: sS :: Sing n_a3xz -> Sing (S n_a3xz)
- Data.Type.Natural: type SNat (a_a3wX :: Nat) = Sing a_a3wX
+ Data.Type.Natural: type SNat (a_a3xy :: Nat) = Sing a_a3xy

Files

Data/Type/Natural.hs view
@@ -45,11 +45,13 @@                     , sN15, sN16, sN17, sN18, sN19, sN20                     ) where import           Data.Singletons-import           Prelude          (Bool (..), Eq (..), Integral (..), Ord ((<)),+import           Data.Type.Monomorphic+import           Prelude          (Int, Bool (..), Eq (..), Integral (..), Ord ((<)),                                    Show (..), error, id, otherwise, ($), (.), undefined) import qualified Prelude          as P import           Proof.Equational + -------------------------------------------------- -- * Natural numbers and its singleton type --------------------------------------------------@@ -627,3 +629,11 @@ sNatToInt :: P.Num n => SNat x -> n sNatToInt SZ     = 0 sNatToInt (SS n) = sNatToInt n P.+ 1++instance Monomorphicable (Sing :: Nat -> *) where+  type MonomorphicRep (Sing :: Nat -> *) = Int+  demote  (Monomorphic sn) = sNatToInt sn+  promote n+      | n < 0     = error "negative integer!"+      | n == 0    = Monomorphic sZ+      | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.0.1.1+version:             0.0.2.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@@ -22,6 +22,7 @@ library   exposed-modules:     Data.Type.Natural   -- other-modules:       -  build-depends:       base                     ==4.6.*-               ,       singletons               ==0.8.*+  build-depends:       base                     == 4.6.*+               ,       singletons               == 0.8.*                ,       equational-reasoning     == 0.0.*+               ,       monomorphic              >= 0.0.3