Safe Haskell	None
Language	Haskell2010

Data.Nat

Synopsis

Documentation

data Nat #

Constructors

Z
S Nat

Instances

Eq Nat #
Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Ord Nat #
Methods compare :: Nat -> Nat -> Ordering # (<) :: Nat -> Nat -> Bool # (<=) :: Nat -> Nat -> Bool # (>) :: Nat -> Nat -> Bool # (>=) :: Nat -> Nat -> Bool # max :: Nat -> Nat -> Nat # min :: Nat -> Nat -> Nat #
Show Nat #
Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
PNum Nat #
Associated Types type (Nat :+ (arg :: Nat)) (arg1 :: Nat) :: a # type (Nat :- (arg :: Nat)) (arg1 :: Nat) :: a # type (Nat :* (arg :: Nat)) (arg1 :: Nat) :: a # type Negate Nat (arg :: Nat) :: a # type Abs Nat (arg :: Nat) :: a # type Signum Nat (arg :: Nat) :: a # type FromInteger Nat (arg :: Nat) :: a #
SNum Nat #
Methods (%:+) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t1) t2) # (%:-) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t1) t2) # (%:) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:$) Nat) t1) t2) # sNegate :: Sing Nat t -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t) # sAbs :: Sing Nat t -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t) # sSignum :: Sing Nat t -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t) # sFromInteger :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t) #
POrd Nat #
Associated Types type Compare Nat (arg :: Nat) (arg1 :: Nat) :: Ordering # type (Nat :< (arg :: Nat)) (arg1 :: Nat) :: Bool # type (Nat :<= (arg :: Nat)) (arg1 :: Nat) :: Bool # type (Nat :> (arg :: Nat)) (arg1 :: Nat) :: Bool # type (Nat :>= (arg :: Nat)) (arg1 :: Nat) :: Bool # type Max Nat (arg :: Nat) (arg1 :: Nat) :: a # type Min Nat (arg :: Nat) (arg1 :: Nat) :: a #
SOrd Nat => SOrd Nat #
Methods sCompare :: Sing Nat t1 -> Sing Nat t2 -> Sing Ordering (Apply Nat Ordering (Apply Nat (TyFun Nat Ordering -> Type) (CompareSym0 Nat) t1) t2) # (%:<) :: Sing Nat t1 -> Sing Nat t2 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:<$) Nat) t1) t2) # (%:<=) :: Sing Nat t1 -> Sing Nat t2 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:<=$) Nat) t1) t2) # (%:>) :: Sing Nat t1 -> Sing Nat t2 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:>$) Nat) t1) t2) # (%:>=) :: Sing Nat t1 -> Sing Nat t2 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:>=$) Nat) t1) t2) # sMax :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (MaxSym0 Nat) t1) t2) # sMin :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (MinSym0 Nat) t1) t2) #
SEq Nat #
Methods (%:==) :: Sing Nat a -> Sing Nat b -> Sing Bool ((Nat :== a) b) # (%:/=) :: Sing Nat a -> Sing Nat b -> Sing Bool ((Nat :/= a) b) #
PEq Nat #
Associated Types type (Nat :== (x :: Nat)) (y :: Nat) :: Bool # type (Nat :/= (x :: Nat)) (y :: Nat) :: Bool #
SDecide Nat #
Methods (%~) :: Sing Nat a -> Sing Nat b -> Decision ((Nat :~: a) b) #
SingKind Nat #
Associated Types type Demote Nat = (r :: *) # Methods fromSing :: Sing Nat a -> Demote Nat # toSing :: Demote Nat -> SomeSing Nat #
SingI Nat Z #
Methods sing :: Sing Z a #
SingI Nat n => SingI Nat (S n) #
Methods sing :: Sing (S n) a #
Eq (SNat n) #
Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) #
Methods compare :: SNat n -> SNat n -> Ordering # (<) :: SNat n -> SNat n -> Bool # (<=) :: SNat n -> SNat n -> Bool # (>) :: SNat n -> SNat n -> Bool # (>=) :: SNat n -> SNat n -> Bool # max :: SNat n -> SNat n -> SNat n # min :: SNat n -> SNat n -> SNat n #
Show (Sing Nat n) #
Methods showsPrec :: Int -> Sing Nat n -> ShowS # show :: Sing Nat n -> String # showList :: [Sing Nat n] -> ShowS #
SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 #
Methods suppressUnusedWarnings :: Proxy SSym0 t -> () #
data Sing Nat #
data Sing Nat where SZ :: Sing Nat z SS :: Sing Nat z
type Demote Nat #
type Demote Nat = Nat
type FromInteger Nat a #
type FromInteger Nat a = Lit a
type Signum Nat a #
type Signum Nat a = Error Symbol Nat "Data.Nat: signum not implemented"
type Abs Nat a #
type Abs Nat a = NatAbs a
type Negate Nat arg #
type Negate Nat arg = Apply Nat Nat (Negate_6989586621679658425Sym0 Nat) arg
type (:*) Nat a b #
type (:*) Nat a b = NatMul a b
type (:-) Nat a b #
type (:-) Nat a b = NatMinus a b
type (:+) Nat a b #
type (:+) Nat a b = NatPlus a b
type Min Nat arg arg1 #
type Min Nat arg arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Min_6989586621679571879Sym0 Nat) arg) arg1
type Max Nat arg arg1 #
type Max Nat arg arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Max_6989586621679571846Sym0 Nat) arg) arg1
type (:>=) Nat arg arg1 #
type (:>=) Nat arg arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679571813Sym0 Nat) arg) arg1
type (:>) Nat arg arg1 #
type (:>) Nat arg arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679571780Sym0 Nat) arg) arg1
type (:<=) Nat arg arg1 #
type (:<=) Nat arg arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679571747Sym0 Nat) arg) arg1
type (:<) Nat arg arg1 #
type (:<) Nat arg arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679571714Sym0 Nat) arg) arg1
type Compare Nat a1 a2 #
type Compare Nat a1 a2
type (:/=) Nat x y #
type (:/=) Nat x y = Not ((:==) Nat x y)
type (:==) Nat a b #
type (:==) Nat a b
type Apply Nat Nat SSym0 l #
type Apply Nat Nat SSym0 l = S l

