type-natural 0.7.1.2 → 0.7.1.3
raw patch · 2 files changed
+12/−7 lines, 2 filesdep ~constraintsPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: constraints
API changes (from Hackage documentation)
- 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: (%:**) :: forall (t_ansO :: Nat) (t_ansP :: Nat). Sing t_ansO -> Sing t_ansP -> Sing (Apply (Apply (:**$) t_ansO) t_ansP :: Nat)
- Data.Type.Natural: data (:-$$) a1627805586 (l0 :: a1627805586) (l1 :: TyFun a1627805586 a1627805586) :: forall a1627805586. a1627805586 -> TyFun a1627805586 a1627805586 -> *
+ Data.Type.Natural: data (:-$$) a1627805829 (l0 :: a1627805829) (l1 :: TyFun a1627805829 a1627805829) :: forall a1627805829. a1627805829 -> TyFun a1627805829 a1627805829 -> *
- 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 MaxSym0 a1627685643 (l0 :: TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type)) :: forall a1627685643. TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type) -> *
- Data.Type.Natural: data MaxSym1 a1627685414 (l0 :: a1627685414) (l1 :: TyFun a1627685414 a1627685414) :: forall a1627685414. a1627685414 -> TyFun a1627685414 a1627685414 -> *
+ Data.Type.Natural: data MaxSym1 a1627685643 (l0 :: a1627685643) (l1 :: TyFun a1627685643 a1627685643) :: forall a1627685643. a1627685643 -> TyFun a1627685643 a1627685643 -> *
- 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 MinSym0 a1627685643 (l0 :: TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type)) :: forall a1627685643. TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type) -> *
- Data.Type.Natural: data MinSym1 a1627685414 (l0 :: a1627685414) (l1 :: TyFun a1627685414 a1627685414) :: forall a1627685414. a1627685414 -> TyFun a1627685414 a1627685414 -> *
+ Data.Type.Natural: data MinSym1 a1627685643 (l0 :: a1627685643) (l1 :: TyFun a1627685643 a1627685643) :: forall a1627685643. a1627685643 -> TyFun a1627685643 a1627685643 -> *
- Data.Type.Natural: data SSym0 (l_ajnP :: TyFun Nat Nat)
+ Data.Type.Natural: data SSym0 (l_ajsn :: TyFun Nat Nat)
- Data.Type.Natural: type (:-$$$) a1627805586 (t0 :: a1627805586) (t1 :: a1627805586) = (:-) a1627805586 t0 t1
+ Data.Type.Natural: type (:-$$$) a1627805829 (t0 :: a1627805829) (t1 :: a1627805829) = (:-) a1627805829 t0 t1
- Data.Type.Natural: type MaxSym2 a1627685414 (t0 :: a1627685414) (t1 :: a1627685414) = Max a1627685414 t0 t1
+ Data.Type.Natural: type MaxSym2 a1627685643 (t0 :: a1627685643) (t1 :: a1627685643) = Max a1627685643 t0 t1
- Data.Type.Natural: type MinSym2 a1627685414 (t0 :: a1627685414) (t1 :: a1627685414) = Min a1627685414 t0 t1
+ Data.Type.Natural: type MinSym2 a1627685643 (t0 :: a1627685643) (t1 :: a1627685643) = Min a1627685643 t0 t1
- Data.Type.Natural: type SSym1 (t_ajnO :: Nat) = S t_ajnO
+ Data.Type.Natural: type SSym1 (t_ajsm :: Nat) = S t_ajsm
- Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_aTjn :: Ordering). Sing t_aTjn -> Sing (Apply FlipOrderingSym0 t_aTjn :: Ordering)
+ Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_aTpR :: Ordering). Sing t_aTpR -> Sing (Apply FlipOrderingSym0 t_aTpR :: Ordering)
Files
- Data/Type/Natural.hs +11/−6
- type-natural.cabal +1/−1
Data/Type/Natural.hs view
@@ -71,7 +71,6 @@ import Proof.Equational import Proof.Propositional hiding (Not) import Data.Void-import Language.Haskell.TH hiding (Type) import Language.Haskell.TH.Quote --------------------------------------------------@@ -217,6 +216,8 @@ STrue -> Left $ sequalToRefl n m Witness SFalse -> Right Refl + cmpZero _ = Refl+ flipCompare n m = case n %:== m of STrue -> withRefl (sequalSym n m) Refl@@ -256,11 +257,15 @@ maxLeqR (SS n) (SS m) = maxLeqR n m maxLeqR SZ (SS m) = leqRefl m - maxLeast SZ SZ SZ Witness _ = Witness- maxLeast SZ SZ (SS _) a _ = case a of {}- maxLeast SZ (SS _) SZ a _ = case a of {}- maxLeast SZ (SS _) (SS _) a _ = case a of {}- maxLeast (SS _) _ _ _ a = case a of {}+ maxLeast _ SZ SZ _ _ = Witness+ maxLeast _ SZ (SS _) _ a = a+ maxLeast _ (SS _) SZ a _ = a+ maxLeast SZ _ (SS n) _ a = absurd $ succLeqZeroAbsurd n a+ maxLeast (SS k) (SS l) (SS m) slLEsk smLEsk =+ coerce (leqSucc' (sMax l m) k) $+ maxLeast k l m+ (coerce (sym $ leqSucc' l k) slLEsk)+ (coerce (sym $ leqSucc' m k) smLEsk) leqReversed _ _ = Refl lneqReversed _ _ = Refl
type-natural.cabal view
@@ -1,5 +1,5 @@ name: type-natural-version: 0.7.1.2+version: 0.7.1.3 cabal-version: >=1.10 build-type: Simple license: BSD3