type-natural 0.2.3.1 → 0.2.3.2
raw patch · 3 files changed
+14/−2 lines, 3 filesdep ~singletonsPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: singletons
API changes (from Hackage documentation)
- Data.Type.Natural: instance Eq (Sing Nat n)
- Data.Type.Natural: instance Monomorphicable Nat (Sing Nat)
- Data.Type.Natural: instance Preorder Nat Leq
- Data.Type.Natural: instance Show (Sing Nat n)
- Data.Type.Ordinal: instance SingI Nat n => Bounded (Ordinal ('S n))
- Data.Type.Ordinal: instance SingI Nat n => Enum (Ordinal n)
- Data.Type.Ordinal: instance SingI Nat n => Num (Ordinal n)
+ Data.Type.Natural: (%**) :: SNat n -> SNat m -> SNat (n :**: m)
+ Data.Type.Natural: (%:**) :: Sing t_acSr -> Sing t_acSs -> Sing (Apply (Apply (:**$) t_acSr) t_acSs)
+ Data.Type.Natural: data (:<<=$$) (l_adQc :: Nat) (l_adQb :: TyFun Nat Bool)
+ Data.Type.Natural: data MaxSym0 (l_acqh :: TyFun Nat (TyFun Nat Nat -> *))
+ Data.Type.Natural: data MaxSym1 (l_acqk :: Nat) (l_acqj :: TyFun Nat Nat)
+ Data.Type.Natural: data MinSym0 (l_acqu :: TyFun Nat (TyFun Nat Nat -> *))
+ Data.Type.Natural: data MinSym1 (l_acqx :: Nat) (l_acqw :: TyFun Nat Nat)
+ Data.Type.Natural: data SSym0 (l_abVi :: TyFun Nat Nat)
+ Data.Type.Natural: instance Eq (Sing n)
+ Data.Type.Natural: instance Monomorphicable Sing
+ Data.Type.Natural: instance Preorder Leq
+ Data.Type.Natural: instance Show (Sing n)
+ Data.Type.Natural: type EightSym0 = Eight
+ Data.Type.Natural: type EighteenSym0 = Eighteen
+ Data.Type.Natural: type ElevenSym0 = Eleven
+ Data.Type.Natural: type FifteenSym0 = Fifteen
+ Data.Type.Natural: type FiveSym0 = Five
+ Data.Type.Natural: type FourSym0 = Four
+ Data.Type.Natural: type FourteenSym0 = Fourteen
+ Data.Type.Natural: type MaxSym2 (t_acqf :: Nat) (t_acqg :: Nat) = Max t_acqf t_acqg
+ Data.Type.Natural: type MinSym2 (t_acqs :: Nat) (t_acqt :: Nat) = Min t_acqs t_acqt
+ Data.Type.Natural: type N0Sym0 = N0
+ Data.Type.Natural: type N10Sym0 = N10
+ Data.Type.Natural: type N11Sym0 = N11
+ Data.Type.Natural: type N12Sym0 = N12
+ Data.Type.Natural: type N13Sym0 = N13
+ Data.Type.Natural: type N14Sym0 = N14
+ Data.Type.Natural: type N15Sym0 = N15
+ Data.Type.Natural: type N16Sym0 = N16
+ Data.Type.Natural: type N17Sym0 = N17
+ Data.Type.Natural: type N18Sym0 = N18
+ Data.Type.Natural: type N19Sym0 = N19
+ Data.Type.Natural: type N1Sym0 = N1
+ Data.Type.Natural: type N20Sym0 = N20
+ Data.Type.Natural: type N2Sym0 = N2
+ Data.Type.Natural: type N3Sym0 = N3
+ Data.Type.Natural: type N4Sym0 = N4
+ Data.Type.Natural: type N5Sym0 = N5
+ Data.Type.Natural: type N6Sym0 = N6
+ Data.Type.Natural: type N7Sym0 = N7
+ Data.Type.Natural: type N8Sym0 = N8
+ Data.Type.Natural: type N9Sym0 = N9
+ Data.Type.Natural: type NineSym0 = Nine
+ Data.Type.Natural: type NineteenSym0 = Nineteen
+ Data.Type.Natural: type OneSym0 = One
+ Data.Type.Natural: type SSym1 (t_abVh :: Nat) = S t_abVh
+ Data.Type.Natural: type SevenSym0 = Seven
+ Data.Type.Natural: type SeventeenSym0 = Seventeen
+ Data.Type.Natural: type SixSym0 = Six
+ Data.Type.Natural: type SixteenSym0 = Sixteen
+ Data.Type.Natural: type TenSym0 = Ten
+ Data.Type.Natural: type ThirteenSym0 = Thirteen
+ Data.Type.Natural: type ThreeSym0 = Three
+ Data.Type.Natural: type TwelveSym0 = Twelve
+ Data.Type.Natural: type TwentySym0 = Twenty
+ Data.Type.Natural: type TwoSym0 = Two
+ Data.Type.Natural: type ZSym0 = Z
+ Data.Type.Natural: type ZeroSym0 = Zero
+ Data.Type.Ordinal: instance SingI n => Bounded (Ordinal ('S n))
+ Data.Type.Ordinal: instance SingI n => Enum (Ordinal n)
+ Data.Type.Ordinal: instance SingI n => Num (Ordinal n)
+ Data.Type.Ordinal: instance Typeable Ordinal
- Data.Type.Natural: (%:*) :: Sing t_a3UH -> Sing t_a3UI -> Sing (:* t_a3UH t_a3UI)
+ Data.Type.Natural: (%:*) :: Sing t_acSp -> Sing t_acSq -> Sing (Apply (Apply (:*$) t_acSp) t_acSq)
- Data.Type.Natural: (%:+) :: Sing t_a3UD -> Sing t_a3UE -> Sing (:+ t_a3UD t_a3UE)
+ Data.Type.Natural: (%:+) :: Sing t_acSn -> Sing t_acSo -> Sing (Apply (Apply (:+$) t_acSn) t_acSo)
- Data.Type.Natural: (%:-) :: Sing t_a3UF -> Sing t_a3UG -> Sing (:- t_a3UF t_a3UG)
+ Data.Type.Natural: (%:-) :: Sing t_acSl -> Sing t_acSm -> Sing (Apply (Apply (:-$) t_acSl) t_acSm)
- Data.Type.Natural: (%:<<=) :: Sing t_a4uW -> Sing t_a4uX -> Sing (:<<= t_a4uW t_a4uX)
+ Data.Type.Natural: (%:<<=) :: Sing t_adQk -> Sing t_adQl -> Sing (Apply (Apply (:<<=$) t_adQk) t_adQl)
- Data.Type.Natural: sEight :: Sing Eight
+ Data.Type.Natural: sEight :: Sing EightSym0
- Data.Type.Natural: sEighteen :: Sing Eighteen
+ Data.Type.Natural: sEighteen :: Sing EighteenSym0
- Data.Type.Natural: sEleven :: Sing Eleven
+ Data.Type.Natural: sEleven :: Sing ElevenSym0
- Data.Type.Natural: sFifteen :: Sing Fifteen
+ Data.Type.Natural: sFifteen :: Sing FifteenSym0
- Data.Type.Natural: sFive :: Sing Five
+ Data.Type.Natural: sFive :: Sing FiveSym0
- Data.Type.Natural: sFour :: Sing Four
+ Data.Type.Natural: sFour :: Sing FourSym0
- Data.Type.Natural: sFourteen :: Sing Fourteen
+ Data.Type.Natural: sFourteen :: Sing FourteenSym0
- Data.Type.Natural: sMax :: Sing t_a3Jj -> Sing t_a3Jk -> Sing (Max t_a3Jj t_a3Jk)
+ Data.Type.Natural: sMax :: Sing t_acqF -> Sing t_acqG -> Sing (Apply (Apply MaxSym0 t_acqF) t_acqG)
- Data.Type.Natural: sMin :: Sing t_a3Jh -> Sing t_a3Ji -> Sing (Min t_a3Jh t_a3Ji)
+ Data.Type.Natural: sMin :: Sing t_acqH -> Sing t_acqI -> Sing (Apply (Apply MinSym0 t_acqH) t_acqI)
- Data.Type.Natural: sN0 :: Sing N0
+ Data.Type.Natural: sN0 :: Sing N0Sym0
- Data.Type.Natural: sN1 :: Sing N1
+ Data.Type.Natural: sN1 :: Sing N1Sym0
- Data.Type.Natural: sN10 :: Sing N10
+ Data.Type.Natural: sN10 :: Sing N10Sym0
- Data.Type.Natural: sN11 :: Sing N11
+ Data.Type.Natural: sN11 :: Sing N11Sym0
- Data.Type.Natural: sN12 :: Sing N12
+ Data.Type.Natural: sN12 :: Sing N12Sym0
- Data.Type.Natural: sN13 :: Sing N13
+ Data.Type.Natural: sN13 :: Sing N13Sym0
- Data.Type.Natural: sN14 :: Sing N14
+ Data.Type.Natural: sN14 :: Sing N14Sym0
- Data.Type.Natural: sN15 :: Sing N15
+ Data.Type.Natural: sN15 :: Sing N15Sym0
- Data.Type.Natural: sN16 :: Sing N16
+ Data.Type.Natural: sN16 :: Sing N16Sym0
- Data.Type.Natural: sN17 :: Sing N17
+ Data.Type.Natural: sN17 :: Sing N17Sym0
- Data.Type.Natural: sN18 :: Sing N18
+ Data.Type.Natural: sN18 :: Sing N18Sym0
- Data.Type.Natural: sN19 :: Sing N19
+ Data.Type.Natural: sN19 :: Sing N19Sym0
- Data.Type.Natural: sN2 :: Sing N2
+ Data.Type.Natural: sN2 :: Sing N2Sym0
- Data.Type.Natural: sN20 :: Sing N20
+ Data.Type.Natural: sN20 :: Sing N20Sym0
- Data.Type.Natural: sN3 :: Sing N3
+ Data.Type.Natural: sN3 :: Sing N3Sym0
- Data.Type.Natural: sN4 :: Sing N4
+ Data.Type.Natural: sN4 :: Sing N4Sym0
- Data.Type.Natural: sN5 :: Sing N5
+ Data.Type.Natural: sN5 :: Sing N5Sym0
- Data.Type.Natural: sN6 :: Sing N6
+ Data.Type.Natural: sN6 :: Sing N6Sym0
- Data.Type.Natural: sN7 :: Sing N7
+ Data.Type.Natural: sN7 :: Sing N7Sym0
- Data.Type.Natural: sN8 :: Sing N8
+ Data.Type.Natural: sN8 :: Sing N8Sym0
- Data.Type.Natural: sN9 :: Sing N9
+ Data.Type.Natural: sN9 :: Sing N9Sym0
- Data.Type.Natural: sNine :: Sing Nine
+ Data.Type.Natural: sNine :: Sing NineSym0
- Data.Type.Natural: sNineteen :: Sing Nineteen
+ Data.Type.Natural: sNineteen :: Sing NineteenSym0
- Data.Type.Natural: sOne :: Sing One
+ Data.Type.Natural: sOne :: Sing OneSym0
- Data.Type.Natural: sS :: Sing n_a3sR -> Sing (S n_a3sR)
+ Data.Type.Natural: sS :: SNat n -> SNat (S n)
- Data.Type.Natural: sSeven :: Sing Seven
+ Data.Type.Natural: sSeven :: Sing SevenSym0
- Data.Type.Natural: sSeventeen :: Sing Seventeen
+ Data.Type.Natural: sSeventeen :: Sing SeventeenSym0
- Data.Type.Natural: sSix :: Sing Six
+ Data.Type.Natural: sSix :: Sing SixSym0
- Data.Type.Natural: sSixteen :: Sing Sixteen
+ Data.Type.Natural: sSixteen :: Sing SixteenSym0
- Data.Type.Natural: sTen :: Sing Ten
+ Data.Type.Natural: sTen :: Sing TenSym0
- Data.Type.Natural: sThirteen :: Sing Thirteen
+ Data.Type.Natural: sThirteen :: Sing ThirteenSym0
- Data.Type.Natural: sThree :: Sing Three
+ Data.Type.Natural: sThree :: Sing ThreeSym0
- Data.Type.Natural: sTwelve :: Sing Twelve
+ Data.Type.Natural: sTwelve :: Sing TwelveSym0
- Data.Type.Natural: sTwenty :: Sing Twenty
+ Data.Type.Natural: sTwenty :: Sing TwentySym0
- Data.Type.Natural: sTwo :: Sing Two
+ Data.Type.Natural: sTwo :: Sing TwoSym0
- Data.Type.Natural: sZ :: Sing Z
+ Data.Type.Natural: sZ :: SNat Z
- Data.Type.Natural: sZero :: Sing Zero
+ Data.Type.Natural: sZero :: Sing ZeroSym0
- Data.Type.Natural: type (:-:) n m = n :- m
+ Data.Type.Natural: type (:<<=$$$) (t_adQ7 :: Nat) (t_adQ8 :: Nat) = (:<<=) t_adQ7 t_adQ8
- Data.Type.Natural: type Eight = S Seven
+ Data.Type.Natural: type Eight = (Apply SSym0 SevenSym0 :: Nat)
- Data.Type.Natural: type Eighteen = S Seventeen
+ Data.Type.Natural: type Eighteen = (Apply SSym0 SeventeenSym0 :: Nat)
- Data.Type.Natural: type Eleven = S Ten
+ Data.Type.Natural: type Eleven = (Apply SSym0 TenSym0 :: Nat)
- Data.Type.Natural: type Fifteen = S Fourteen
+ Data.Type.Natural: type Fifteen = (Apply SSym0 FourteenSym0 :: Nat)
- Data.Type.Natural: type Five = S Four
+ Data.Type.Natural: type Five = (Apply SSym0 FourSym0 :: Nat)
- Data.Type.Natural: type Four = S Three
+ Data.Type.Natural: type Four = (Apply SSym0 ThreeSym0 :: Nat)
- Data.Type.Natural: type Fourteen = S Thirteen
+ Data.Type.Natural: type Fourteen = (Apply SSym0 ThirteenSym0 :: Nat)
- Data.Type.Natural: type N0 = Zero
+ Data.Type.Natural: type N0 = (ZeroSym0 :: Nat)
- Data.Type.Natural: type N1 = One
+ Data.Type.Natural: type N1 = (OneSym0 :: Nat)
- Data.Type.Natural: type N10 = Ten
+ Data.Type.Natural: type N10 = (TenSym0 :: Nat)
- Data.Type.Natural: type N11 = Eleven
+ Data.Type.Natural: type N11 = (ElevenSym0 :: Nat)
- Data.Type.Natural: type N12 = Twelve
+ Data.Type.Natural: type N12 = (TwelveSym0 :: Nat)
- Data.Type.Natural: type N13 = Thirteen
+ Data.Type.Natural: type N13 = (ThirteenSym0 :: Nat)
- Data.Type.Natural: type N14 = Fourteen
+ Data.Type.Natural: type N14 = (FourteenSym0 :: Nat)
- Data.Type.Natural: type N15 = Fifteen
+ Data.Type.Natural: type N15 = (FifteenSym0 :: Nat)
- Data.Type.Natural: type N16 = Sixteen
+ Data.Type.Natural: type N16 = (SixteenSym0 :: Nat)
- Data.Type.Natural: type N17 = Seventeen
+ Data.Type.Natural: type N17 = (SeventeenSym0 :: Nat)
- Data.Type.Natural: type N18 = Eighteen
+ Data.Type.Natural: type N18 = (EighteenSym0 :: Nat)
- Data.Type.Natural: type N19 = Nineteen
+ Data.Type.Natural: type N19 = (NineteenSym0 :: Nat)
- Data.Type.Natural: type N2 = Two
+ Data.Type.Natural: type N2 = (TwoSym0 :: Nat)
- Data.Type.Natural: type N20 = Twenty
+ Data.Type.Natural: type N20 = (TwentySym0 :: Nat)
- Data.Type.Natural: type N3 = Three
+ Data.Type.Natural: type N3 = (ThreeSym0 :: Nat)
- Data.Type.Natural: type N4 = Four
+ Data.Type.Natural: type N4 = (FourSym0 :: Nat)
- Data.Type.Natural: type N5 = Five
+ Data.Type.Natural: type N5 = (FiveSym0 :: Nat)
- Data.Type.Natural: type N6 = Six
+ Data.Type.Natural: type N6 = (SixSym0 :: Nat)
- Data.Type.Natural: type N7 = Seven
+ Data.Type.Natural: type N7 = (SevenSym0 :: Nat)
- Data.Type.Natural: type N8 = Eight
+ Data.Type.Natural: type N8 = (EightSym0 :: Nat)
- Data.Type.Natural: type N9 = Nine
+ Data.Type.Natural: type N9 = (NineSym0 :: Nat)
- Data.Type.Natural: type Nine = S Eight
+ Data.Type.Natural: type Nine = (Apply SSym0 EightSym0 :: Nat)
- Data.Type.Natural: type Nineteen = S Eighteen
+ Data.Type.Natural: type Nineteen = (Apply SSym0 EighteenSym0 :: Nat)
- Data.Type.Natural: type One = S Zero
+ Data.Type.Natural: type One = (Apply SSym0 ZeroSym0 :: Nat)
- Data.Type.Natural: type SNat (a_a3sQ :: Nat) = Sing a_a3sQ
+ Data.Type.Natural: type SNat (z_abVk :: Nat) = Sing z_abVk
- Data.Type.Natural: type Seven = S Six
+ Data.Type.Natural: type Seven = (Apply SSym0 SixSym0 :: Nat)
- Data.Type.Natural: type Seventeen = S Sixteen
+ Data.Type.Natural: type Seventeen = (Apply SSym0 SixteenSym0 :: Nat)
- Data.Type.Natural: type Six = S Five
+ Data.Type.Natural: type Six = (Apply SSym0 FiveSym0 :: Nat)
- Data.Type.Natural: type Sixteen = S Fifteen
+ Data.Type.Natural: type Sixteen = (Apply SSym0 FifteenSym0 :: Nat)
- Data.Type.Natural: type Ten = S Nine
+ Data.Type.Natural: type Ten = (Apply SSym0 NineSym0 :: Nat)
- Data.Type.Natural: type Thirteen = S Twelve
+ Data.Type.Natural: type Thirteen = (Apply SSym0 TwelveSym0 :: Nat)
- Data.Type.Natural: type Three = S Two
+ Data.Type.Natural: type Three = (Apply SSym0 TwoSym0 :: Nat)
- Data.Type.Natural: type Twelve = S Eleven
+ Data.Type.Natural: type Twelve = (Apply SSym0 ElevenSym0 :: Nat)
- Data.Type.Natural: type Twenty = S Nineteen
+ Data.Type.Natural: type Twenty = (Apply SSym0 NineteenSym0 :: Nat)
- Data.Type.Natural: type Two = S One
+ Data.Type.Natural: type Two = (Apply SSym0 OneSym0 :: Nat)
- Data.Type.Natural: type Zero = Z
+ Data.Type.Natural: type Zero = (ZSym0 :: Nat)
Files
- Data/Type/Natural.hs +1/−0
- Data/Type/Natural/Definitions.hs +11/−0
- type-natural.cabal +2/−2
Data/Type/Natural.hs view
@@ -32,6 +32,7 @@ (:*$), (:*$$), (:*$$$), #endif (%:*), (%*), (:-:), (:-),+ (:**:), (:**), (%:**), (%**), #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 (:-$), (:-$$), (:-$$$), #endif
Data/Type/Natural/Definitions.hs view
@@ -69,6 +69,10 @@ (*) :: Nat -> Nat -> Nat Z * _ = Z S n * m = n * m + m++ (**) :: Nat -> Nat -> Nat+ n ** Z = S Z+ n ** S m = (n ** m) * n |] infixl 6 :-:, %:-, -@@ -90,6 +94,13 @@ -- | Multiplication for singleton numbers. (%*) :: SNat n -> SNat m -> SNat (n :*: m) (%*) = (%:*)++-- | Type-level exponentiation.+type n :**: m = n :** m++-- | Exponentiation for singleton numbers.+(%**) :: SNat n -> SNat m -> SNat (n :**: m)+(%**) = (%:**) singletons [d| zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.2.3.1+version: 0.2.3.2 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@@ -30,4 +30,4 @@ if impl(ghc < 7.8) build-depends: singletons == 0.8.* else- build-depends: singletons >= 1.0 && < 1.1+ build-depends: singletons >= 1.0 && < 1.2