type-natural 0.8.1.0 → 0.8.2.0
raw patch · 2 files changed
+14/−3 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 MaxSym1 a6989586621679302787 (l :: a6989586621679302787) (l1 :: TyFun a6989586621679302787 a6989586621679302787) :: forall a6989586621679302787. () => a6989586621679302787 -> TyFun a6989586621679302787 a6989586621679302787 -> *
- Data.Type.Natural: type *@#@$ = (:*$)
- Data.Type.Natural: type *@#@$$ = (:*$$)
- Data.Type.Natural: type +@#@$ = (:+$)
- Data.Type.Natural: type +@#@$$ = (:+$$)
- Data.Type.Natural: type -@#@$ = (:-$)
- Data.Type.Natural: type -@#@$$ = (:-$$)
- Data.Type.Natural.Builtin: (%*) :: forall nat_al8g (a_al8e :: nat_al8g) (b_al8f :: nat_al8g). SNum nat_al8g => Sing a_al8e -> Sing b_al8f -> Sing ((*) a_al8e b_al8f)
- Data.Type.Natural.Builtin: (%+) :: forall nat_al4h (a_al4f :: nat_al4h) (b_al4g :: nat_al4h). SNum nat_al4h => Sing a_al4f -> Sing b_al4g -> Sing ((+) a_al4f b_al4g)
- Data.Type.Natural.Builtin: (%-) :: forall nat_al6y (a_al6w :: nat_al6y) (b_al6x :: nat_al6y). SNum nat_al6y => Sing a_al6w -> Sing b_al6x -> Sing ((-) a_al6w b_al6x)
- Data.Type.Natural.Builtin: (%/=) :: forall nat_akZo (a_akZm :: nat_akZo) (b_akZn :: nat_akZo). SEq nat_akZo => Sing a_akZm -> Sing b_akZn -> Sing ((/=) a_akZm b_akZn)
- Data.Type.Natural.Builtin: (%<) :: forall nat_akRw (a_akRu :: nat_akRw) (b_akRv :: nat_akRw). SOrd nat_akRw => Sing a_akRu -> Sing b_akRv -> Sing ((<) a_akRu b_akRv)
- Data.Type.Natural.Builtin: (%<=) :: forall nat_akVW (a_akVU :: nat_akVW) (b_akVV :: nat_akVW). SOrd nat_akVW => Sing a_akVU -> Sing b_akVV -> Sing ((<=) a_akVU b_akVV)
- Data.Type.Natural.Builtin: (%==) :: forall nat_al1h (a_al1f :: nat_al1h) (b_al1g :: nat_al1h). SEq nat_al1h => Sing a_al1f -> Sing b_al1g -> Sing ((==) a_al1f b_al1g)
- Data.Type.Natural.Builtin: (%>) :: forall nat_akUd (a_akUb :: nat_akUd) (b_akUc :: nat_akUd). SOrd nat_akUd => Sing a_akUb -> Sing b_akUc -> Sing ((>) a_akUb b_akUc)
- Data.Type.Natural.Builtin: (%>=) :: forall nat_akXF (a_akXD :: nat_akXF) (b_akXE :: nat_akXF). SOrd nat_akXF => Sing a_akXD -> Sing b_akXE -> Sing ((>=) a_akXD b_akXE)
- Data.Type.Natural.Builtin: infix 4 %==
- Data.Type.Natural.Builtin: infixl 6 %-
- Data.Type.Natural.Builtin: infixl 7 %*
- Data.Type.Natural.Builtin: type (*@#@$$$) a_al8e b_al8f = (:*$$$) a_al8e b_al8f
- Data.Type.Natural.Builtin: type *@#@$ = (:*$)
- Data.Type.Natural.Builtin: type *@#@$$ = (:*$$)
- Data.Type.Natural.Builtin: type +@#@$ = (:+$)
- Data.Type.Natural.Builtin: type +@#@$$ = (:+$$)
- Data.Type.Natural.Builtin: type -@#@$ = (:-$)
- Data.Type.Natural.Builtin: type -@#@$$ = (:-$$)
- Data.Type.Natural.Builtin: type /=@#@$ = (:/=$)
- Data.Type.Natural.Builtin: type /=@#@$$ = (:/=$$)
- Data.Type.Natural.Builtin: type <=@#@$ = (:<=$)
- Data.Type.Natural.Builtin: type <=@#@$$ = (:<=$$)
- Data.Type.Natural.Builtin: type <@#@$ = (:<$)
- Data.Type.Natural.Builtin: type <@#@$$ = (:<$$)
- Data.Type.Natural.Builtin: type ==@#@$ = (:==$)
- Data.Type.Natural.Builtin: type ==@#@$$ = (:==$$)
- Data.Type.Natural.Builtin: type >=@#@$ = (:>=$)
- Data.Type.Natural.Builtin: type >=@#@$$ = (:>=$$)
- Data.Type.Natural.Builtin: type >@#@$ = (:>$)
- Data.Type.Natural.Builtin: type >@#@$$ = (:>$$)
- Data.Type.Natural.Class.Arithmetic: (%<) :: forall nat_akRw (a_akRu :: nat_akRw) (b_akRv :: nat_akRw). SOrd nat_akRw => Sing a_akRu -> Sing b_akRv -> Sing ((<) a_akRu b_akRv)
- Data.Type.Natural.Class.Arithmetic: (%<=) :: forall nat_akVW (a_akVU :: nat_akVW) (b_akVV :: nat_akVW). SOrd nat_akVW => Sing a_akVU -> Sing b_akVV -> Sing ((<=) a_akVU b_akVV)
- Data.Type.Natural.Class.Arithmetic: (%>) :: forall nat_akUd (a_akUb :: nat_akUd) (b_akUc :: nat_akUd). SOrd nat_akUd => Sing a_akUb -> Sing b_akUc -> Sing ((>) a_akUb b_akUc)
- Data.Type.Natural.Class.Arithmetic: (%>=) :: forall nat_akXF (a_akXD :: nat_akXF) (b_akXE :: nat_akXF). SOrd nat_akXF => Sing a_akXD -> Sing b_akXE -> Sing ((>=) a_akXD b_akXE)
- Data.Type.Natural.Class.Arithmetic: infixl 6 %-
- Data.Type.Natural.Class.Arithmetic: infixl 7 %*
- Data.Type.Natural.Class.Arithmetic: type *@#@$ = (:*$)
- Data.Type.Natural.Class.Arithmetic: type *@#@$$ = (:*$$)
- Data.Type.Natural.Class.Arithmetic: type +@#@$ = (:+$)
- Data.Type.Natural.Class.Arithmetic: type +@#@$$ = (:+$$)
- Data.Type.Natural.Class.Arithmetic: type -@#@$ = (:-$)
- Data.Type.Natural.Class.Arithmetic: type -@#@$$ = (:-$$)
- Data.Type.Natural.Class.Arithmetic: type /=@#@$ = (:/=$)
- Data.Type.Natural.Class.Arithmetic: type /=@#@$$ = (:/=$$)
- Data.Type.Natural.Class.Arithmetic: type <=@#@$ = (:<=$)
- Data.Type.Natural.Class.Arithmetic: type <=@#@$$ = (:<=$$)
- Data.Type.Natural.Class.Arithmetic: type <@#@$ = (:<$)
- Data.Type.Natural.Class.Arithmetic: type <@#@$$ = (:<$$)
- Data.Type.Natural.Class.Arithmetic: type ==@#@$ = (:==$)
- Data.Type.Natural.Class.Arithmetic: type ==@#@$$ = (:==$$)
- Data.Type.Natural.Class.Arithmetic: type >=@#@$ = (:>=$)
- Data.Type.Natural.Class.Arithmetic: type >=@#@$$ = (:>=$$)
- Data.Type.Natural.Class.Arithmetic: type >@#@$ = (:>$)
- Data.Type.Natural.Class.Arithmetic: type >@#@$$ = (:>$$)
- Data.Type.Natural.Class.Order: (%*) :: forall nat_al8g (a_al8e :: nat_al8g) (b_al8f :: nat_al8g). SNum nat_al8g => Sing a_al8e -> Sing b_al8f -> Sing ((*) a_al8e b_al8f)
- Data.Type.Natural.Class.Order: (%+) :: forall nat_al4h (a_al4f :: nat_al4h) (b_al4g :: nat_al4h). SNum nat_al4h => Sing a_al4f -> Sing b_al4g -> Sing ((+) a_al4f b_al4g)
- Data.Type.Natural.Class.Order: (%-) :: forall nat_al6y (a_al6w :: nat_al6y) (b_al6x :: nat_al6y). SNum nat_al6y => Sing a_al6w -> Sing b_al6x -> Sing ((-) a_al6w b_al6x)
- Data.Type.Natural.Class.Order: (%/=) :: forall nat_akZo (a_akZm :: nat_akZo) (b_akZn :: nat_akZo). SEq nat_akZo => Sing a_akZm -> Sing b_akZn -> Sing ((/=) a_akZm b_akZn)
- Data.Type.Natural.Class.Order: (%==) :: forall nat_al1h (a_al1f :: nat_al1h) (b_al1g :: nat_al1h). SEq nat_al1h => Sing a_al1f -> Sing b_al1g -> Sing ((==) a_al1f b_al1g)
- Data.Type.Natural.Class.Order: infix 4 %==
- Data.Type.Natural.Class.Order: infixl 6 %-
- Data.Type.Natural.Class.Order: infixl 7 %*
- Data.Type.Natural.Class.Order: type *@#@$ = (:*$)
- Data.Type.Natural.Class.Order: type *@#@$$ = (:*$$)
- Data.Type.Natural.Class.Order: type +@#@$ = (:+$)
- Data.Type.Natural.Class.Order: type +@#@$$ = (:+$$)
- Data.Type.Natural.Class.Order: type -@#@$ = (:-$)
- Data.Type.Natural.Class.Order: type -@#@$$ = (:-$$)
- Data.Type.Natural.Class.Order: type /=@#@$ = (:/=$)
- Data.Type.Natural.Class.Order: type /=@#@$$ = (:/=$$)
- Data.Type.Natural.Class.Order: type <=@#@$ = (:<=$)
- Data.Type.Natural.Class.Order: type <=@#@$$ = (:<=$$)
- Data.Type.Natural.Class.Order: type <@#@$ = (:<$)
- Data.Type.Natural.Class.Order: type <@#@$$ = (:<$$)
- Data.Type.Natural.Class.Order: type ==@#@$ = (:==$)
- Data.Type.Natural.Class.Order: type ==@#@$$ = (:==$$)
- Data.Type.Natural.Class.Order: type >=@#@$ = (:>=$)
- Data.Type.Natural.Class.Order: type >=@#@$$ = (:>=$$)
- Data.Type.Natural.Class.Order: type >@#@$ = (:>$)
- Data.Type.Natural.Class.Order: type >@#@$$ = (:>$$)
- Data.Type.Ordinal: instance (Data.Singletons.SingI m, Data.Singletons.SingI n, n ~ (m Data.Type.Natural.Singleton.Compat.+ 1)) => GHC.Enum.Bounded (Data.Type.Ordinal.Ordinal n)
- Data.Type.Ordinal: instance (Data.Type.Natural.Class.Order.PeanoOrder nat, Data.Singletons.SingKind nat) => Data.Type.Ordinal.HasOrdinal nat
- Data.Type.Ordinal: instance Data.Singletons.SingI n => GHC.Enum.Bounded (Data.Type.Ordinal.Ordinal ('Data.Type.Natural.Definitions.S n))
- Data.Type.Ordinal: instance forall k (nat1 :: k) nat2 (n :: nat2). (Data.Singletons.SingI n, Data.Type.Ordinal.HasOrdinal nat2) => GHC.Show.Show (Data.Type.Ordinal.Ordinal n)
- Data.Type.Ordinal: instance forall k (nat1 :: k) nat2 (n :: nat2). (Data.Type.Ordinal.HasOrdinal nat2, Data.Singletons.SingI n) => GHC.Enum.Enum (Data.Type.Ordinal.Ordinal n)
- Data.Type.Ordinal: instance forall k (nat1 :: k) nat2 (n :: nat2). (Data.Type.Ordinal.HasOrdinal nat2, Data.Singletons.SingI n) => GHC.Num.Num (Data.Type.Ordinal.Ordinal n)
- Data.Type.Ordinal: instance forall k (nat1 :: k) nat2 (n :: nat2). Data.Type.Ordinal.HasOrdinal nat2 => GHC.Classes.Eq (Data.Type.Ordinal.Ordinal n)
- Data.Type.Ordinal: instance forall k (nat1 :: k) nat2 (n :: nat2). Data.Type.Ordinal.HasOrdinal nat2 => GHC.Classes.Ord (Data.Type.Ordinal.Ordinal n)
+ Data.Type.Natural: data MaxSym1 (l :: a6989586621679299162) (l1 :: TyFun a6989586621679299162 a6989586621679299162) :: forall a6989586621679299162. () => a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *
+ Data.Type.Natural: data (-@#@$$) (l :: a6989586621679412326) (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. () => a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *
+ Data.Type.Natural: nat :: QuasiQuoter
+ Data.Type.Natural.Class.Arithmetic: class PNum a where {
+ Data.Type.Natural.Class.Arithmetic: class SNum a
+ Data.Type.Natural.Class.Arithmetic: data (/=@#@$) (l :: TyFun a6989586621679288106 TyFun a6989586621679288106 Bool -> Type) :: forall a6989586621679288106. () => TyFun a6989586621679288106 TyFun a6989586621679288106 Bool -> Type -> *
+ Data.Type.Natural.Class.Arithmetic: data (/=@#@$$) (l :: a6989586621679288106) (l1 :: TyFun a6989586621679288106 Bool) :: forall a6989586621679288106. () => a6989586621679288106 -> TyFun a6989586621679288106 Bool -> *
+ Data.Type.Natural.Class.Arithmetic: data (*@#@$$) (l :: a6989586621679412326) (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. () => a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *
+ Data.Type.Natural.Class.Arithmetic: sAbs :: SNum a => Sing t -> Sing Apply (AbsSym0 :: TyFun a a -> *) t
+ Data.Type.Natural.Class.Arithmetic: sFromInteger :: SNum a => Sing t -> Sing Apply (FromIntegerSym0 :: TyFun Nat a -> *) t
+ Data.Type.Natural.Class.Arithmetic: sNegate :: SNum a => Sing t -> Sing Apply (NegateSym0 :: TyFun a a -> *) t
+ Data.Type.Natural.Class.Arithmetic: sSignum :: SNum a => Sing t -> Sing Apply (SignumSym0 :: TyFun a a -> *) t
+ Data.Type.Natural.Class.Arithmetic: type FromIntegerSym1 (t :: Nat) = (FromInteger t :: k)
+ Data.Type.Natural.Class.Arithmetic: type family FromInteger (arg :: Nat) :: a;
+ Data.Type.Natural.Class.Arithmetic: }
+ Data.Type.Natural.Class.Order: class PEq a => POrd a where {
+ Data.Type.Natural.Class.Order: class SEq a => SOrd a
+ Data.Type.Natural.Class.Order: data MinSym0 (l :: TyFun a6989586621679299162 TyFun a6989586621679299162 a6989586621679299162 -> Type) :: forall a6989586621679299162. () => TyFun a6989586621679299162 TyFun a6989586621679299162 a6989586621679299162 -> Type -> *
+ Data.Type.Natural.Class.Order: data MinSym1 (l :: a6989586621679299162) (l1 :: TyFun a6989586621679299162 a6989586621679299162) :: forall a6989586621679299162. () => a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *
+ Data.Type.Natural.Class.Order: sCompare :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply (CompareSym0 :: TyFun a TyFun a Ordering -> Type -> *) t1 t2
+ Data.Type.Natural.Class.Order: sMax :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply (MaxSym0 :: TyFun a TyFun a a -> Type -> *) t1 t2
+ Data.Type.Natural.Class.Order: sMin :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply (MinSym0 :: TyFun a TyFun a a -> Type -> *) t1 t2
+ Data.Type.Natural.Class.Order: type CompareSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Compare t t1
+ Data.Type.Natural.Class.Order: type EQSym0 = EQ
+ Data.Type.Natural.Class.Order: type GTSym0 = GT
+ Data.Type.Natural.Class.Order: type LTSym0 = LT
+ Data.Type.Natural.Class.Order: type MaxSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Max t t1
+ Data.Type.Natural.Class.Order: type MinSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Min t t1
+ Data.Type.Natural.Class.Order: type family Min (arg :: a) (arg1 :: a) :: a;
+ Data.Type.Natural.Class.Order: }
+ Data.Type.Ordinal: instance (Data.Singletons.Internal.SingI m, Data.Singletons.Internal.SingI n, n ~ (m Data.Singletons.Prelude.Num.+ 1)) => GHC.Enum.Bounded (Data.Type.Ordinal.Ordinal n)
+ Data.Type.Ordinal: instance (Data.Type.Natural.Class.Order.PeanoOrder nat, Data.Singletons.Internal.SingKind nat) => Data.Type.Ordinal.HasOrdinal nat
+ Data.Type.Ordinal: instance Data.Singletons.Internal.SingI n => GHC.Enum.Bounded (Data.Type.Ordinal.Ordinal ('Data.Type.Natural.Definitions.S n))
+ Data.Type.Ordinal: instance forall nat (n :: nat). (Data.Singletons.Internal.SingI n, Data.Type.Ordinal.HasOrdinal nat) => GHC.Show.Show (Data.Type.Ordinal.Ordinal n)
+ Data.Type.Ordinal: instance forall nat (n :: nat). (Data.Type.Ordinal.HasOrdinal nat, Data.Singletons.Internal.SingI n) => GHC.Enum.Enum (Data.Type.Ordinal.Ordinal n)
+ Data.Type.Ordinal: instance forall nat (n :: nat). (Data.Type.Ordinal.HasOrdinal nat, Data.Singletons.Internal.SingI n) => GHC.Num.Num (Data.Type.Ordinal.Ordinal n)
+ Data.Type.Ordinal: instance forall nat (n :: nat). Data.Type.Ordinal.HasOrdinal nat => GHC.Classes.Eq (Data.Type.Ordinal.Ordinal n)
+ Data.Type.Ordinal: instance forall nat (n :: nat). Data.Type.Ordinal.HasOrdinal nat => GHC.Classes.Ord (Data.Type.Ordinal.Ordinal n)
- Data.Type.Natural: (%*) :: forall nat_al8g (a_al8e :: nat_al8g) (b_al8f :: nat_al8g). SNum nat_al8g => Sing a_al8e -> Sing b_al8f -> Sing ((*) a_al8e b_al8f)
+ Data.Type.Natural: (%*) :: SNum a => Sing t1 -> Sing t2 -> Sing Apply Apply ((*@#@$) :: TyFun a TyFun a a -> Type -> *) t1 t2
- Data.Type.Natural: (%**) :: SNat n -> SNat m -> SNat (n ** m)
+ Data.Type.Natural: (%**) :: forall (t_asDz :: Nat) (t_asDA :: Nat). Sing t_asDz -> Sing t_asDA -> Sing (Apply (Apply (**@#@$) t_asDz) t_asDA :: Nat)
- Data.Type.Natural: (%+) :: forall nat_al4h (a_al4f :: nat_al4h) (b_al4g :: nat_al4h). SNum nat_al4h => Sing a_al4f -> Sing b_al4g -> Sing ((+) a_al4f b_al4g)
+ Data.Type.Natural: (%+) :: SNum a => Sing t1 -> Sing t2 -> Sing Apply Apply ((+@#@$) :: TyFun a TyFun a a -> Type -> *) t1 t2
- Data.Type.Natural: (%-) :: forall nat_al6y (a_al6w :: nat_al6y) (b_al6x :: nat_al6y). SNum nat_al6y => Sing a_al6w -> Sing b_al6x -> Sing ((-) a_al6w b_al6x)
+ Data.Type.Natural: (%-) :: SNum a => Sing t1 -> Sing t2 -> Sing Apply Apply ((-@#@$) :: TyFun a TyFun a a -> Type -> *) t1 t2
- Data.Type.Natural: data SSym0 (l_anmq :: TyFun Nat Nat)
+ Data.Type.Natural: data SSym0 (l_ai2n :: TyFun Nat Nat)
- Data.Type.Natural: data MaxSym0 a6989586621679302787 (l :: TyFun a6989586621679302787 (TyFun a6989586621679302787 a6989586621679302787 -> Type)) :: forall a6989586621679302787. () => TyFun a6989586621679302787 (TyFun a6989586621679302787 a6989586621679302787 -> Type) -> *
+ Data.Type.Natural: data (-@#@$) (l :: TyFun a6989586621679412326 TyFun a6989586621679412326 a6989586621679412326 -> Type) :: forall a6989586621679412326. () => TyFun a6989586621679412326 TyFun a6989586621679412326 a6989586621679412326 -> Type -> *
- Data.Type.Natural: leqStep :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + l) :~: m -> IsTrue (n <= m)
+ Data.Type.Natural: leqStep :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m -> IsTrue (n <= m)
- Data.Type.Natural: minusNilpotent :: IsPeano nat => Sing n -> (n - n) :~: Zero nat
+ Data.Type.Natural: minusNilpotent :: IsPeano nat => Sing n -> n - n :~: Zero nat
- Data.Type.Natural: minusPlus :: forall (n :: nat) m. (PeanoOrder nat, PeanoOrder nat) => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n
+ Data.Type.Natural: minusPlus :: forall (n :: nat) m. (PeanoOrder nat, PeanoOrder nat) => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> n - m + m :~: n
- Data.Type.Natural: minusSucc :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)
+ Data.Type.Natural: minusSucc :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Succ n - m :~: Succ (n - m)
- Data.Type.Natural: minusZero :: IsPeano nat => Sing n -> (n - Zero nat) :~: n
+ Data.Type.Natural: minusZero :: IsPeano nat => Sing n -> n - Zero nat :~: n
- Data.Type.Natural: multAssoc :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))
+ Data.Type.Natural: multAssoc :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) * l :~: n * (m * l)
- Data.Type.Natural: multComm :: IsPeano nat => Sing (n :: nat) -> Sing m -> (n * m) :~: (m * n)
+ Data.Type.Natural: multComm :: IsPeano nat => Sing (n :: nat) -> Sing m -> n * m :~: m * n
- Data.Type.Natural: multCong :: n :~: m -> l :~: k -> (n * l) :~: (m * k)
+ Data.Type.Natural: multCong :: n :~: m -> l :~: k -> n * l :~: m * k
- Data.Type.Natural: multCongL :: n :~: m -> Sing k -> (n * k) :~: (m * k)
+ Data.Type.Natural: multCongL :: n :~: m -> Sing k -> n * k :~: m * k
- Data.Type.Natural: multCongR :: Sing k -> n :~: m -> (k * n) :~: (k * m)
+ Data.Type.Natural: multCongR :: Sing k -> n :~: m -> k * n :~: k * m
- Data.Type.Natural: multEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (Succ n * m) :~: (Succ n * l) -> m :~: l
+ Data.Type.Natural: multEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> Succ n * m :~: Succ n * l -> m :~: l
- Data.Type.Natural: multEqCancelR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * Succ l) :~: (m * Succ l) -> n :~: m
+ Data.Type.Natural: multEqCancelR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * Succ l :~: m * Succ l -> n :~: m
- Data.Type.Natural: multEqSuccElimL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) :~: Succ l -> n :~: Succ (Pred n)
+ Data.Type.Natural: multEqSuccElimL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> n :~: Succ (Pred n)
- Data.Type.Natural: multEqSuccElimR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) :~: Succ l -> m :~: Succ (Pred m)
+ Data.Type.Natural: multEqSuccElimR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> m :~: Succ (Pred m)
- Data.Type.Natural: multOneL :: IsPeano nat => Sing n -> (One nat * n) :~: n
+ Data.Type.Natural: multOneL :: IsPeano nat => Sing n -> One nat * n :~: n
- Data.Type.Natural: multOneR :: IsPeano nat => Sing n -> (n * One nat) :~: n
+ Data.Type.Natural: multOneR :: IsPeano nat => Sing n -> n * One nat :~: n
- Data.Type.Natural: multPlusDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))
+ Data.Type.Natural: multPlusDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * (m + l) :~: (n * m) + (n * l)
- Data.Type.Natural: multSuccL :: IsPeano nat => Sing (n :: nat) -> Sing m -> (S n * m) :~: ((n * m) + m)
+ Data.Type.Natural: multSuccL :: IsPeano nat => Sing (n :: nat) -> Sing m -> S n * m :~: n * m + m
- Data.Type.Natural: multSuccR :: IsPeano nat => Sing n -> Sing m -> (n * S m) :~: ((n * m) + (n :: nat))
+ Data.Type.Natural: multSuccR :: IsPeano nat => Sing n -> Sing m -> n * S m :~: n * m + (n :: nat)
- Data.Type.Natural: multZeroL :: IsPeano nat => Sing n -> (Zero nat * n) :~: Zero nat
+ Data.Type.Natural: multZeroL :: IsPeano nat => Sing n -> Zero nat * n :~: Zero nat
- Data.Type.Natural: multZeroR :: IsPeano nat => Sing n -> (n * Zero nat) :~: Zero nat
+ Data.Type.Natural: multZeroR :: IsPeano nat => Sing n -> n * Zero nat :~: Zero nat
- Data.Type.Natural: plusAssoc :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))
+ Data.Type.Natural: plusAssoc :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) + l :~: n + (m + l)
- Data.Type.Natural: plusComm :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: ((m :: nat) + n)
+ Data.Type.Natural: plusComm :: IsPeano nat => Sing n -> Sing m -> n + m :~: (m :: nat) + n
- Data.Type.Natural: plusCong :: n :~: m -> n' :~: m' -> (n + n') :~: (m + m')
+ Data.Type.Natural: plusCong :: n :~: m -> n' :~: m' -> n + n' :~: m + m'
- Data.Type.Natural: plusCongL :: n :~: m -> Sing k -> (n + k) :~: (m + k)
+ Data.Type.Natural: plusCongL :: n :~: m -> Sing k -> n + k :~: m + k
- Data.Type.Natural: plusCongR :: Sing k -> n :~: m -> (k + n) :~: (k + m)
+ Data.Type.Natural: plusCongR :: Sing k -> n :~: m -> k + n :~: k + m
- Data.Type.Natural: plusEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) :~: (n + l) -> m :~: l
+ Data.Type.Natural: plusEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n + m :~: n + l -> m :~: l
- Data.Type.Natural: plusEqCancelR :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + l) :~: (m + l) -> n :~: m
+ Data.Type.Natural: plusEqCancelR :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m + l -> n :~: m
- Data.Type.Natural: plusEqZeroL :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: Zero nat -> n :~: Zero nat
+ Data.Type.Natural: plusEqZeroL :: IsPeano nat => Sing n -> Sing m -> n + m :~: Zero nat -> n :~: Zero nat
- Data.Type.Natural: plusEqZeroR :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: Zero nat -> m :~: Zero nat
+ Data.Type.Natural: plusEqZeroR :: IsPeano nat => Sing n -> Sing m -> n + m :~: Zero nat -> m :~: Zero nat
- Data.Type.Natural: plusInjectiveL :: SNat n -> SNat m -> SNat l -> (n + m) :~: (n + l) -> m :~: l
+ Data.Type.Natural: plusInjectiveL :: SNat n -> SNat m -> SNat l -> n + m :~: n + l -> m :~: l
- Data.Type.Natural: plusInjectiveR :: SNat n -> SNat m -> SNat l -> (n + l) :~: (m + l) -> n :~: m
+ Data.Type.Natural: plusInjectiveR :: SNat n -> SNat m -> SNat l -> n + l :~: m + l -> n :~: m
- Data.Type.Natural: plusMinus :: IsPeano nat => Sing (n :: nat) -> Sing m -> ((n + m) - m) :~: n
+ Data.Type.Natural: plusMinus :: IsPeano nat => Sing (n :: nat) -> Sing m -> n + m - m :~: n
- Data.Type.Natural: plusMinus' :: IsPeano nat => Sing (n :: nat) -> Sing m -> ((n + m) - n) :~: m
+ Data.Type.Natural: plusMinus' :: IsPeano nat => Sing (n :: nat) -> Sing m -> n + m - n :~: m
- Data.Type.Natural: plusMultDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))
+ Data.Type.Natural: plusMultDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) * l :~: (n * l) + (m * l)
- Data.Type.Natural: plusNeutralL :: SNat n -> SNat m -> (n + m) :~: m -> n :~: 'Z
+ Data.Type.Natural: plusNeutralL :: SNat n -> SNat m -> n + m :~: m -> n :~: 'Z
- Data.Type.Natural: plusNeutralR :: SNat n -> SNat m -> (n + m) :~: n -> m :~: 'Z
+ Data.Type.Natural: plusNeutralR :: SNat n -> SNat m -> n + m :~: n -> m :~: 'Z
- Data.Type.Natural: plusSuccL :: IsPeano nat => Sing n -> Sing m -> (S n + m) :~: S (n + m :: nat)
+ Data.Type.Natural: plusSuccL :: IsPeano nat => Sing n -> Sing m -> S n + m :~: S (n + m :: nat)
- Data.Type.Natural: plusSuccR :: IsPeano nat => Sing n -> Sing m -> (n + S m) :~: S (n + m :: nat)
+ Data.Type.Natural: plusSuccR :: IsPeano nat => Sing n -> Sing m -> n + S m :~: S (n + m :: nat)
- Data.Type.Natural: sMax :: SOrd a => forall (t1 :: a) (t2 :: a). () => Sing a t1 -> Sing a t2 -> Sing a Apply a a Apply a (TyFun a a -> Type) MaxSym0 a t1 t2
+ Data.Type.Natural: sMax :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply (MaxSym0 :: TyFun a TyFun a a -> Type -> *) t1 t2
- Data.Type.Natural: sMin :: SOrd a => forall (t1 :: a) (t2 :: a). () => Sing a t1 -> Sing a t2 -> Sing a Apply a a Apply a (TyFun a a -> Type) MinSym0 a t1 t2
+ Data.Type.Natural: sMin :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply (MinSym0 :: TyFun a TyFun a a -> Type -> *) t1 t2
- Data.Type.Natural: succAndPlusOneL :: IsPeano nat => Sing n -> Succ n :~: (One nat + n)
+ Data.Type.Natural: succAndPlusOneL :: IsPeano nat => Sing n -> Succ n :~: One nat + n
- Data.Type.Natural: succAndPlusOneR :: IsPeano nat => Sing n -> Succ n :~: (n + One nat)
+ Data.Type.Natural: succAndPlusOneR :: IsPeano nat => Sing n -> Succ n :~: n + One nat
- Data.Type.Natural: type (<=) a_akVU b_akVV = (:<=) a_akVU b_akVV
+ Data.Type.Natural: type (-@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t - t1
- Data.Type.Natural: type MaxSym2 a6989586621679302787 (t :: a6989586621679302787) (t1 :: a6989586621679302787) = Max a6989586621679302787 t t1
+ Data.Type.Natural: type MaxSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Max t t1
- Data.Type.Natural: type MinSym2 a6989586621679302787 (t :: a6989586621679302787) (t1 :: a6989586621679302787) = Min a6989586621679302787 t t1
+ Data.Type.Natural: type MinSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Min t t1
- Data.Type.Natural: type SSym1 (t_anmp :: Nat) = S t_anmp
+ Data.Type.Natural: type SSym1 (t_ai2m :: Nat) = S t_ai2m
- Data.Type.Natural.Builtin: fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n * m) :~: (FromPeano n * FromPeano m)
+ Data.Type.Natural.Builtin: fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n * m) :~: FromPeano n * FromPeano m
- Data.Type.Natural.Builtin: fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n + m) :~: (FromPeano n + FromPeano m)
+ Data.Type.Natural.Builtin: fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n + m) :~: FromPeano n + FromPeano m
- Data.Type.Natural.Builtin: minusNilpotent :: IsPeano nat => Sing n -> (n - n) :~: Zero nat
+ Data.Type.Natural.Builtin: minusNilpotent :: IsPeano nat => Sing n -> n - n :~: Zero nat
- Data.Type.Natural.Builtin: minusZero :: IsPeano nat => Sing n -> (n - Zero nat) :~: n
+ Data.Type.Natural.Builtin: minusZero :: IsPeano nat => Sing n -> n - Zero nat :~: n
- Data.Type.Natural.Builtin: multAssoc :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))
+ Data.Type.Natural.Builtin: multAssoc :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) * l :~: n * (m * l)
- Data.Type.Natural.Builtin: multComm :: IsPeano nat => Sing (n :: nat) -> Sing m -> (n * m) :~: (m * n)
+ Data.Type.Natural.Builtin: multComm :: IsPeano nat => Sing (n :: nat) -> Sing m -> n * m :~: m * n
- Data.Type.Natural.Builtin: multEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (Succ n * m) :~: (Succ n * l) -> m :~: l
+ Data.Type.Natural.Builtin: multEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> Succ n * m :~: Succ n * l -> m :~: l
- Data.Type.Natural.Builtin: multEqCancelR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * Succ l) :~: (m * Succ l) -> n :~: m
+ Data.Type.Natural.Builtin: multEqCancelR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * Succ l :~: m * Succ l -> n :~: m
- Data.Type.Natural.Builtin: multEqSuccElimL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) :~: Succ l -> n :~: Succ (Pred n)
+ Data.Type.Natural.Builtin: multEqSuccElimL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> n :~: Succ (Pred n)
- Data.Type.Natural.Builtin: multEqSuccElimR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) :~: Succ l -> m :~: Succ (Pred m)
+ Data.Type.Natural.Builtin: multEqSuccElimR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> m :~: Succ (Pred m)
- Data.Type.Natural.Builtin: multOneL :: IsPeano nat => Sing n -> (One nat * n) :~: n
+ Data.Type.Natural.Builtin: multOneL :: IsPeano nat => Sing n -> One nat * n :~: n
- Data.Type.Natural.Builtin: multOneR :: IsPeano nat => Sing n -> (n * One nat) :~: n
+ Data.Type.Natural.Builtin: multOneR :: IsPeano nat => Sing n -> n * One nat :~: n
- Data.Type.Natural.Builtin: multPlusDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))
+ Data.Type.Natural.Builtin: multPlusDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * (m + l) :~: (n * m) + (n * l)
- Data.Type.Natural.Builtin: multSuccL :: IsPeano nat => Sing (n :: nat) -> Sing m -> (S n * m) :~: ((n * m) + m)
+ Data.Type.Natural.Builtin: multSuccL :: IsPeano nat => Sing (n :: nat) -> Sing m -> S n * m :~: n * m + m
- Data.Type.Natural.Builtin: multSuccR :: IsPeano nat => Sing n -> Sing m -> (n * S m) :~: ((n * m) + (n :: nat))
+ Data.Type.Natural.Builtin: multSuccR :: IsPeano nat => Sing n -> Sing m -> n * S m :~: n * m + (n :: nat)
- Data.Type.Natural.Builtin: multZeroL :: IsPeano nat => Sing n -> (Zero nat * n) :~: Zero nat
+ Data.Type.Natural.Builtin: multZeroL :: IsPeano nat => Sing n -> Zero nat * n :~: Zero nat
- Data.Type.Natural.Builtin: multZeroR :: IsPeano nat => Sing n -> (n * Zero nat) :~: Zero nat
+ Data.Type.Natural.Builtin: multZeroR :: IsPeano nat => Sing n -> n * Zero nat :~: Zero nat
- Data.Type.Natural.Builtin: plusAssoc :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))
+ Data.Type.Natural.Builtin: plusAssoc :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) + l :~: n + (m + l)
- Data.Type.Natural.Builtin: plusComm :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: ((m :: nat) + n)
+ Data.Type.Natural.Builtin: plusComm :: IsPeano nat => Sing n -> Sing m -> n + m :~: (m :: nat) + n
- Data.Type.Natural.Builtin: plusEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) :~: (n + l) -> m :~: l
+ Data.Type.Natural.Builtin: plusEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n + m :~: n + l -> m :~: l
- Data.Type.Natural.Builtin: plusEqCancelR :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + l) :~: (m + l) -> n :~: m
+ Data.Type.Natural.Builtin: plusEqCancelR :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m + l -> n :~: m
- Data.Type.Natural.Builtin: plusEqZeroL :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: Zero nat -> n :~: Zero nat
+ Data.Type.Natural.Builtin: plusEqZeroL :: IsPeano nat => Sing n -> Sing m -> n + m :~: Zero nat -> n :~: Zero nat
- Data.Type.Natural.Builtin: plusEqZeroR :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: Zero nat -> m :~: Zero nat
+ Data.Type.Natural.Builtin: plusEqZeroR :: IsPeano nat => Sing n -> Sing m -> n + m :~: Zero nat -> m :~: Zero nat
- Data.Type.Natural.Builtin: plusMinus :: IsPeano nat => Sing (n :: nat) -> Sing m -> ((n + m) - m) :~: n
+ Data.Type.Natural.Builtin: plusMinus :: IsPeano nat => Sing (n :: nat) -> Sing m -> n + m - m :~: n
- Data.Type.Natural.Builtin: plusMinus' :: IsPeano nat => Sing (n :: nat) -> Sing m -> ((n + m) - n) :~: m
+ Data.Type.Natural.Builtin: plusMinus' :: IsPeano nat => Sing (n :: nat) -> Sing m -> n + m - n :~: m
- Data.Type.Natural.Builtin: plusMultDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))
+ Data.Type.Natural.Builtin: plusMultDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) * l :~: (n * l) + (m * l)
- Data.Type.Natural.Builtin: plusSuccL :: IsPeano nat => Sing n -> Sing m -> (S n + m) :~: S (n + m :: nat)
+ Data.Type.Natural.Builtin: plusSuccL :: IsPeano nat => Sing n -> Sing m -> S n + m :~: S (n + m :: nat)
- Data.Type.Natural.Builtin: plusSuccR :: IsPeano nat => Sing n -> Sing m -> (n + S m) :~: S (n + m :: nat)
+ Data.Type.Natural.Builtin: plusSuccR :: IsPeano nat => Sing n -> Sing m -> n + S m :~: S (n + m :: nat)
- Data.Type.Natural.Builtin: succAndPlusOneL :: IsPeano nat => Sing n -> Succ n :~: (One nat + n)
+ Data.Type.Natural.Builtin: succAndPlusOneL :: IsPeano nat => Sing n -> Succ n :~: One nat + n
- Data.Type.Natural.Builtin: succAndPlusOneR :: IsPeano nat => Sing n -> Succ n :~: (n + One nat)
+ Data.Type.Natural.Builtin: succAndPlusOneR :: IsPeano nat => Sing n -> Succ n :~: n + One nat
- Data.Type.Natural.Builtin: toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n * m) :~: (ToPeano n * ToPeano m)
+ Data.Type.Natural.Builtin: toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n * m) :~: ToPeano n * ToPeano m
- Data.Type.Natural.Builtin: toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n + m) :~: (ToPeano n + ToPeano m)
+ Data.Type.Natural.Builtin: toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n + m) :~: ToPeano n + ToPeano m
- Data.Type.Natural.Class.Arithmetic: (%*) :: forall nat_al8g (a_al8e :: nat_al8g) (b_al8f :: nat_al8g). SNum nat_al8g => Sing a_al8e -> Sing b_al8f -> Sing ((*) a_al8e b_al8f)
+ Data.Type.Natural.Class.Arithmetic: (%*) :: SNum a => Sing t1 -> Sing t2 -> Sing Apply Apply ((*@#@$) :: TyFun a TyFun a a -> Type -> *) t1 t2
- Data.Type.Natural.Class.Arithmetic: (%+) :: forall nat_al4h (a_al4f :: nat_al4h) (b_al4g :: nat_al4h). SNum nat_al4h => Sing a_al4f -> Sing b_al4g -> Sing ((+) a_al4f b_al4g)
+ Data.Type.Natural.Class.Arithmetic: (%+) :: SNum a => Sing t1 -> Sing t2 -> Sing Apply Apply ((+@#@$) :: TyFun a TyFun a a -> Type -> *) t1 t2
- Data.Type.Natural.Class.Arithmetic: (%-) :: forall nat_al6y (a_al6w :: nat_al6y) (b_al6x :: nat_al6y). SNum nat_al6y => Sing a_al6w -> Sing b_al6x -> Sing ((-) a_al6w b_al6x)
+ Data.Type.Natural.Class.Arithmetic: (%-) :: SNum a => Sing t1 -> Sing t2 -> Sing Apply Apply ((-@#@$) :: TyFun a TyFun a a -> Type -> *) t1 t2
- Data.Type.Natural.Class.Arithmetic: (%/=) :: forall nat_akZo (a_akZm :: nat_akZo) (b_akZn :: nat_akZo). SEq nat_akZo => Sing a_akZm -> Sing b_akZn -> Sing ((/=) a_akZm b_akZn)
+ Data.Type.Natural.Class.Arithmetic: (%/=) :: SEq k => Sing a -> Sing b -> Sing a /= b
- Data.Type.Natural.Class.Arithmetic: (%==) :: forall nat_al1h (a_al1f :: nat_al1h) (b_al1g :: nat_al1h). SEq nat_al1h => Sing a_al1f -> Sing b_al1g -> Sing ((==) a_al1f b_al1g)
+ Data.Type.Natural.Class.Arithmetic: (%==) :: SEq k => Sing a -> Sing b -> Sing a == b
- Data.Type.Natural.Class.Arithmetic: infix 4 %==
+ Data.Type.Natural.Class.Arithmetic: infix 4 %/=
- Data.Type.Natural.Class.Arithmetic: minusCong :: n :~: m -> l :~: k -> (n - l) :~: (m - k)
+ Data.Type.Natural.Class.Arithmetic: minusCong :: n :~: m -> l :~: k -> n - l :~: m - k
- Data.Type.Natural.Class.Arithmetic: minusCongL :: n :~: m -> Sing k -> (n - k) :~: (m - k)
+ Data.Type.Natural.Class.Arithmetic: minusCongL :: n :~: m -> Sing k -> n - k :~: m - k
- Data.Type.Natural.Class.Arithmetic: minusCongR :: Sing k -> n :~: m -> (k - n) :~: (k - m)
+ Data.Type.Natural.Class.Arithmetic: minusCongR :: Sing k -> n :~: m -> k - n :~: k - m
- Data.Type.Natural.Class.Arithmetic: minusNilpotent :: IsPeano nat => Sing n -> (n - n) :~: Zero nat
+ Data.Type.Natural.Class.Arithmetic: minusNilpotent :: IsPeano nat => Sing n -> n - n :~: Zero nat
- Data.Type.Natural.Class.Arithmetic: minusZero :: IsPeano nat => Sing n -> (n - Zero nat) :~: n
+ Data.Type.Natural.Class.Arithmetic: minusZero :: IsPeano nat => Sing n -> n - Zero nat :~: n
- Data.Type.Natural.Class.Arithmetic: multAssoc :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))
+ Data.Type.Natural.Class.Arithmetic: multAssoc :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) * l :~: n * (m * l)
- Data.Type.Natural.Class.Arithmetic: multComm :: IsPeano nat => Sing (n :: nat) -> Sing m -> (n * m) :~: (m * n)
+ Data.Type.Natural.Class.Arithmetic: multComm :: IsPeano nat => Sing (n :: nat) -> Sing m -> n * m :~: m * n
- Data.Type.Natural.Class.Arithmetic: multCong :: n :~: m -> l :~: k -> (n * l) :~: (m * k)
+ Data.Type.Natural.Class.Arithmetic: multCong :: n :~: m -> l :~: k -> n * l :~: m * k
- Data.Type.Natural.Class.Arithmetic: multCongL :: n :~: m -> Sing k -> (n * k) :~: (m * k)
+ Data.Type.Natural.Class.Arithmetic: multCongL :: n :~: m -> Sing k -> n * k :~: m * k
- Data.Type.Natural.Class.Arithmetic: multCongR :: Sing k -> n :~: m -> (k * n) :~: (k * m)
+ Data.Type.Natural.Class.Arithmetic: multCongR :: Sing k -> n :~: m -> k * n :~: k * m
- Data.Type.Natural.Class.Arithmetic: multEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (Succ n * m) :~: (Succ n * l) -> m :~: l
+ Data.Type.Natural.Class.Arithmetic: multEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> Succ n * m :~: Succ n * l -> m :~: l
- Data.Type.Natural.Class.Arithmetic: multEqCancelR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * Succ l) :~: (m * Succ l) -> n :~: m
+ Data.Type.Natural.Class.Arithmetic: multEqCancelR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * Succ l :~: m * Succ l -> n :~: m
- Data.Type.Natural.Class.Arithmetic: multEqSuccElimL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) :~: Succ l -> n :~: Succ (Pred n)
+ Data.Type.Natural.Class.Arithmetic: multEqSuccElimL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> n :~: Succ (Pred n)
- Data.Type.Natural.Class.Arithmetic: multEqSuccElimR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * m) :~: Succ l -> m :~: Succ (Pred m)
+ Data.Type.Natural.Class.Arithmetic: multEqSuccElimR :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * m :~: Succ l -> m :~: Succ (Pred m)
- Data.Type.Natural.Class.Arithmetic: multOneL :: IsPeano nat => Sing n -> (One nat * n) :~: n
+ Data.Type.Natural.Class.Arithmetic: multOneL :: IsPeano nat => Sing n -> One nat * n :~: n
- Data.Type.Natural.Class.Arithmetic: multOneR :: IsPeano nat => Sing n -> (n * One nat) :~: n
+ Data.Type.Natural.Class.Arithmetic: multOneR :: IsPeano nat => Sing n -> n * One nat :~: n
- Data.Type.Natural.Class.Arithmetic: multPlusDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))
+ Data.Type.Natural.Class.Arithmetic: multPlusDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n * (m + l) :~: (n * m) + (n * l)
- Data.Type.Natural.Class.Arithmetic: multSuccL :: IsPeano nat => Sing (n :: nat) -> Sing m -> (S n * m) :~: ((n * m) + m)
+ Data.Type.Natural.Class.Arithmetic: multSuccL :: IsPeano nat => Sing (n :: nat) -> Sing m -> S n * m :~: n * m + m
- Data.Type.Natural.Class.Arithmetic: multSuccR :: IsPeano nat => Sing n -> Sing m -> (n * S m) :~: ((n * m) + (n :: nat))
+ Data.Type.Natural.Class.Arithmetic: multSuccR :: IsPeano nat => Sing n -> Sing m -> n * S m :~: n * m + (n :: nat)
- Data.Type.Natural.Class.Arithmetic: multZeroL :: IsPeano nat => Sing n -> (Zero nat * n) :~: Zero nat
+ Data.Type.Natural.Class.Arithmetic: multZeroL :: IsPeano nat => Sing n -> Zero nat * n :~: Zero nat
- Data.Type.Natural.Class.Arithmetic: multZeroR :: IsPeano nat => Sing n -> (n * Zero nat) :~: Zero nat
+ Data.Type.Natural.Class.Arithmetic: multZeroR :: IsPeano nat => Sing n -> n * Zero nat :~: Zero nat
- Data.Type.Natural.Class.Arithmetic: plusAssoc :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))
+ Data.Type.Natural.Class.Arithmetic: plusAssoc :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) + l :~: n + (m + l)
- Data.Type.Natural.Class.Arithmetic: plusComm :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: ((m :: nat) + n)
+ Data.Type.Natural.Class.Arithmetic: plusComm :: IsPeano nat => Sing n -> Sing m -> n + m :~: (m :: nat) + n
- Data.Type.Natural.Class.Arithmetic: plusCong :: n :~: m -> n' :~: m' -> (n + n') :~: (m + m')
+ Data.Type.Natural.Class.Arithmetic: plusCong :: n :~: m -> n' :~: m' -> n + n' :~: m + m'
- Data.Type.Natural.Class.Arithmetic: plusCongL :: n :~: m -> Sing k -> (n + k) :~: (m + k)
+ Data.Type.Natural.Class.Arithmetic: plusCongL :: n :~: m -> Sing k -> n + k :~: m + k
- Data.Type.Natural.Class.Arithmetic: plusCongR :: Sing k -> n :~: m -> (k + n) :~: (k + m)
+ Data.Type.Natural.Class.Arithmetic: plusCongR :: Sing k -> n :~: m -> k + n :~: k + m
- Data.Type.Natural.Class.Arithmetic: plusEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) :~: (n + l) -> m :~: l
+ Data.Type.Natural.Class.Arithmetic: plusEqCancelL :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n + m :~: n + l -> m :~: l
- Data.Type.Natural.Class.Arithmetic: plusEqCancelR :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + l) :~: (m + l) -> n :~: m
+ Data.Type.Natural.Class.Arithmetic: plusEqCancelR :: forall n m l. IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m + l -> n :~: m
- Data.Type.Natural.Class.Arithmetic: plusEqZeroL :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: Zero nat -> n :~: Zero nat
+ Data.Type.Natural.Class.Arithmetic: plusEqZeroL :: IsPeano nat => Sing n -> Sing m -> n + m :~: Zero nat -> n :~: Zero nat
- Data.Type.Natural.Class.Arithmetic: plusEqZeroR :: IsPeano nat => Sing n -> Sing m -> (n + m) :~: Zero nat -> m :~: Zero nat
+ Data.Type.Natural.Class.Arithmetic: plusEqZeroR :: IsPeano nat => Sing n -> Sing m -> n + m :~: Zero nat -> m :~: Zero nat
- Data.Type.Natural.Class.Arithmetic: plusMinus :: IsPeano nat => Sing (n :: nat) -> Sing m -> ((n + m) - m) :~: n
+ Data.Type.Natural.Class.Arithmetic: plusMinus :: IsPeano nat => Sing (n :: nat) -> Sing m -> n + m - m :~: n
- Data.Type.Natural.Class.Arithmetic: plusMinus' :: IsPeano nat => Sing (n :: nat) -> Sing m -> ((n + m) - n) :~: m
+ Data.Type.Natural.Class.Arithmetic: plusMinus' :: IsPeano nat => Sing (n :: nat) -> Sing m -> n + m - n :~: m
- Data.Type.Natural.Class.Arithmetic: plusMultDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))
+ Data.Type.Natural.Class.Arithmetic: plusMultDistrib :: IsPeano nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + m) * l :~: (n * l) + (m * l)
- Data.Type.Natural.Class.Arithmetic: plusSuccL :: IsPeano nat => Sing n -> Sing m -> (S n + m) :~: S (n + m :: nat)
+ Data.Type.Natural.Class.Arithmetic: plusSuccL :: IsPeano nat => Sing n -> Sing m -> S n + m :~: S (n + m :: nat)
- Data.Type.Natural.Class.Arithmetic: plusSuccR :: IsPeano nat => Sing n -> Sing m -> (n + S m) :~: S (n + m :: nat)
+ Data.Type.Natural.Class.Arithmetic: plusSuccR :: IsPeano nat => Sing n -> Sing m -> n + S m :~: S (n + m :: nat)
- Data.Type.Natural.Class.Arithmetic: succAndPlusOneL :: IsPeano nat => Sing n -> Succ n :~: (One nat + n)
+ Data.Type.Natural.Class.Arithmetic: succAndPlusOneL :: IsPeano nat => Sing n -> Succ n :~: One nat + n
- Data.Type.Natural.Class.Arithmetic: succAndPlusOneR :: IsPeano nat => Sing n -> Succ n :~: (n + One nat)
+ Data.Type.Natural.Class.Arithmetic: succAndPlusOneR :: IsPeano nat => Sing n -> Succ n :~: n + One nat
- Data.Type.Natural.Class.Arithmetic: type (*@#@$$$) a_al8e b_al8f = (:*$$$) a_al8e b_al8f
+ Data.Type.Natural.Class.Arithmetic: type (/=@#@$$$) (t :: a6989586621679288106) (t1 :: a6989586621679288106) = t /= t1
- Data.Type.Natural.Class.Order: (%<) :: forall nat_akRw (a_akRu :: nat_akRw) (b_akRv :: nat_akRw). SOrd nat_akRw => Sing a_akRu -> Sing b_akRv -> Sing ((<) a_akRu b_akRv)
+ Data.Type.Natural.Class.Order: (%<) :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply ((<@#@$) :: TyFun a TyFun a Bool -> Type -> *) t1 t2
- Data.Type.Natural.Class.Order: (%<=) :: forall nat_akVW (a_akVU :: nat_akVW) (b_akVV :: nat_akVW). SOrd nat_akVW => Sing a_akVU -> Sing b_akVV -> Sing ((<=) a_akVU b_akVV)
+ Data.Type.Natural.Class.Order: (%<=) :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply ((<=@#@$) :: TyFun a TyFun a Bool -> Type -> *) t1 t2
- Data.Type.Natural.Class.Order: (%>) :: forall nat_akUd (a_akUb :: nat_akUd) (b_akUc :: nat_akUd). SOrd nat_akUd => Sing a_akUb -> Sing b_akUc -> Sing ((>) a_akUb b_akUc)
+ Data.Type.Natural.Class.Order: (%>) :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply ((>@#@$) :: TyFun a TyFun a Bool -> Type -> *) t1 t2
- Data.Type.Natural.Class.Order: (%>=) :: forall nat_akXF (a_akXD :: nat_akXF) (b_akXE :: nat_akXF). SOrd nat_akXF => Sing a_akXD -> Sing b_akXE -> Sing ((>=) a_akXD b_akXE)
+ Data.Type.Natural.Class.Order: (%>=) :: SOrd a => Sing t1 -> Sing t2 -> Sing Apply Apply ((>=@#@$) :: TyFun a TyFun a Bool -> Type -> *) t1 t2
- Data.Type.Natural.Class.Order: leqStep :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing l -> (n + l) :~: m -> IsTrue (n <= m)
+ Data.Type.Natural.Class.Order: leqStep :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing l -> n + l :~: m -> IsTrue (n <= m)
- Data.Type.Natural.Class.Order: minPlusTruncMinus :: (PeanoOrder nat) => Sing (n :: nat) -> Sing (m :: nat) -> (Min n m + (n -. m)) :~: n
+ Data.Type.Natural.Class.Order: minPlusTruncMinus :: (PeanoOrder nat) => Sing (n :: nat) -> Sing (m :: nat) -> Min n m + (n -. m) :~: n
- Data.Type.Natural.Class.Order: minusPlus :: forall (n :: nat) m. (PeanoOrder nat, PeanoOrder nat) => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n
+ Data.Type.Natural.Class.Order: minusPlus :: forall (n :: nat) m. (PeanoOrder nat, PeanoOrder nat) => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> n - m + m :~: n
- Data.Type.Natural.Class.Order: minusSucc :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)
+ Data.Type.Natural.Class.Order: minusSucc :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Succ n - m :~: Succ (n - m)
- Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_aQLS :: Ordering). Sing t_aQLS -> Sing (Apply FlipOrderingSym0 t_aQLS :: Ordering)
+ Data.Type.Natural.Class.Order: sFlipOrdering :: forall (t_aNLp :: Ordering). Sing t_aNLp -> Sing (Apply FlipOrderingSym0 t_aNLp :: Ordering)
- Data.Type.Natural.Class.Order: type (*@#@$$$) a_al8e b_al8f = (:*$$$) a_al8e b_al8f
+ Data.Type.Natural.Class.Order: type (>=@#@$$$) (t :: a6989586621679299162) (t1 :: a6989586621679299162) = t >= t1
Files
- Data/Type/Natural.hs +12/−1
- type-natural.cabal +2/−2
Data/Type/Natural.hs view
@@ -31,7 +31,7 @@ -- * Conversion functions natToInt, intToNat, sNatToInt, -- * Quasi quotes for natural numbers- snat,+ nat, snat, -- * Properties of natural numbers IsPeano(..), plusCong, plusCongR, plusCongL,@@ -70,6 +70,7 @@ import Data.Type.Natural.Definitions hiding (type (<=)) import Data.Void import Language.Haskell.TH.Quote+import Language.Haskell.TH (conT, appT, conP, conE, appE) import Proof.Equational import Proof.Propositional hiding (Not) @@ -277,6 +278,16 @@ -------------------------------------------------- -- * Quasi Quoter --------------------------------------------------++-- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type.+--+-- for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@+nat :: QuasiQuoter+nat = QuasiQuoter { quoteExp = foldr appE (conE 'Z) . flip replicate (conE 'S) . read+ , quotePat = foldr (\a b -> conP a [b]) (conP 'Z []) . flip replicate 'S . read+ , quoteType = foldr appT (conT 'Z) . flip replicate (conT 'S) . read+ , quoteDec = error "not implemented"+ } -- | Quotesi-quoter for 'SNat'. This can be used for an expression. --
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.8.1.0+version: 0.8.2.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. .@@ -18,7 +18,7 @@ category: Math build-type: Simple cabal-version: >= 1.10-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1+tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3 source-repository head Type: git