type family NatPlus (a :: Nat) (a :: Nat) :: Nat where ... #

Equations

NatPlus Z b = b
NatPlus (S a) b = Apply SSym0 (Apply (Apply NatPlusSym0 a) b)

type family NatMul (a :: Nat) (a :: Nat) :: Nat where ... #

Equations

NatMul Z b = ZSym0
NatMul (S a) b = Apply (Apply NatPlusSym0 b) (Apply (Apply NatMulSym0 a) b)

type family NatMinus (a :: Nat) (a :: Nat) :: Nat where ... #

Equations

NatMinus Z b = ZSym0
NatMinus (S a) (S b) = Apply (Apply NatMinusSym0 a) b
NatMinus a Z = a

type family NatAbs (a :: Nat) :: Nat where ... #

Equations

NatAbs n = n

natPlus :: Nat -> Nat -> Nat #

natMul :: Nat -> Nat -> Nat #

natMinus :: Nat -> Nat -> Nat #

natAbs :: Nat -> Nat #

type SNat = (Sing :: Nat -> Type) #

data family Sing k (a :: k) :: * #

The singleton kind-indexed data family.

Instances

Eq (SNat n) #
Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) #
Methods compare :: SNat n -> SNat n -> Ordering # (<) :: SNat n -> SNat n -> Bool # (<=) :: SNat n -> SNat n -> Bool # (>) :: SNat n -> SNat n -> Bool # (>=) :: SNat n -> SNat n -> Bool # max :: SNat n -> SNat n -> SNat n # min :: SNat n -> SNat n -> SNat n #
Show (Sing Nat n) #
Methods showsPrec :: Int -> Sing Nat n -> ShowS # show :: Sing Nat n -> String # showList :: [Sing Nat n] -> ShowS #
data Sing Bool
data Sing Bool where SFalse :: Sing Bool z STrue :: Sing Bool z
data Sing Ordering
data Sing Ordering where SLT :: Sing Ordering z SEQ :: Sing Ordering z SGT :: Sing Ordering z
data Sing Nat
data Sing Nat where SNat :: Sing Nat n
data Sing Symbol
data Sing Symbol where SSym :: Sing Symbol n
data Sing ()
data Sing () where STuple0 :: Sing () z
data Sing Nat #
data Sing Nat where SZ :: Sing Nat z SS :: Sing Nat z
data Sing [a]
data Sing [a] where SNil :: Sing [a] z SCons :: Sing [a] z
data Sing (Maybe a)
data Sing (Maybe a) where SNothing :: Sing (Maybe a) z SJust :: Sing (Maybe a) z
data Sing (NonEmpty a)
data Sing (NonEmpty a) where (:%\|) :: Sing (NonEmpty a) z
data Sing (Either a b)
data Sing (Either a b) where SLeft :: Sing (Either a b) z SRight :: Sing (Either a b) z
data Sing (a, b)
data Sing (a, b) where STuple2 :: Sing (a, b) z
data Sing ((~>) k1 k2)
data Sing ((~>) k1 k2) = SLambda { applySing :: forall (t :: k1). Sing k1 t -> Sing k2 ((@@) k1 k2 f t) }
data Sing (a, b, c)
data Sing (a, b, c) where STuple3 :: Sing (a, b, c) z
data Sing (a, b, c, d)
data Sing (a, b, c, d) where STuple4 :: Sing (a, b, c, d) z
data Sing (a, b, c, d, e)
data Sing (a, b, c, d, e) where STuple5 :: Sing (a, b, c, d, e) z
data Sing (a, b, c, d, e, f)
data Sing (a, b, c, d, e, f) where STuple6 :: Sing (a, b, c, d, e, f) z
data Sing (a, b, c, d, e, f, g)
data Sing (a, b, c, d, e, f, g) where STuple7 :: Sing (a, b, c, d, e, f, g) z

