type-natural 0.7.1.1 → 0.7.1.2
raw patch · 2 files changed
+53/−60 lines, 2 filesdep ~ghc-typelits-natnormalisedep ~monomorphicPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: ghc-typelits-natnormalise, monomorphic
API changes (from Hackage documentation)
- Data.Type.Natural: (%:**) :: forall (t_aYb2 :: Nat) (t_aYb3 :: Nat). Sing t_aYb2 -> Sing t_aYb3 -> Sing (Apply (Apply (:**$) t_aYb2) t_aYb3 :: Nat)
+ Data.Type.Natural: (%:**) :: forall (t_anog :: Nat) (t_anoh :: Nat). Sing t_anog -> Sing t_anoh -> Sing (Apply (Apply (:**$) t_anog) t_anoh :: Nat)
- Data.Type.Natural: data (:-$$) a1627810386 (l0 :: a1627810386) (l1 :: TyFun a1627810386 a1627810386) :: forall a1627810386. a1627810386 -> TyFun a1627810386 a1627810386 -> *
+ Data.Type.Natural: data (:-$$) a1627805586 (l0 :: a1627805586) (l1 :: TyFun a1627805586 a1627805586) :: forall a1627805586. a1627805586 -> TyFun a1627805586 a1627805586 -> *
- 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_aVl8 :: TyFun Nat Nat)
+ Data.Type.Natural: data SSym0 (l_ajnP :: TyFun Nat Nat)
- Data.Type.Natural: type (:-$$$) a1627810386 (t0 :: a1627810386) (t1 :: a1627810386) = (:-) a1627810386 t0 t1
+ Data.Type.Natural: type (:-$$$) a1627805586 (t0 :: a1627805586) (t1 :: a1627805586) = (:-) a1627805586 t0 t1
- 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_aVl7 :: Nat) = S t_aVl7
+ Data.Type.Natural: type SSym1 (t_ajnO :: Nat) = S t_ajnO
- Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_azMn :: Ordering). Sing t_azMn -> Sing (Apply FlipOrderingSym0 t_azMn :: Ordering)
+ Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_aTjn :: Ordering). Sing t_aTjn -> Sing (Apply FlipOrderingSym0 t_aTjn :: Ordering)
Files
- Data/Type/Natural/Builtin.hs +1/−1
- type-natural.cabal +52/−59
Data/Type/Natural/Builtin.hs view
@@ -263,7 +263,7 @@ case sn %~ (sing :: Sing 0) of Proved eql -> withRefl eql Refl Disproved nPos -> case sm %~ (sing :: Sing 0) of- Proved _ -> absurd $ nPos $ natLeqZero sn+ Proved mEq0 -> withRefl mEq0 $ absurd $ nPos $ natLeqZero sn Disproved mPos -> let pn = sPred sn pm = sPred sm
type-natural.cabal view
@@ -1,64 +1,57 @@--- Initial type-natural.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/--name: type-natural-version: 0.7.1.1-synopsis: Type-level natural and proofs of their properties.-description: Type-level natural numbers and proofs of their properties.- .- Version 0.6+ supports __GHC 8+ only__.- .- __Use 0.5.* with ~ GHC 7.10.3__.-homepage: https://github.com/konn/type-natural-license: BSD3-license-file: LICENSE-author: Hiromi ISHII-maintainer: konn.jinro_at_gmail.com-copyright: (C) Hiromi ISHII 2013-2014-category: Math-build-type: Simple-cabal-version: >= 1.10-tested-with: GHC == 7.10.3+name: type-natural+version: 0.7.1.2+cabal-version: >=1.10+build-type: Simple+license: BSD3+license-file: LICENSE+copyright: (C) Hiromi ISHII 2013-2014+maintainer: konn.jinro_at_gmail.com+homepage: https://github.com/konn/type-natural+synopsis: Type-level natural and proofs of their properties.+description:+ Type-level natural numbers and proofs of their properties.+ .+ Version 0.6+ supports __GHC 8+ only__.+ .+ __Use 0.5.* with ~ GHC 7.10.3__.+category: Math+author: Hiromi ISHII+tested-with: GHC ==7.10.3 source-repository head- Type: git- Location: git://github.com/konn/type-natural.git-+ type: git+ location: git://github.com/konn/type-natural.git library- ghc-options: -Wall -O2 -fno-warn-orphans- if impl(ghc >= 8.0.0)- ghc-options: -Wno-redundant-constraints- exposed-modules: Data.Type.Natural- , Data.Type.Ordinal- , Data.Type.Ordinal.Builtin- , Data.Type.Ordinal.Peano- , Data.Type.Natural.Builtin- , Data.Type.Natural.Class- , Data.Type.Natural.Class.Arithmetic- , Data.Type.Natural.Class.Order- other-modules: Data.Type.Natural.Definitions- , Data.Type.Natural.Core- , Data.Type.Natural.Compat- build-depends: base >= 4 && < 5- , equational-reasoning >= 0.4.1.1 && < 1- , monomorphic >= 0.0.3- , template-haskell >= 2.8 && < 3- , constraints >= 0.3 && < 0.9- , ghc-typelits-natnormalise == 0.4.*- , ghc-typelits-presburger >= 0.1.1 && < 1- , singletons == 2.2.*+ + if impl(ghc >=8.0.0)+ ghc-options: -Wno-redundant-constraints+ exposed-modules:+ Data.Type.Natural+ Data.Type.Ordinal+ Data.Type.Ordinal.Builtin+ Data.Type.Ordinal.Peano+ Data.Type.Natural.Builtin+ Data.Type.Natural.Class+ Data.Type.Natural.Class.Arithmetic+ Data.Type.Natural.Class.Order+ build-depends:+ base ==4.*,+ equational-reasoning >=0.4.1.1 && <1,+ monomorphic >=0.0.3 && <0.1,+ template-haskell >=2.8 && <3,+ constraints >=0.3 && <0.9,+ ghc-typelits-natnormalise >=0.4 && <0.6,+ ghc-typelits-presburger >=0.1.1 && <1,+ singletons ==2.2.*+ default-language: Haskell2010+ default-extensions: DataKinds PolyKinds ConstraintKinds GADTs+ ScopedTypeVariables TemplateHaskell TypeFamilies TypeOperators+ MultiParamTypeClasses UndecidableInstances FlexibleContexts+ FlexibleInstances+ other-modules:+ Data.Type.Natural.Definitions+ Data.Type.Natural.Core+ Data.Type.Natural.Compat+ ghc-options: -Wall -O2 -fno-warn-orphans - default-language: Haskell2010- default-extensions: DataKinds- PolyKinds- ConstraintKinds- GADTs- ScopedTypeVariables- TemplateHaskell- TypeFamilies- TypeOperators- MultiParamTypeClasses- UndecidableInstances- FlexibleContexts- FlexibleInstances