type-natural 0.2.3.0 → 0.2.3.1
raw patch · 2 files changed
+14/−5 lines, 2 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Data.Type.Natural: data (:<<=$$) (l_adDD :: Nat) (l_adDC :: TyFun Nat Bool)
- Data.Type.Natural: data MaxSym0 (l_acn5 :: TyFun Nat (TyFun Nat Nat -> *))
- Data.Type.Natural: data MaxSym1 (l_acn8 :: Nat) (l_acn7 :: TyFun Nat Nat)
- Data.Type.Natural: data MinSym0 (l_acni :: TyFun Nat (TyFun Nat Nat -> *))
- Data.Type.Natural: data MinSym1 (l_acnl :: Nat) (l_acnk :: TyFun Nat Nat)
- Data.Type.Natural: data SSym0 (l_abS6 :: 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_acn3 :: Nat) (t_acn4 :: Nat) = Max t_acn3 t_acn4
- Data.Type.Natural: type MinSym2 (t_acng :: Nat) (t_acnh :: Nat) = Min t_acng t_acnh
- 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_abS5 :: Nat) = S t_abS5
- 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: 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: (%:*) :: Sing t_acNt -> Sing t_acNu -> Sing (Apply (Apply (:*$) t_acNt) t_acNu)
+ Data.Type.Natural: (%:*) :: Sing t_a3UH -> Sing t_a3UI -> Sing (:* t_a3UH t_a3UI)
- Data.Type.Natural: (%:+) :: Sing t_acNr -> Sing t_acNs -> Sing (Apply (Apply (:+$) t_acNr) t_acNs)
+ Data.Type.Natural: (%:+) :: Sing t_a3UD -> Sing t_a3UE -> Sing (:+ t_a3UD t_a3UE)
- Data.Type.Natural: (%:-) :: Sing t_acNp -> Sing t_acNq -> Sing (Apply (Apply (:-$) t_acNp) t_acNq)
+ Data.Type.Natural: (%:-) :: Sing t_a3UF -> Sing t_a3UG -> Sing (:- t_a3UF t_a3UG)
- Data.Type.Natural: (%:<<=) :: Sing t_adDL -> Sing t_adDM -> Sing (Apply (Apply (:<<=$) t_adDL) t_adDM)
+ Data.Type.Natural: (%:<<=) :: Sing t_a4uW -> Sing t_a4uX -> Sing (:<<= t_a4uW t_a4uX)
- Data.Type.Natural: sEight :: Sing EightSym0
+ Data.Type.Natural: sEight :: Sing Eight
- Data.Type.Natural: sEighteen :: Sing EighteenSym0
+ Data.Type.Natural: sEighteen :: Sing Eighteen
- Data.Type.Natural: sEleven :: Sing ElevenSym0
+ Data.Type.Natural: sEleven :: Sing Eleven
- Data.Type.Natural: sFifteen :: Sing FifteenSym0
+ Data.Type.Natural: sFifteen :: Sing Fifteen
- Data.Type.Natural: sFive :: Sing FiveSym0
+ Data.Type.Natural: sFive :: Sing Five
- Data.Type.Natural: sFour :: Sing FourSym0
+ Data.Type.Natural: sFour :: Sing Four
- Data.Type.Natural: sFourteen :: Sing FourteenSym0
+ Data.Type.Natural: sFourteen :: Sing Fourteen
- Data.Type.Natural: sMax :: Sing t_acnt -> Sing t_acnu -> Sing (Apply (Apply MaxSym0 t_acnt) t_acnu)
+ Data.Type.Natural: sMax :: Sing t_a3Jj -> Sing t_a3Jk -> Sing (Max t_a3Jj t_a3Jk)
- Data.Type.Natural: sMin :: Sing t_acnv -> Sing t_acnw -> Sing (Apply (Apply MinSym0 t_acnv) t_acnw)
+ Data.Type.Natural: sMin :: Sing t_a3Jh -> Sing t_a3Ji -> Sing (Min t_a3Jh t_a3Ji)
- Data.Type.Natural: sN0 :: Sing N0Sym0
+ Data.Type.Natural: sN0 :: Sing N0
- Data.Type.Natural: sN1 :: Sing N1Sym0
+ Data.Type.Natural: sN1 :: Sing N1
- Data.Type.Natural: sN10 :: Sing N10Sym0
+ Data.Type.Natural: sN10 :: Sing N10
- Data.Type.Natural: sN11 :: Sing N11Sym0
+ Data.Type.Natural: sN11 :: Sing N11
- Data.Type.Natural: sN12 :: Sing N12Sym0
+ Data.Type.Natural: sN12 :: Sing N12
- Data.Type.Natural: sN13 :: Sing N13Sym0
+ Data.Type.Natural: sN13 :: Sing N13
- Data.Type.Natural: sN14 :: Sing N14Sym0
+ Data.Type.Natural: sN14 :: Sing N14
- Data.Type.Natural: sN15 :: Sing N15Sym0
+ Data.Type.Natural: sN15 :: Sing N15
- Data.Type.Natural: sN16 :: Sing N16Sym0
+ Data.Type.Natural: sN16 :: Sing N16
- Data.Type.Natural: sN17 :: Sing N17Sym0
+ Data.Type.Natural: sN17 :: Sing N17
- Data.Type.Natural: sN18 :: Sing N18Sym0
+ Data.Type.Natural: sN18 :: Sing N18
- Data.Type.Natural: sN19 :: Sing N19Sym0
+ Data.Type.Natural: sN19 :: Sing N19
- Data.Type.Natural: sN2 :: Sing N2Sym0
+ Data.Type.Natural: sN2 :: Sing N2
- Data.Type.Natural: sN20 :: Sing N20Sym0
+ Data.Type.Natural: sN20 :: Sing N20
- Data.Type.Natural: sN3 :: Sing N3Sym0
+ Data.Type.Natural: sN3 :: Sing N3
- Data.Type.Natural: sN4 :: Sing N4Sym0
+ Data.Type.Natural: sN4 :: Sing N4
- Data.Type.Natural: sN5 :: Sing N5Sym0
+ Data.Type.Natural: sN5 :: Sing N5
- Data.Type.Natural: sN6 :: Sing N6Sym0
+ Data.Type.Natural: sN6 :: Sing N6
- Data.Type.Natural: sN7 :: Sing N7Sym0
+ Data.Type.Natural: sN7 :: Sing N7
- Data.Type.Natural: sN8 :: Sing N8Sym0
+ Data.Type.Natural: sN8 :: Sing N8
- Data.Type.Natural: sN9 :: Sing N9Sym0
+ Data.Type.Natural: sN9 :: Sing N9
- Data.Type.Natural: sNine :: Sing NineSym0
+ Data.Type.Natural: sNine :: Sing Nine
- Data.Type.Natural: sNineteen :: Sing NineteenSym0
+ Data.Type.Natural: sNineteen :: Sing Nineteen
- Data.Type.Natural: sOne :: Sing OneSym0
+ Data.Type.Natural: sOne :: Sing One
- Data.Type.Natural: sS :: SNat n -> SNat (S n)
+ Data.Type.Natural: sS :: Sing n_a3sR -> Sing (S n_a3sR)
- Data.Type.Natural: sSeven :: Sing SevenSym0
+ Data.Type.Natural: sSeven :: Sing Seven
- Data.Type.Natural: sSeventeen :: Sing SeventeenSym0
+ Data.Type.Natural: sSeventeen :: Sing Seventeen
- Data.Type.Natural: sSix :: Sing SixSym0
+ Data.Type.Natural: sSix :: Sing Six
- Data.Type.Natural: sSixteen :: Sing SixteenSym0
+ Data.Type.Natural: sSixteen :: Sing Sixteen
- Data.Type.Natural: sTen :: Sing TenSym0
+ Data.Type.Natural: sTen :: Sing Ten
- Data.Type.Natural: sThirteen :: Sing ThirteenSym0
+ Data.Type.Natural: sThirteen :: Sing Thirteen
- Data.Type.Natural: sThree :: Sing ThreeSym0
+ Data.Type.Natural: sThree :: Sing Three
- Data.Type.Natural: sTwelve :: Sing TwelveSym0
+ Data.Type.Natural: sTwelve :: Sing Twelve
- Data.Type.Natural: sTwenty :: Sing TwentySym0
+ Data.Type.Natural: sTwenty :: Sing Twenty
- Data.Type.Natural: sTwo :: Sing TwoSym0
+ Data.Type.Natural: sTwo :: Sing Two
- Data.Type.Natural: sZ :: SNat Z
+ Data.Type.Natural: sZ :: Sing Z
- Data.Type.Natural: sZero :: Sing ZeroSym0
+ Data.Type.Natural: sZero :: Sing Zero
- Data.Type.Natural: type (:<<=$$$) (t_adDy :: Nat) (t_adDz :: Nat) = (:<<=) t_adDy t_adDz
+ Data.Type.Natural: type (:-:) n m = n :- m
- Data.Type.Natural: type Eight = (Apply SSym0 SevenSym0 :: Nat)
+ Data.Type.Natural: type Eight = S Seven
- Data.Type.Natural: type Eighteen = (Apply SSym0 SeventeenSym0 :: Nat)
+ Data.Type.Natural: type Eighteen = S Seventeen
- Data.Type.Natural: type Eleven = (Apply SSym0 TenSym0 :: Nat)
+ Data.Type.Natural: type Eleven = S Ten
- Data.Type.Natural: type Fifteen = (Apply SSym0 FourteenSym0 :: Nat)
+ Data.Type.Natural: type Fifteen = S Fourteen
- Data.Type.Natural: type Five = (Apply SSym0 FourSym0 :: Nat)
+ Data.Type.Natural: type Five = S Four
- Data.Type.Natural: type Four = (Apply SSym0 ThreeSym0 :: Nat)
+ Data.Type.Natural: type Four = S Three
- Data.Type.Natural: type Fourteen = (Apply SSym0 ThirteenSym0 :: Nat)
+ Data.Type.Natural: type Fourteen = S Thirteen
- Data.Type.Natural: type N0 = (ZeroSym0 :: Nat)
+ Data.Type.Natural: type N0 = Zero
- Data.Type.Natural: type N1 = (OneSym0 :: Nat)
+ Data.Type.Natural: type N1 = One
- Data.Type.Natural: type N10 = (TenSym0 :: Nat)
+ Data.Type.Natural: type N10 = Ten
- Data.Type.Natural: type N11 = (ElevenSym0 :: Nat)
+ Data.Type.Natural: type N11 = Eleven
- Data.Type.Natural: type N12 = (TwelveSym0 :: Nat)
+ Data.Type.Natural: type N12 = Twelve
- Data.Type.Natural: type N13 = (ThirteenSym0 :: Nat)
+ Data.Type.Natural: type N13 = Thirteen
- Data.Type.Natural: type N14 = (FourteenSym0 :: Nat)
+ Data.Type.Natural: type N14 = Fourteen
- Data.Type.Natural: type N15 = (FifteenSym0 :: Nat)
+ Data.Type.Natural: type N15 = Fifteen
- Data.Type.Natural: type N16 = (SixteenSym0 :: Nat)
+ Data.Type.Natural: type N16 = Sixteen
- Data.Type.Natural: type N17 = (SeventeenSym0 :: Nat)
+ Data.Type.Natural: type N17 = Seventeen
- Data.Type.Natural: type N18 = (EighteenSym0 :: Nat)
+ Data.Type.Natural: type N18 = Eighteen
- Data.Type.Natural: type N19 = (NineteenSym0 :: Nat)
+ Data.Type.Natural: type N19 = Nineteen
- Data.Type.Natural: type N2 = (TwoSym0 :: Nat)
+ Data.Type.Natural: type N2 = Two
- Data.Type.Natural: type N20 = (TwentySym0 :: Nat)
+ Data.Type.Natural: type N20 = Twenty
- Data.Type.Natural: type N3 = (ThreeSym0 :: Nat)
+ Data.Type.Natural: type N3 = Three
- Data.Type.Natural: type N4 = (FourSym0 :: Nat)
+ Data.Type.Natural: type N4 = Four
- Data.Type.Natural: type N5 = (FiveSym0 :: Nat)
+ Data.Type.Natural: type N5 = Five
- Data.Type.Natural: type N6 = (SixSym0 :: Nat)
+ Data.Type.Natural: type N6 = Six
- Data.Type.Natural: type N7 = (SevenSym0 :: Nat)
+ Data.Type.Natural: type N7 = Seven
- Data.Type.Natural: type N8 = (EightSym0 :: Nat)
+ Data.Type.Natural: type N8 = Eight
- Data.Type.Natural: type N9 = (NineSym0 :: Nat)
+ Data.Type.Natural: type N9 = Nine
- Data.Type.Natural: type Nine = (Apply SSym0 EightSym0 :: Nat)
+ Data.Type.Natural: type Nine = S Eight
- Data.Type.Natural: type Nineteen = (Apply SSym0 EighteenSym0 :: Nat)
+ Data.Type.Natural: type Nineteen = S Eighteen
- Data.Type.Natural: type One = (Apply SSym0 ZeroSym0 :: Nat)
+ Data.Type.Natural: type One = S Zero
- Data.Type.Natural: type SNat (z_abS8 :: Nat) = Sing z_abS8
+ Data.Type.Natural: type SNat (a_a3sQ :: Nat) = Sing a_a3sQ
- Data.Type.Natural: type Seven = (Apply SSym0 SixSym0 :: Nat)
+ Data.Type.Natural: type Seven = S Six
- Data.Type.Natural: type Seventeen = (Apply SSym0 SixteenSym0 :: Nat)
+ Data.Type.Natural: type Seventeen = S Sixteen
- Data.Type.Natural: type Six = (Apply SSym0 FiveSym0 :: Nat)
+ Data.Type.Natural: type Six = S Five
- Data.Type.Natural: type Sixteen = (Apply SSym0 FifteenSym0 :: Nat)
+ Data.Type.Natural: type Sixteen = S Fifteen
- Data.Type.Natural: type Ten = (Apply SSym0 NineSym0 :: Nat)
+ Data.Type.Natural: type Ten = S Nine
- Data.Type.Natural: type Thirteen = (Apply SSym0 TwelveSym0 :: Nat)
+ Data.Type.Natural: type Thirteen = S Twelve
- Data.Type.Natural: type Three = (Apply SSym0 TwoSym0 :: Nat)
+ Data.Type.Natural: type Three = S Two
- Data.Type.Natural: type Twelve = (Apply SSym0 ElevenSym0 :: Nat)
+ Data.Type.Natural: type Twelve = S Eleven
- Data.Type.Natural: type Twenty = (Apply SSym0 NineteenSym0 :: Nat)
+ Data.Type.Natural: type Twenty = S Nineteen
- Data.Type.Natural: type Two = (Apply SSym0 OneSym0 :: Nat)
+ Data.Type.Natural: type Two = S One
- Data.Type.Natural: type Zero = (ZSym0 :: Nat)
+ Data.Type.Natural: type Zero = Z
Files
- Data/Type/Ordinal.hs +13/−4
- type-natural.cabal +1/−1
Data/Type/Ordinal.hs view
@@ -97,9 +97,13 @@ unsafeFromInt n = case (promote n :: Monomorphic (Sing :: Nat -> *)) of Monomorphic sn ->- case SS sn %:<<= (sing :: SNat n) of- STrue -> sNatToOrd' (sing :: SNat n) sn- SFalse -> error "Bound over!"+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707+ case singInstance sn of+ SingInstance ->+#endif+ case SS sn %:<<= (sing :: SNat n) of+ STrue -> sNatToOrd' (sing :: SNat n) sn+ SFalse -> error "Bound over!" -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal n@@ -119,7 +123,12 @@ ordToSNat' OZ = CastedOrdinal SZ ordToSNat' (OS on) = case ordToSNat' on of- CastedOrdinal m -> CastedOrdinal (SS m)+ CastedOrdinal m ->+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707 + case singInstance m of+ SingInstance ->+#endif+ CastedOrdinal (SS m) -- | Convert @Ordinal n@ into monomorphic @SNat@ ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.2.3.0+version: 0.2.3.1 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