class PNum a #

Instances

PNum Nat
Associated Types type (Nat :+ (arg :: Nat)) (arg1 :: Nat) :: a # type (Nat :- (arg :: Nat)) (arg1 :: Nat) :: a # type (Nat :* (arg :: Nat)) (arg1 :: Nat) :: a # type Negate Nat (arg :: Nat) :: a # type Abs Nat (arg :: Nat) :: a # type Signum Nat (arg :: Nat) :: a # type FromInteger Nat (arg :: Nat) :: a #
PNum Nat #
Associated Types type (Nat :+ (arg :: Nat)) (arg1 :: Nat) :: a # type (Nat :- (arg :: Nat)) (arg1 :: Nat) :: a # type (Nat :* (arg :: Nat)) (arg1 :: Nat) :: a # type Negate Nat (arg :: Nat) :: a # type Abs Nat (arg :: Nat) :: a # type Signum Nat (arg :: Nat) :: a # type FromInteger Nat (arg :: Nat) :: a #

class SNum a #

Minimal complete definition

(%:+), (%:*), sAbs, sSignum, sFromInteger

Instances

SNum Nat
Methods (%:+) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t1) t2) # (%:-) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t1) t2) # (%:) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:$) Nat) t1) t2) # sNegate :: Sing Nat t -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t) # sAbs :: Sing Nat t -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t) # sSignum :: Sing Nat t -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t) # sFromInteger :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t) #
SNum Nat #
Methods (%:+) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t1) t2) # (%:-) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t1) t2) # (%:) :: Sing Nat t1 -> Sing Nat t2 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:$) Nat) t1) t2) # sNegate :: Sing Nat t -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t) # sAbs :: Sing Nat t -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t) # sSignum :: Sing Nat t -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t) # sFromInteger :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t) #

data SSym0 (l :: TyFun Nat Nat) #

Constructors

SameKind (Apply SSym0 arg) (SSym1 arg) => SSym0KindInference

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 #
Methods suppressUnusedWarnings :: Proxy SSym0 t -> () #
type Apply Nat Nat SSym0 l #
type Apply Nat Nat SSym0 l = S l

type SSym1 (t :: Nat) = S t #

type ZSym0 = Z #

type family Lit n where ... #

Provides a shorthand for Nat-s using GHC.TypeLits, for example:

>>> :kind! Lit 3
Lit 3 :: Nat
= 'S ('S ('S 'Z))

Equations

Lit 0 = Z
Lit n = S (Lit (n - 1))

type SLit n = Sing (Lit n) #

sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n) #

Shorthand for SNat literals using TypeApplications.

>>> :set -XTypeApplications
>>> sLit @5
SS (SS (SS (SS (SS SZ))))