type-natural 0.4.1.0 → 0.4.1.1
raw patch · 2 files changed
+4/−4 lines, 2 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Data.Type.Natural: (%:**) :: forall (t_anAC :: Nat) (t_anAD :: Nat). Sing t_anAC -> Sing t_anAD -> Sing (Apply (Apply (:**$) t_anAC) t_anAD :: Nat)
+ Data.Type.Natural: (%:**) :: forall (t_am3F :: Nat) (t_am3G :: Nat). Sing t_am3F -> Sing t_am3G -> Sing (Apply (Apply (:**$) t_am3F) t_am3G :: Nat)
- Data.Type.Natural: (%:<<=) :: forall (t_aogo :: Nat) (t_aogp :: Nat). Sing t_aogo -> Sing t_aogp -> Sing (Apply (Apply (:<<=$) t_aogo) t_aogp :: Bool)
+ Data.Type.Natural: (%:<<=) :: forall (t_amJq :: Nat) (t_amJr :: Nat). Sing t_amJq -> Sing t_amJr -> Sing (Apply (Apply (:<<=$) t_amJq) t_amJr :: Bool)
- Data.Type.Natural: data (:<<=$$) (l_aogc :: Nat) (l_aogb :: TyFun Nat Bool)
+ Data.Type.Natural: data (:<<=$$) (l_amJe :: Nat) (l_amJd :: TyFun Nat Bool)
- Data.Type.Natural: data MaxSym0 a1627675388 (l0 :: TyFun a1627675388 (TyFun a1627675388 a1627675388 -> Type)) :: forall a1627675388. TyFun a1627675388 (TyFun a1627675388 a1627675388 -> Type) -> *
+ Data.Type.Natural: data MaxSym0 a1627685414 (l0 :: TyFun a1627685414 (TyFun a1627685414 a1627685414 -> Type)) :: forall a1627685414. TyFun a1627685414 (TyFun a1627685414 a1627685414 -> Type) -> *
- Data.Type.Natural: data MaxSym1 a1627675388 (l0 :: a1627675388) (l1 :: TyFun a1627675388 a1627675388) :: forall a1627675388. a1627675388 -> TyFun a1627675388 a1627675388 -> *
+ Data.Type.Natural: data MaxSym1 a1627685414 (l0 :: a1627685414) (l1 :: TyFun a1627685414 a1627685414) :: forall a1627685414. a1627685414 -> TyFun a1627685414 a1627685414 -> *
- Data.Type.Natural: data MinSym0 a1627675388 (l0 :: TyFun a1627675388 (TyFun a1627675388 a1627675388 -> Type)) :: forall a1627675388. TyFun a1627675388 (TyFun a1627675388 a1627675388 -> Type) -> *
+ Data.Type.Natural: data MinSym0 a1627685414 (l0 :: TyFun a1627685414 (TyFun a1627685414 a1627685414 -> Type)) :: forall a1627685414. TyFun a1627685414 (TyFun a1627685414 a1627685414 -> Type) -> *
- Data.Type.Natural: data MinSym1 a1627675388 (l0 :: a1627675388) (l1 :: TyFun a1627675388 a1627675388) :: forall a1627675388. a1627675388 -> TyFun a1627675388 a1627675388 -> *
+ Data.Type.Natural: data MinSym1 a1627685414 (l0 :: a1627685414) (l1 :: TyFun a1627685414 a1627685414) :: forall a1627685414. a1627685414 -> TyFun a1627685414 a1627685414 -> *
- Data.Type.Natural: data SSym0 (l_akiL :: TyFun Nat Nat)
+ Data.Type.Natural: data SSym0 (l_aiSc :: TyFun Nat Nat)
- Data.Type.Natural: type (:<<=$$$) (t_aog7 :: Nat) (t_aog8 :: Nat) = (:<<=) t_aog7 t_aog8
+ Data.Type.Natural: type (:<<=$$$) (t_amJ9 :: Nat) (t_amJa :: Nat) = (:<<=) t_amJ9 t_amJa
- Data.Type.Natural: type MaxSym2 a1627675388 (t0 :: a1627675388) (t1 :: a1627675388) = Max a1627675388 t0 t1
+ Data.Type.Natural: type MaxSym2 a1627685414 (t0 :: a1627685414) (t1 :: a1627685414) = Max a1627685414 t0 t1
- Data.Type.Natural: type MinSym2 a1627675388 (t0 :: a1627675388) (t1 :: a1627675388) = Min a1627675388 t0 t1
+ Data.Type.Natural: type MinSym2 a1627685414 (t0 :: a1627685414) (t1 :: a1627685414) = Min a1627685414 t0 t1
- Data.Type.Natural: type SSym1 (t_akiK :: Nat) = S t_akiK
+ Data.Type.Natural: type SSym1 (t_aiSb :: Nat) = S t_aiSb
Files
- Data/Type/Natural.hs +3/−3
- type-natural.cabal +1/−1
Data/Type/Natural.hs view
@@ -214,7 +214,7 @@ minusCongEq, minusCongL :: n :=: m -> SNat l -> n :-: l :=: m :-: l minusCongL Refl _ = Refl minusCongEq = minusCongL-{-# DEPRECATED minusCongEq "Will be removed in @0.5.0.0@. Use @'minusCongEq'@ instead." #-}+{-# DEPRECATED minusCongEq "Will be removed in @0.5.0.0@. Use @'minusCongL'@ instead." #-} minusNilpotent :: SNat n -> n :-: n :=: Zero minusNilpotent SZ = Refl@@ -310,7 +310,7 @@ =~= (SS n %* l) %+ (SS n %* m) === (SS n %* m) %+ (SS n %* l) `because` plusCommutative (SS n %* l) (SS n %* m) multPlusDistr = multPlusDistrib-{-# DEPRECATED plusMultDistrib "Will be removed in @0.5.0.0@. Use @'plusMultDistirb'@ instead." #-}+{-# DEPRECATED multPlusDistr "Will be removed in @0.5.0.0@. Use @'multPlusDistrib'@ instead." #-} plusMultDistr, plusMultDistrib :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: (n :* l) :+ (m :* l) plusMultDistrib SZ _ _ = Refl@@ -325,7 +325,7 @@ === (SS n %* l) %+ (m %* l) `because` plusCommutative (m %* l) (SS n %* l) plusMultDistr = plusMultDistrib-{-# DEPRECATED multPlusDistrib "Will be removed in @0.5.0.0@. Use @'multPlusDistirb'@ instead." #-}+{-# DEPRECATED plusMultDistr "Will be removed in @0.5.0.0@. Use @'plusMultDistrib'@ instead." #-} multAssoc, multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l multAssoc SZ _ _ = Refl
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.4.1.0+version: 0.4.1.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