Safe Haskell | None |
---|---|
Language | Haskell2010 |
Type level peano natural number, some arithmetic functions and their singletons.
- module Data.Singletons
- data Nat
- data SSym0 l
- type SSym1 t = S t
- type ZSym0 = Z
- type SNat = (Sing :: Nat -> Type)
- data family Sing k (a :: k) :: *
- min :: Ord a => a -> a -> a
- type family Min a0 (arg0 :: a0) (arg1 :: a0) :: a0
- sMin :: SOrd a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) (MinSym0 a0) t0) t1)
- max :: Ord a => a -> a -> a
- type family Max a0 (arg0 :: a0) (arg1 :: a0) :: a0
- sMax :: SOrd a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) (MaxSym0 a0) t0) t1)
- data MinSym0 a1627685414 l0 :: forall a1627685414. TyFun a1627685414 (TyFun a1627685414 a1627685414 -> Type) -> *
- data MinSym1 a1627685414 l0 l1 :: forall a1627685414. a1627685414 -> TyFun a1627685414 a1627685414 -> *
- type MinSym2 a1627685414 t0 t1 = Min a1627685414 t0 t1
- data MaxSym0 a1627685414 l0 :: forall a1627685414. TyFun a1627685414 (TyFun a1627685414 a1627685414 -> Type) -> *
- data MaxSym1 a1627685414 l0 l1 :: forall a1627685414. a1627685414 -> TyFun a1627685414 a1627685414 -> *
- type MaxSym2 a1627685414 t0 t1 = Max a1627685414 t0 t1
- type (:+:) n m = n :+ m
- type family (a0 :+ (arg0 :: a0)) (arg1 :: a0) :: a0
- data a1627805586 :+$ l0 :: forall a1627805586. TyFun a1627805586 (TyFun a1627805586 a1627805586 -> Type) -> *
- data (a1627805586 :+$$ l0) l1 :: forall a1627805586. a1627805586 -> TyFun a1627805586 a1627805586 -> *
- type (:+$$$) a1627805586 t0 t1 = (:+) a1627805586 t0 t1
- (%+) :: SNat n -> SNat m -> SNat (n :+: m)
- (%:+) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:+$) a0) t0) t1)
- type family (a0 :* (arg0 :: a0)) (arg1 :: a0) :: a0
- type (:*:) n m = n :* m
- data a1627805586 :*$ l0 :: forall a1627805586. TyFun a1627805586 (TyFun a1627805586 a1627805586 -> Type) -> *
- data (a1627805586 :*$$ l0) l1 :: forall a1627805586. a1627805586 -> TyFun a1627805586 a1627805586 -> *
- type (:*$$$) a1627805586 t0 t1 = (:*) a1627805586 t0 t1
- (%:*) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:*$) a0) t0) t1)
- (%*) :: SNat n -> SNat m -> SNat (n :*: m)
- type (:-:) n m = n :- m
- type family (a0 :- (arg0 :: a0)) (arg1 :: a0) :: a0
- type (:**:) n m = n :** m
- type family (a :: Nat) :** (a :: Nat) :: Nat where ...
- (%:**) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:**$) t) t :: Nat)
- (%**) :: SNat n -> SNat m -> SNat (n :**: m)
- data a1627805586 :-$ l0 :: forall a1627805586. TyFun a1627805586 (TyFun a1627805586 a1627805586 -> Type) -> *
- data (a1627805586 :-$$ l0) l1 :: forall a1627805586. a1627805586 -> TyFun a1627805586 a1627805586 -> *
- type (:-$$$) a1627805586 t0 t1 = (:-) a1627805586 t0 t1
- (%:-) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:-$) a0) t0) t1)
- (%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)
- data Leq n m where
- class n :<= m
- type family (a :: Nat) :<<= (a :: Nat) :: Bool where ...
- data (:<<=$) l
- data l :<<=$$ l
- type (:<<=$$$) t t = (:<<=) t t
- (%:<<=) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:<<=$) t) t :: Bool)
- type LeqInstance n m = Dict (n :<= m)
- boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
- boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
- propToClassLeq :: Leq n m -> LeqInstance n m
- type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)
- propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m
- natToInt :: Integral n => Nat -> n
- intToNat :: (Integral a, Ord a) => a -> Nat
- sNatToInt :: Num n => SNat x -> n
- nat :: QuasiQuoter
- snat :: QuasiQuoter
- succCongEq :: (n :=: m) -> S n :=: S m
- eqPreservesS :: (n :=: m) -> S n :=: S m
- succCong :: (n :=: m) -> S n :=: S m
- plusCongR :: SNat n -> (m :=: m') -> (m :+ n) :=: (m' :+ n)
- plusCongL :: SNat n -> (m :=: m') -> (n :+ m) :=: (n :+ m')
- succPlusL :: SNat n -> SNat m -> (S n :+ m) :=: S (n :+ m)
- plusSuccL :: SNat n -> SNat m -> (S n :+ m) :=: S (n :+ m)
- succPlusR :: SNat n -> SNat m -> (n :+ S m) :=: S (n :+ m)
- plusSuccR :: SNat n -> SNat m -> (n :+ S m) :=: S (n :+ m)
- plusZR :: SNat n -> (n :+: Z) :=: n
- plusZL :: SNat n -> (Z :+: n) :=: n
- plusAssociative :: SNat n -> SNat m -> SNat l -> (n :+: (m :+: l)) :=: ((n :+: m) :+: l)
- plusAssoc :: SNat n -> SNat m -> SNat l -> (n :+: (m :+: l)) :=: ((n :+: m) :+: l)
- multAssociative :: SNat n -> SNat m -> SNat l -> (n :* (m :* l)) :=: ((n :* m) :* l)
- multAssoc :: SNat n -> SNat m -> SNat l -> (n :* (m :* l)) :=: ((n :* m) :* l)
- multComm :: SNat n -> SNat m -> (n :* m) :=: (m :* n)
- multZL :: SNat m -> (Zero :* m) :=: Zero
- multZR :: SNat m -> (m :* Zero) :=: Zero
- multOneL :: SNat n -> (One :* n) :=: n
- multOneR :: SNat n -> (n :* One) :=: n
- snEqZAbsurd :: (S n :=: Z) -> a
- succInjective :: (S n :=: S m) -> n :=: m
- succInj :: (S n :=: S m) -> n :=: m
- plusInjectiveL :: SNat n -> SNat m -> SNat l -> ((n :+ m) :=: (n :+ l)) -> m :=: l
- plusInjectiveR :: SNat n -> SNat m -> SNat l -> ((n :+ l) :=: (m :+ l)) -> n :=: m
- plusMultDistr :: SNat n -> SNat m -> SNat l -> ((n :+ m) :* l) :=: ((n :* l) :+ (m :* l))
- plusMultDistrib :: SNat n -> SNat m -> SNat l -> ((n :+ m) :* l) :=: ((n :* l) :+ (m :* l))
- multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l))
- multPlusDistrib :: forall n m l. SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l))
- multCongL :: SNat n -> (m :=: l) -> (n :* m) :=: (n :* l)
- multCongR :: SNat n -> (m :=: l) -> (m :* n) :=: (l :* n)
- sAndPlusOne :: SNat n -> S n :=: (n :+: One)
- succAndPlusOneR :: SNat n -> S n :=: (n :+: One)
- plusComm :: SNat n -> SNat m -> (n :+: m) :=: (m :+: n)
- plusCommutative :: SNat n -> SNat m -> (n :+: m) :=: (m :+: n)
- minusCongEq :: (n :=: m) -> SNat l -> (n :-: l) :=: (m :-: l)
- minusCongL :: (n :=: m) -> SNat l -> (n :-: l) :=: (m :-: l)
- minusNilpotent :: SNat n -> (n :-: n) :=: Zero
- eqSuccMinus :: (m :<<= n) ~ True => SNat n -> SNat m -> (S n :-: m) :=: S (n :-: m)
- plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n
- plusMinusEqR :: SNat n -> SNat m -> ((m :+: n) :-: m) :=: n
- zAbsorbsMinR :: SNat n -> Min n Z :=: Z
- zAbsorbsMinL :: SNat n -> Min Z n :=: Z
- plusSR :: SNat n -> SNat m -> S (n :+: m) :=: (n :+: S m)
- plusNeutralR :: SNat n -> SNat m -> ((n :+ m) :=: n) -> m :=: Z
- plusNeutralL :: SNat n -> SNat m -> ((n :+ m) :=: m) -> n :=: Z
- leqRhs :: Leq n m -> SNat m
- leqLhs :: Leq n m -> SNat n
- minComm :: SNat n -> SNat m -> Min n m :=: Min m n
- maxZL :: SNat n -> Max Z n :=: n
- maxComm :: SNat n -> SNat m -> Max n m :=: Max m n
- maxZR :: SNat n -> Max n Z :=: n
- leqRefl :: SNat n -> Leq n n
- leqSucc :: SNat n -> Leq n (S n)
- leqTrans :: Leq n m -> Leq m l -> Leq n l
- plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)
- plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)
- plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
- minLeqL :: SNat n -> SNat m -> Leq (Min n m) n
- minLeqR :: SNat n -> SNat m -> Leq (Min n m) m
- leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m
- maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)
- maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)
- leqSnZAbsurd :: Leq (S n) Z -> a
- leqnZElim :: Leq n Z -> n :=: Z
- leqSnLeq :: Leq (S n) m -> Leq n m
- leqPred :: Leq (S n) (S m) -> Leq n m
- leqSnnAbsurd :: Leq (S n) n -> a
- zero :: Nat
- one :: Nat
- two :: Nat
- three :: Nat
- four :: Nat
- five :: Nat
- six :: Nat
- seven :: Nat
- eight :: Nat
- nine :: Nat
- ten :: Nat
- eleven :: Nat
- twelve :: Nat
- thirteen :: Nat
- fourteen :: Nat
- fifteen :: Nat
- sixteen :: Nat
- seventeen :: Nat
- eighteen :: Nat
- nineteen :: Nat
- twenty :: Nat
- type family Zero :: Nat where ...
- type family One :: Nat where ...
- type family Two :: Nat where ...
- type family Three :: Nat where ...
- type family Four :: Nat where ...
- type family Five :: Nat where ...
- type family Six :: Nat where ...
- type family Seven :: Nat where ...
- type family Eight :: Nat where ...
- type family Nine :: Nat where ...
- type family Ten :: Nat where ...
- type family Eleven :: Nat where ...
- type family Twelve :: Nat where ...
- type family Thirteen :: Nat where ...
- type family Fourteen :: Nat where ...
- type family Fifteen :: Nat where ...
- type family Sixteen :: Nat where ...
- type family Seventeen :: Nat where ...
- type family Eighteen :: Nat where ...
- type family Nineteen :: Nat where ...
- type family Twenty :: Nat where ...
- type ZeroSym0 = Zero
- type OneSym0 = One
- type TwoSym0 = Two
- type ThreeSym0 = Three
- type FourSym0 = Four
- type FiveSym0 = Five
- type SixSym0 = Six
- type SevenSym0 = Seven
- type EightSym0 = Eight
- type NineSym0 = Nine
- type TenSym0 = Ten
- type ElevenSym0 = Eleven
- type TwelveSym0 = Twelve
- type ThirteenSym0 = Thirteen
- type FourteenSym0 = Fourteen
- type FifteenSym0 = Fifteen
- type SixteenSym0 = Sixteen
- type SeventeenSym0 = Seventeen
- type EighteenSym0 = Eighteen
- type NineteenSym0 = Nineteen
- type TwentySym0 = Twenty
- sZero :: Sing (ZeroSym0 :: Nat)
- sOne :: Sing (OneSym0 :: Nat)
- sTwo :: Sing (TwoSym0 :: Nat)
- sThree :: Sing (ThreeSym0 :: Nat)
- sFour :: Sing (FourSym0 :: Nat)
- sFive :: Sing (FiveSym0 :: Nat)
- sSix :: Sing (SixSym0 :: Nat)
- sSeven :: Sing (SevenSym0 :: Nat)
- sEight :: Sing (EightSym0 :: Nat)
- sNine :: Sing (NineSym0 :: Nat)
- sTen :: Sing (TenSym0 :: Nat)
- sEleven :: Sing (ElevenSym0 :: Nat)
- sTwelve :: Sing (TwelveSym0 :: Nat)
- sThirteen :: Sing (ThirteenSym0 :: Nat)
- sFourteen :: Sing (FourteenSym0 :: Nat)
- sFifteen :: Sing (FifteenSym0 :: Nat)
- sSixteen :: Sing (SixteenSym0 :: Nat)
- sSeventeen :: Sing (SeventeenSym0 :: Nat)
- sEighteen :: Sing (EighteenSym0 :: Nat)
- sNineteen :: Sing (NineteenSym0 :: Nat)
- sTwenty :: Sing (TwentySym0 :: Nat)
- n0 :: Nat
- n1 :: Nat
- n2 :: Nat
- n3 :: Nat
- n4 :: Nat
- n5 :: Nat
- n6 :: Nat
- n7 :: Nat
- n8 :: Nat
- n9 :: Nat
- n10 :: Nat
- n11 :: Nat
- n12 :: Nat
- n13 :: Nat
- n14 :: Nat
- n15 :: Nat
- n16 :: Nat
- n17 :: Nat
- n18 :: Nat
- n19 :: Nat
- n20 :: Nat
- type family N0 :: Nat where ...
- type family N1 :: Nat where ...
- type family N2 :: Nat where ...
- type family N3 :: Nat where ...
- type family N4 :: Nat where ...
- type family N5 :: Nat where ...
- type family N6 :: Nat where ...
- type family N7 :: Nat where ...
- type family N8 :: Nat where ...
- type family N9 :: Nat where ...
- type family N10 :: Nat where ...
- type family N11 :: Nat where ...
- type family N12 :: Nat where ...
- type family N13 :: Nat where ...
- type family N14 :: Nat where ...
- type family N15 :: Nat where ...
- type family N16 :: Nat where ...
- type family N17 :: Nat where ...
- type family N18 :: Nat where ...
- type family N19 :: Nat where ...
- type family N20 :: Nat where ...
- type N0Sym0 = N0
- type N1Sym0 = N1
- type N2Sym0 = N2
- type N3Sym0 = N3
- type N4Sym0 = N4
- type N5Sym0 = N5
- type N6Sym0 = N6
- type N7Sym0 = N7
- type N8Sym0 = N8
- type N9Sym0 = N9
- type N10Sym0 = N10
- type N11Sym0 = N11
- type N12Sym0 = N12
- type N13Sym0 = N13
- type N14Sym0 = N14
- type N15Sym0 = N15
- type N16Sym0 = N16
- type N17Sym0 = N17
- type N18Sym0 = N18
- type N19Sym0 = N19
- type N20Sym0 = N20
- sN0 :: Sing (N0Sym0 :: Nat)
- sN1 :: Sing (N1Sym0 :: Nat)
- sN2 :: Sing (N2Sym0 :: Nat)
- sN3 :: Sing (N3Sym0 :: Nat)
- sN4 :: Sing (N4Sym0 :: Nat)
- sN5 :: Sing (N5Sym0 :: Nat)
- sN6 :: Sing (N6Sym0 :: Nat)
- sN7 :: Sing (N7Sym0 :: Nat)
- sN8 :: Sing (N8Sym0 :: Nat)
- sN9 :: Sing (N9Sym0 :: Nat)
- sN10 :: Sing (N10Sym0 :: Nat)
- sN11 :: Sing (N11Sym0 :: Nat)
- sN12 :: Sing (N12Sym0 :: Nat)
- sN13 :: Sing (N13Sym0 :: Nat)
- sN14 :: Sing (N14Sym0 :: Nat)
- sN15 :: Sing (N15Sym0 :: Nat)
- sN16 :: Sing (N16Sym0 :: Nat)
- sN17 :: Sing (N17Sym0 :: Nat)
- sN18 :: Sing (N18Sym0 :: Nat)
- sN19 :: Sing (N19Sym0 :: Nat)
- sN20 :: Sing (N20Sym0 :: Nat)
Re-exported modules.
module Data.Singletons
Natural Numbers
Peano natural numbers. It will be promoted to the type-level natural number.
Singleton type for Nat
.
data family Sing k (a :: k) :: * #
The singleton kind-indexed data family.
data Sing Bool | |
data Sing Ordering | |
data Sing Nat | |
data Sing Symbol | |
data Sing () | |
data Sing Nat # | |
type MonomorphicRep Nat (Sing Nat) # | |
data Sing [a0] | |
data Sing (Maybe a0) | |
data Sing (NonEmpty a0) | |
data Sing (Either a0 b0) | |
data Sing (a0, b0) | |
data Sing ((~>) k1 k2) | |
data Sing (a0, b0, c0) | |
data Sing (a0, b0, c0, d0) | |
data Sing (a0, b0, c0, d0, e0) | |
data Sing (a0, b0, c0, d0, e0, f0) | |
data Sing (a0, b0, c0, d0, e0, f0, g0) | |
Arithmetic functions and their singletons.
type family Min a0 (arg0 :: a0) (arg1 :: a0) :: a0 #
type Min Bool arg0 arg1 | |
type Min Ordering arg0 arg1 | |
type Min Nat arg0 arg1 | |
type Min Symbol arg0 arg1 | |
type Min () arg0 arg1 | |
type Min Nat a1 a0 # | |
type Min [a0] arg0 arg1 | |
type Min (Maybe a0) arg0 arg1 | |
type Min (NonEmpty a0) arg0 arg1 | |
type Min (Either a0 b0) arg0 arg1 | |
type Min (a0, b0) arg0 arg1 | |
type Min (a0, b0, c0) arg0 arg1 | |
type Min (a0, b0, c0, d0) arg0 arg1 | |
type Min (a0, b0, c0, d0, e0) arg0 arg1 | |
type Min (a0, b0, c0, d0, e0, f0) arg0 arg1 | |
type Min (a0, b0, c0, d0, e0, f0, g0) arg0 arg1 | |
sMin :: SOrd a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) (MinSym0 a0) t0) t1) #
type family Max a0 (arg0 :: a0) (arg1 :: a0) :: a0 #
type Max Bool arg0 arg1 | |
type Max Ordering arg0 arg1 | |
type Max Nat arg0 arg1 | |
type Max Symbol arg0 arg1 | |
type Max () arg0 arg1 | |
type Max Nat a1 a0 # | |
type Max [a0] arg0 arg1 | |
type Max (Maybe a0) arg0 arg1 | |
type Max (NonEmpty a0) arg0 arg1 | |
type Max (Either a0 b0) arg0 arg1 | |
type Max (a0, b0) arg0 arg1 | |
type Max (a0, b0, c0) arg0 arg1 | |
type Max (a0, b0, c0, d0) arg0 arg1 | |
type Max (a0, b0, c0, d0, e0) arg0 arg1 | |
type Max (a0, b0, c0, d0, e0, f0) arg0 arg1 | |
type Max (a0, b0, c0, d0, e0, f0, g0) arg0 arg1 | |
sMax :: SOrd a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) (MaxSym0 a0) t0) t1) #
data MinSym0 a1627685414 l0 :: forall a1627685414. TyFun a1627685414 (TyFun a1627685414 a1627685414 -> Type) -> * #
data MinSym1 a1627685414 l0 l1 :: forall a1627685414. a1627685414 -> TyFun a1627685414 a1627685414 -> * #
data MaxSym0 a1627685414 l0 :: forall a1627685414. TyFun a1627685414 (TyFun a1627685414 a1627685414 -> Type) -> * #
data MaxSym1 a1627685414 l0 l1 :: forall a1627685414. a1627685414 -> TyFun a1627685414 a1627685414 -> * #
data a1627805586 :+$ l0 :: forall a1627805586. TyFun a1627805586 (TyFun a1627805586 a1627805586 -> Type) -> * #
data (a1627805586 :+$$ l0) l1 :: forall a1627805586. a1627805586 -> TyFun a1627805586 a1627805586 -> * #
(%:+) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:+$) a0) t0) t1) #
data a1627805586 :*$ l0 :: forall a1627805586. TyFun a1627805586 (TyFun a1627805586 a1627805586 -> Type) -> * #
data (a1627805586 :*$$ l0) l1 :: forall a1627805586. a1627805586 -> TyFun a1627805586 a1627805586 -> * #
(%:*) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:*$) a0) t0) t1) #
data a1627805586 :-$ l0 :: forall a1627805586. TyFun a1627805586 (TyFun a1627805586 a1627805586 -> Type) -> * #
data (a1627805586 :-$$ l0) l1 :: forall a1627805586. a1627805586 -> TyFun a1627805586 a1627805586 -> * #
(%:-) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:-$) a0) t0) t1) #
Type-level predicate & judgements
Comparison via GADTs.
Comparison via type-class.
type family (a :: Nat) :<<= (a :: Nat) :: Bool where ... Source #
Boolean-valued type-level comparison function.
type LeqInstance n m = Dict (n :<= m) Source #
boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m Source #
propToClassLeq :: Leq n m -> LeqInstance n m Source #
propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m Source #
Conversion functions
Quasi quotes for natural numbers
nat :: QuasiQuoter Source #
Quotesi-quoter for Nat
. This can be used for an expression, pattern and type.
for example: sing :: SNat ([nat| 2 |] :+ [nat| 5 |])
snat :: QuasiQuoter Source #
Properties of natural numbers
succCongEq :: (n :=: m) -> S n :=: S m Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.succCong
eqPreservesS :: (n :=: m) -> S n :=: S m Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.succCong
succPlusL :: SNat n -> SNat m -> (S n :+ m) :=: S (n :+ m) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.plusSuccL
succPlusR :: SNat n -> SNat m -> (n :+ S m) :=: S (n :+ m) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.plusSuccR
plusAssociative :: SNat n -> SNat m -> SNat l -> (n :+: (m :+: l)) :=: ((n :+: m) :+: l) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.plusAssoc
multAssociative :: SNat n -> SNat m -> SNat l -> (n :* (m :* l)) :=: ((n :* m) :* l) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.multAssoc
succInjective :: (S n :=: S m) -> n :=: m Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.succInj
plusMultDistr :: SNat n -> SNat m -> SNat l -> ((n :+ m) :* l) :=: ((n :* l) :+ (m :* l)) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.plusMultDistrib
plusMultDistrib :: SNat n -> SNat m -> SNat l -> ((n :+ m) :* l) :=: ((n :* l) :+ (m :* l)) Source #
multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l)) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.multPlusDistrib
multPlusDistrib :: forall n m l. SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l)) Source #
sAndPlusOne :: SNat n -> S n :=: (n :+: One) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.succAndPlusOneR
plusCommutative :: SNat n -> SNat m -> (n :+: m) :=: (m :+: n) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.plusComm
minusCongEq :: (n :=: m) -> SNat l -> (n :-: l) :=: (m :-: l) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.minusCongL
plusSR :: SNat n -> SNat m -> S (n :+: m) :=: (n :+: S m) Source #
Deprecated: Will be removed in 0.5.0.0
. Use
instead.plusSuccR
Properties of ordering Leq
leqSnnAbsurd :: Leq (S n) n -> a Source #
Useful type synonyms and constructors
type ElevenSym0 = Eleven Source #
type TwelveSym0 = Twelve Source #
type ThirteenSym0 = Thirteen Source #
type FourteenSym0 = Fourteen Source #
type FifteenSym0 = Fifteen Source #
type SixteenSym0 = Sixteen Source #
type SeventeenSym0 = Seventeen Source #
type EighteenSym0 = Eighteen Source #
type NineteenSym0 = Nineteen Source #
type TwentySym0 = Twenty Source #
sSeventeen :: Sing (SeventeenSym0 :: Nat) Source #