Safe Haskell | None |
---|---|
Language | Haskell98 |
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 -> *)
- data family Sing a
- sZ :: SNat Z
- sS :: SNat n -> SNat (S n)
- min :: Ord a => a -> a -> a
- type family Min arg0 arg1 :: a0
- sMin :: SOrd a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 (MinSym0 a0) t0) t1)
- max :: Ord a => a -> a -> a
- type family Max arg0 arg1 :: a0
- sMax :: SOrd a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 (MaxSym0 a0) t0) t1)
- data MinSym0 l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *
- data MinSym1 l0 l1 :: a0 -> TyFun a0 a0 -> *
- type MinSym2 t0 t1 = Min a t0 t1
- data MaxSym0 l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *
- data MaxSym1 l0 l1 :: a0 -> TyFun a0 a0 -> *
- type MaxSym2 t0 t1 = Max a t0 t1
- type (:+:) n m = n :+ m
- type family arg0 :+ arg1 :: a0
- data (:+$) l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *
- data l0 :+$$ l1 :: a0 -> TyFun a0 a0 -> *
- type (:+$$$) t0 t1 = (:+) a0 t0 t1
- (%+) :: SNat n -> SNat m -> SNat (n :+: m)
- (%:+) :: SNum a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 ((:+$) a0) t0) t1)
- type family arg0 :* arg1 :: a0
- type (:*:) n m = n :* m
- data (:*$) l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *
- data l0 :*$$ l1 :: a0 -> TyFun a0 a0 -> *
- type (:*$$$) t0 t1 = (:*) a t0 t1
- (%:*) :: SNum a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 ((:*$) a0) t0) t1)
- (%*) :: SNat n -> SNat m -> SNat (n :*: m)
- type (:-:) n m = n :- m
- type family arg0 :- arg1 :: a0
- type (:**:) n m = n :** m
- type family a :** a :: Nat
- (%:**) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:**$) t) t :: Nat)
- (%**) :: SNat n -> SNat m -> SNat (n :**: m)
- data (:-$) l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *
- data l0 :-$$ l1 :: a0 -> TyFun a0 a0 -> *
- type (:-$$$) t0 t1 = (:-) a0 t0 t1
- (%:-) :: SNum a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 ((:-$) a0) t0) t1)
- (%-) :: ((m :<<= n) ~ True) => SNat n -> SNat m -> SNat (n :-: m)
- data Leq n m where
- class n :<= m
- type family a :<<= a :: Bool
- 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
- 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)
- succPlusR :: SNat n -> SNat m -> (n :+ S m) :=: S (n :+ m)
- plusZR :: SNat n -> (n :+: Z) :=: n
- plusZL :: SNat n -> (Z :+: n) :=: n
- eqPreservesS :: (n :=: m) -> S n :=: S m
- plusAssociative :: 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)
- 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
- 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))
- multPlusDistr :: 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)
- plusCommutative :: SNat n -> SNat m -> (n :+: m) :=: (m :+: n)
- minusCongEq :: (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
- type family One :: Nat
- type family Two :: Nat
- type family Three :: Nat
- type family Four :: Nat
- type family Five :: Nat
- type family Six :: Nat
- type family Seven :: Nat
- type family Eight :: Nat
- type family Nine :: Nat
- type family Ten :: Nat
- type family Eleven :: Nat
- type family Twelve :: Nat
- type family Thirteen :: Nat
- type family Fourteen :: Nat
- type family Fifteen :: Nat
- type family Sixteen :: Nat
- type family Seventeen :: Nat
- type family Eighteen :: Nat
- type family Nineteen :: Nat
- type family Twenty :: Nat
- 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
- type family N1 :: Nat
- type family N2 :: Nat
- type family N3 :: Nat
- type family N4 :: Nat
- type family N5 :: Nat
- type family N6 :: Nat
- type family N7 :: Nat
- type family N8 :: Nat
- type family N9 :: Nat
- type family N10 :: Nat
- type family N11 :: Nat
- type family N12 :: Nat
- type family N13 :: Nat
- type family N14 :: Nat
- type family N15 :: Nat
- type family N16 :: Nat
- type family N17 :: Nat
- type family N18 :: Nat
- type family N19 :: Nat
- type family N20 :: Nat
- 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 a
The singleton kind-indexed data family.
data Sing Bool where | |
data Sing Ordering where | |
data Sing Nat where | |
data Sing Symbol where
| |
data Sing () where | |
data Sing Nat where | |
type MonomorphicRep Nat (Sing Nat) = Int | |
data Sing [a0] where | |
data Sing (Maybe a0) where | |
data Sing (TyFun k1 k2 -> *) = SLambda {} | |
data Sing (Either a0 b0) where | |
data Sing ((,) a0 b0) where | |
data Sing ((,,) a0 b0 c0) where | |
data Sing ((,,,) a0 b0 c0 d0) where | |
data Sing ((,,,,) a0 b0 c0 d0 e0) where | |
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where | |
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where |
Smart constructors
WARNING: Smart constructors are deprecated as of singletons 0.10, so these are provided only for backward compatibility.
Deprecated: Smart constructors are no longer needed in singletons; Use SS
or SZ
instead.
sS :: SNat n -> SNat (S n) Source
Deprecated: Smart constructors are no longer needed in singletons; Use SS
or SZ
instead.
Arithmetic functions and their singletons.
type family Min arg0 arg1 :: a0
type Min Bool arg0 arg1 = Apply Bool Bool (Apply (TyFun Bool Bool -> *) Bool (Min_1627641698Sym0 Bool) arg0) arg1 | |
type Min Ordering arg0 arg1 = Apply Ordering Ordering (Apply (TyFun Ordering Ordering -> *) Ordering (Min_1627641698Sym0 Ordering) arg0) arg1 | |
type Min Nat arg0 arg1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat (Min_1627641698Sym0 Nat) arg0) arg1 | |
type Min Symbol arg0 arg1 = Apply Symbol Symbol (Apply (TyFun Symbol Symbol -> *) Symbol (Min_1627641698Sym0 Symbol) arg0) arg1 | |
type Min () arg0 arg1 = Apply () () (Apply (TyFun () () -> *) () (Min_1627641698Sym0 ()) arg0) arg1 | |
type Min Nat a0 a1 | |
type Min [a0] arg0 arg1 = Apply [a0] [a0] (Apply (TyFun [a0] [a0] -> *) [a0] (Min_1627641698Sym0 [a0]) arg0) arg1 | |
type Min (Maybe a0) arg0 arg1 = Apply (Maybe a0) (Maybe a0) (Apply (TyFun (Maybe a0) (Maybe a0) -> *) (Maybe a0) (Min_1627641698Sym0 (Maybe a0)) arg0) arg1 | |
type Min (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) (Either a0 b0) (Apply (TyFun (Either a0 b0) (Either a0 b0) -> *) (Either a0 b0) (Min_1627641698Sym0 (Either a0 b0)) arg0) arg1 | |
type Min ((,) a0 b0) arg0 arg1 = Apply ((,) a0 b0) ((,) a0 b0) (Apply (TyFun ((,) a0 b0) ((,) a0 b0) -> *) ((,) a0 b0) (Min_1627641698Sym0 ((,) a0 b0)) arg0) arg1 | |
type Min ((,,) a0 b0 c0) arg0 arg1 = Apply ((,,) a0 b0 c0) ((,,) a0 b0 c0) (Apply (TyFun ((,,) a0 b0 c0) ((,,) a0 b0 c0) -> *) ((,,) a0 b0 c0) (Min_1627641698Sym0 ((,,) a0 b0 c0)) arg0) arg1 | |
type Min ((,,,) a0 b0 c0 d0) arg0 arg1 = Apply ((,,,) a0 b0 c0 d0) ((,,,) a0 b0 c0 d0) (Apply (TyFun ((,,,) a0 b0 c0 d0) ((,,,) a0 b0 c0 d0) -> *) ((,,,) a0 b0 c0 d0) (Min_1627641698Sym0 ((,,,) a0 b0 c0 d0)) arg0) arg1 | |
type Min ((,,,,) a0 b0 c0 d0 e0) arg0 arg1 = Apply ((,,,,) a0 b0 c0 d0 e0) ((,,,,) a0 b0 c0 d0 e0) (Apply (TyFun ((,,,,) a0 b0 c0 d0 e0) ((,,,,) a0 b0 c0 d0 e0) -> *) ((,,,,) a0 b0 c0 d0 e0) (Min_1627641698Sym0 ((,,,,) a0 b0 c0 d0 e0)) arg0) arg1 | |
type Min ((,,,,,) a0 b0 c0 d0 e0 f0) arg0 arg1 = Apply ((,,,,,) a0 b0 c0 d0 e0 f0) ((,,,,,) a0 b0 c0 d0 e0 f0) (Apply (TyFun ((,,,,,) a0 b0 c0 d0 e0 f0) ((,,,,,) a0 b0 c0 d0 e0 f0) -> *) ((,,,,,) a0 b0 c0 d0 e0 f0) (Min_1627641698Sym0 ((,,,,,) a0 b0 c0 d0 e0 f0)) arg0) arg1 | |
type Min ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) arg0 arg1 = Apply ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) (Apply (TyFun ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) -> *) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) (Min_1627641698Sym0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0)) arg0) arg1 |
sMin :: SOrd a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 (MinSym0 a0) t0) t1)
type family Max arg0 arg1 :: a0
type Max Bool arg0 arg1 = Apply Bool Bool (Apply (TyFun Bool Bool -> *) Bool (Max_1627641665Sym0 Bool) arg0) arg1 | |
type Max Ordering arg0 arg1 = Apply Ordering Ordering (Apply (TyFun Ordering Ordering -> *) Ordering (Max_1627641665Sym0 Ordering) arg0) arg1 | |
type Max Nat arg0 arg1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat (Max_1627641665Sym0 Nat) arg0) arg1 | |
type Max Symbol arg0 arg1 = Apply Symbol Symbol (Apply (TyFun Symbol Symbol -> *) Symbol (Max_1627641665Sym0 Symbol) arg0) arg1 | |
type Max () arg0 arg1 = Apply () () (Apply (TyFun () () -> *) () (Max_1627641665Sym0 ()) arg0) arg1 | |
type Max Nat a0 a1 | |
type Max [a0] arg0 arg1 = Apply [a0] [a0] (Apply (TyFun [a0] [a0] -> *) [a0] (Max_1627641665Sym0 [a0]) arg0) arg1 | |
type Max (Maybe a0) arg0 arg1 = Apply (Maybe a0) (Maybe a0) (Apply (TyFun (Maybe a0) (Maybe a0) -> *) (Maybe a0) (Max_1627641665Sym0 (Maybe a0)) arg0) arg1 | |
type Max (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) (Either a0 b0) (Apply (TyFun (Either a0 b0) (Either a0 b0) -> *) (Either a0 b0) (Max_1627641665Sym0 (Either a0 b0)) arg0) arg1 | |
type Max ((,) a0 b0) arg0 arg1 = Apply ((,) a0 b0) ((,) a0 b0) (Apply (TyFun ((,) a0 b0) ((,) a0 b0) -> *) ((,) a0 b0) (Max_1627641665Sym0 ((,) a0 b0)) arg0) arg1 | |
type Max ((,,) a0 b0 c0) arg0 arg1 = Apply ((,,) a0 b0 c0) ((,,) a0 b0 c0) (Apply (TyFun ((,,) a0 b0 c0) ((,,) a0 b0 c0) -> *) ((,,) a0 b0 c0) (Max_1627641665Sym0 ((,,) a0 b0 c0)) arg0) arg1 | |
type Max ((,,,) a0 b0 c0 d0) arg0 arg1 = Apply ((,,,) a0 b0 c0 d0) ((,,,) a0 b0 c0 d0) (Apply (TyFun ((,,,) a0 b0 c0 d0) ((,,,) a0 b0 c0 d0) -> *) ((,,,) a0 b0 c0 d0) (Max_1627641665Sym0 ((,,,) a0 b0 c0 d0)) arg0) arg1 | |
type Max ((,,,,) a0 b0 c0 d0 e0) arg0 arg1 = Apply ((,,,,) a0 b0 c0 d0 e0) ((,,,,) a0 b0 c0 d0 e0) (Apply (TyFun ((,,,,) a0 b0 c0 d0 e0) ((,,,,) a0 b0 c0 d0 e0) -> *) ((,,,,) a0 b0 c0 d0 e0) (Max_1627641665Sym0 ((,,,,) a0 b0 c0 d0 e0)) arg0) arg1 | |
type Max ((,,,,,) a0 b0 c0 d0 e0 f0) arg0 arg1 = Apply ((,,,,,) a0 b0 c0 d0 e0 f0) ((,,,,,) a0 b0 c0 d0 e0 f0) (Apply (TyFun ((,,,,,) a0 b0 c0 d0 e0 f0) ((,,,,,) a0 b0 c0 d0 e0 f0) -> *) ((,,,,,) a0 b0 c0 d0 e0 f0) (Max_1627641665Sym0 ((,,,,,) a0 b0 c0 d0 e0 f0)) arg0) arg1 | |
type Max ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) arg0 arg1 = Apply ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) (Apply (TyFun ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) -> *) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) (Max_1627641665Sym0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0)) arg0) arg1 |
sMax :: SOrd a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 (MaxSym0 a0) t0) t1)
(%:+) :: SNum a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 ((:+$) a0) t0) t1)
(%:*) :: SNum a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 ((:*$) a0) t0) t1)
(%:-) :: SNum a0 kproxy0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply (TyFun a0 a0 -> *) a0 ((:-$) a0) t0) t1)
Type-level predicate & judgements
Comparison via GADTs.
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
type LeqTrueInstance a b = Dict ((a :<<= b) ~ True) 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 |])
Properties of natural numbers
snEqZAbsurd :: (S n :=: Z) -> a Source
multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l)) Source
Properties of ordering Leq
leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m Source
leqSnZAbsurd :: Leq (S n) Z -> a Source
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
sEleven :: Sing (ElevenSym0 :: Nat) Source
sTwelve :: Sing (TwelveSym0 :: Nat) Source
sThirteen :: Sing (ThirteenSym0 :: Nat) Source
sFourteen :: Sing (FourteenSym0 :: Nat) Source
sFifteen :: Sing (FifteenSym0 :: Nat) Source
sSixteen :: Sing (SixteenSym0 :: Nat) Source
sSeventeen :: Sing (SeventeenSym0 :: Nat) Source
sEighteen :: Sing (EighteenSym0 :: Nat) Source
sNineteen :: Sing (NineteenSym0 :: Nat) Source
sTwenty :: Sing (TwentySym0 :: Nat) Source