type-natural 0.7.1.3 → 0.7.1.4
raw patch · 2 files changed
+18/−17 lines, 2 filesdep ~equational-reasoningdep ~ghc-typelits-presburgerdep ~singletonsPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: equational-reasoning, ghc-typelits-presburger, singletons, template-haskell
API changes (from Hackage documentation)
- Data.Type.Natural: (%:**) :: forall (t_ansO :: Nat) (t_ansP :: Nat). Sing t_ansO -> Sing t_ansP -> Sing (Apply (Apply (:**$) t_ansO) t_ansP :: Nat)
+ Data.Type.Natural: (%:**) :: forall (t_anwy :: Nat) (t_anwz :: Nat). Sing t_anwy -> Sing t_anwz -> Sing (Apply (Apply (:**$) t_anwy) t_anwz :: Nat)
- Data.Type.Natural: data (:-$$) a1627805829 (l0 :: a1627805829) (l1 :: TyFun a1627805829 a1627805829) :: forall a1627805829. a1627805829 -> TyFun a1627805829 a1627805829 -> *
+ Data.Type.Natural: data (:-$$) a6989586621679425695 (l0 :: a6989586621679425695) (l1 :: TyFun a6989586621679425695 a6989586621679425695) :: forall a6989586621679425695. a6989586621679425695 -> TyFun a6989586621679425695 a6989586621679425695 -> *
- Data.Type.Natural: data MaxSym0 a1627685643 (l0 :: TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type)) :: forall a1627685643. TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type) -> *
+ Data.Type.Natural: data MaxSym0 a6989586621679305513 (l0 :: TyFun a6989586621679305513 (TyFun a6989586621679305513 a6989586621679305513 -> Type)) :: forall a6989586621679305513. TyFun a6989586621679305513 (TyFun a6989586621679305513 a6989586621679305513 -> Type) -> *
- Data.Type.Natural: data MaxSym1 a1627685643 (l0 :: a1627685643) (l1 :: TyFun a1627685643 a1627685643) :: forall a1627685643. a1627685643 -> TyFun a1627685643 a1627685643 -> *
+ Data.Type.Natural: data MaxSym1 a6989586621679305513 (l0 :: a6989586621679305513) (l1 :: TyFun a6989586621679305513 a6989586621679305513) :: forall a6989586621679305513. a6989586621679305513 -> TyFun a6989586621679305513 a6989586621679305513 -> *
- Data.Type.Natural: data MinSym0 a1627685643 (l0 :: TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type)) :: forall a1627685643. TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type) -> *
+ Data.Type.Natural: data MinSym0 a6989586621679305513 (l0 :: TyFun a6989586621679305513 (TyFun a6989586621679305513 a6989586621679305513 -> Type)) :: forall a6989586621679305513. TyFun a6989586621679305513 (TyFun a6989586621679305513 a6989586621679305513 -> Type) -> *
- Data.Type.Natural: data MinSym1 a1627685643 (l0 :: a1627685643) (l1 :: TyFun a1627685643 a1627685643) :: forall a1627685643. a1627685643 -> TyFun a1627685643 a1627685643 -> *
+ Data.Type.Natural: data MinSym1 a6989586621679305513 (l0 :: a6989586621679305513) (l1 :: TyFun a6989586621679305513 a6989586621679305513) :: forall a6989586621679305513. a6989586621679305513 -> TyFun a6989586621679305513 a6989586621679305513 -> *
- Data.Type.Natural: data SSym0 (l_ajsn :: TyFun Nat Nat)
+ Data.Type.Natural: data SSym0 (l_ajw7 :: TyFun Nat Nat)
- Data.Type.Natural: type (:-$$$) a1627805829 (t0 :: a1627805829) (t1 :: a1627805829) = (:-) a1627805829 t0 t1
+ Data.Type.Natural: type (:-$$$) a6989586621679425695 (t0 :: a6989586621679425695) (t1 :: a6989586621679425695) = (:-) a6989586621679425695 t0 t1
- Data.Type.Natural: type MaxSym2 a1627685643 (t0 :: a1627685643) (t1 :: a1627685643) = Max a1627685643 t0 t1
+ Data.Type.Natural: type MaxSym2 a6989586621679305513 (t0 :: a6989586621679305513) (t1 :: a6989586621679305513) = Max a6989586621679305513 t0 t1
- Data.Type.Natural: type MinSym2 a1627685643 (t0 :: a1627685643) (t1 :: a1627685643) = Min a1627685643 t0 t1
+ Data.Type.Natural: type MinSym2 a6989586621679305513 (t0 :: a6989586621679305513) (t1 :: a6989586621679305513) = Min a6989586621679305513 t0 t1
- Data.Type.Natural: type SSym1 (t_ajsm :: Nat) = S t_ajsm
+ Data.Type.Natural: type SSym1 (t_ajw6 :: Nat) = S t_ajw6
- Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_aTpR :: Ordering). Sing t_aTpR -> Sing (Apply FlipOrderingSym0 t_aTpR :: Ordering)
+ Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_aTvV :: Ordering). Sing t_aTvV -> Sing (Apply FlipOrderingSym0 t_aTvV :: Ordering)
Files
- Data/Type/Natural/Builtin.hs +10/−9
- type-natural.cabal +8/−8
Data/Type/Natural/Builtin.hs view
@@ -32,7 +32,7 @@ import Data.Singletons.Decide (SDecide (..)) import Data.Singletons.Decide (Decision (..))-import Data.Singletons.Prelude (SNum (..), PNum(..), Sing (..))+import Data.Singletons.Prelude (PNum (..), SNum (..), Sing (..)) import Data.Singletons.Prelude (SingI (..)) import Data.Singletons.Prelude (SingKind (..), SomeSing (..)) import Data.Singletons.Prelude.Enum (PEnum (..), SEnum (..))@@ -52,7 +52,8 @@ import Proof.Equational (coerce, withRefl) import Proof.Equational (start, sym, (===), (=~=)) import Proof.Equational (because)-import Proof.Propositional (Empty (..), IsTrue (..), withWitness)+import Proof.Propositional (Empty (..), IsTrue (..),+ withEmpty, withWitness) import Unsafe.Coerce (unsafeCoerce) -- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@.@@ -69,11 +70,11 @@ viewNat :: Sing (n :: TL.Nat) -> ZeroOrSucc n viewNat n = case n %~ (sing :: Sing 0) of- Proved _ -> IsZero- Disproved _ -> IsSucc (sPred n)+ Proved Refl -> IsZero+ Disproved t -> withEmpty t $ IsSucc (sPred n) sFromPeano :: Sing n -> Sing (FromPeano n)-sFromPeano SZ = sing+sFromPeano SZ = sing sFromPeano (SS sn) = sSucc (sFromPeano sn) toPeanoInjective :: ToPeano n :~: ToPeano m -> n :~: m@@ -250,9 +251,9 @@ natSuccPred _ = Refl myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :~: (n :<= m)-myLeqPred SZ _ = Refl+myLeqPred SZ _ = Refl myLeqPred (SS _) (SS _) = Refl-myLeqPred (SS _) SZ = Refl+myLeqPred (SS _) SZ = Refl toPeanoCong :: a :~: b -> ToPeano a :~: ToPeano b toPeanoCong Refl = Refl@@ -281,7 +282,7 @@ inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n inductionNat base step sn = case viewNat sn of- IsZero -> base+ IsZero -> base IsSucc sl -> step (inductionNat base step sl) @@ -291,7 +292,7 @@ plusMinus _ _ = Refl succInj Refl = Refl succOneCong = Refl- succNonCyclic _ a = case a of { }+ succNonCyclic _ a = case a of _ -> error "Bug in GHC!" plusZeroR _ = Refl plusZeroL _ = Refl plusSuccL _ _ = Refl
type-natural.cabal view
@@ -1,5 +1,5 @@ name: type-natural-version: 0.7.1.3+version: 0.7.1.4 cabal-version: >=1.10 build-type: Simple license: BSD3@@ -16,7 +16,7 @@ __Use 0.5.* with ~ GHC 7.10.3__. category: Math author: Hiromi ISHII-tested-with: GHC ==7.10.3+tested-with: GHC ==8.0.2 GHC ==8.2.2 source-repository head type: git@@ -36,14 +36,14 @@ Data.Type.Natural.Class.Arithmetic Data.Type.Natural.Class.Order build-depends:- base ==4.*,- equational-reasoning >=0.4.1.1 && <1,+ base >=4 && <4.10,+ equational-reasoning >=0.4.1.1 && <0.6, monomorphic >=0.0.3 && <0.1,- template-haskell >=2.8 && <3,- constraints >=0.3 && <0.9,+ template-haskell >=2.8 && <2.12,+ constraints >=0.3 && <0.10, ghc-typelits-natnormalise >=0.4 && <0.6,- ghc-typelits-presburger >=0.1.1 && <1,- singletons ==2.2.*+ ghc-typelits-presburger >=0.1.1 && <0.2,+ singletons >=2.2 && <2.4 default-language: Haskell2010 default-extensions: DataKinds PolyKinds ConstraintKinds GADTs ScopedTypeVariables TemplateHaskell TypeFamilies TypeOperators