Safe Haskell	None
Language	Haskell2010

Data.Nat

Synopsis

Documentation

data Nat Source #

Constructors

Z
S Nat

Instances

Eq Nat Source #
Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Ord Nat Source #
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 Source #
Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #
SNum Nat Source #
Methods (%:+) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t0) t1) # (%:-) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t0) t1) # (%:) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:$) Nat) t0) t1) # sNegate :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t0) # sAbs :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t0) # sSignum :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t0) # sFromInteger :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t0) #
SOrd Nat => SOrd Nat Source #
Methods sCompare :: Sing Nat t0 -> Sing Nat t1 -> Sing Ordering (Apply Nat Ordering (Apply Nat (TyFun Nat Ordering -> Type) (CompareSym0 Nat) t0) t1) # (%:<) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:<$) Nat) t0) t1) # (%:<=) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:<=$) Nat) t0) t1) # (%:>) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:>$) Nat) t0) t1) # (%:>=) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:>=$) Nat) t0) t1) # sMax :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (MaxSym0 Nat) t0) t1) # sMin :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (MinSym0 Nat) t0) t1) #
SEq Nat Source #
Methods (%:==) :: Sing Nat a -> Sing Nat b -> Sing Bool ((Nat :== a) b) # (%:/=) :: Sing Nat a -> Sing Nat b -> Sing Bool ((Nat :/= a) b) #
SDecide Nat Source #
Methods (%~) :: Sing Nat a -> Sing Nat b -> Decision ((Nat :~: a) b) #
SingKind Nat Source #
Associated Types type DemoteRep Nat :: * # Methods fromSing :: Sing Nat a -> DemoteRep Nat # toSing :: DemoteRep Nat -> SomeSing Nat #
SingI Nat Z Source #
Methods sing :: Sing Z a #
SingI Nat n0 => SingI Nat (S n0) Source #
Methods sing :: Sing (S n0) a #
PNum Nat (Proxy * Nat) Source #
Associated Types type ((Proxy * Nat) :+ (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type ((Proxy * Nat) :- (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type ((Proxy * Nat) :* (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type Negate (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type Abs (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type Signum (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type FromInteger (Proxy * Nat) (arg0 :: Nat) :: a0 #
POrd Nat (Proxy * Nat) Source #
Associated Types type Compare (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: Ordering # type ((Proxy * Nat) :< (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool # type ((Proxy * Nat) :<= (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool # type ((Proxy * Nat) :> (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool # type ((Proxy * Nat) :>= (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool # type Max (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: a0 # type Min (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: a0 #
PEq Nat (Proxy * Nat) Source #
Associated Types type ((Proxy * Nat) :== (x :: Proxy * Nat)) (y :: Proxy * Nat) :: Bool # type ((Proxy * Nat) :/= (x :: Proxy * Nat)) (y :: Proxy * Nat) :: Bool #
Eq (SNat n) Source #
Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) Source #
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) Source #
Methods showsPrec :: Int -> Sing Nat n -> ShowS # show :: Sing Nat n -> String # showList :: [Sing Nat n] -> ShowS #
SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 Source #
Methods suppressUnusedWarnings :: Proxy SSym0 t -> () #
data Sing Nat Source #
data Sing Nat where SZ :: Sing Nat z SS :: Sing Nat z
type DemoteRep Nat Source #
type DemoteRep Nat = Nat
type FromInteger Nat a Source #
type FromInteger Nat a = Lit a
type Signum Nat a Source #
type Signum Nat a = Error Nat Symbol "Data.Nat: signum not implemented"
type Abs Nat a Source #
type Abs Nat a = NatAbs a
type Negate Nat arg0 Source #
type Negate Nat arg0 = Apply Nat Nat (Negate_6989586621679425771Sym0 Nat) arg0
type (:*) Nat a b Source #
type (:*) Nat a b = NatMul a b
type (:-) Nat a b Source #
type (:-) Nat a b = NatMinus a b
type (:+) Nat a b Source #
type (:+) Nat a b = NatPlus a b
type Min Nat arg0 arg1 Source #
type Min Nat arg0 arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Min_6989586621679308019Sym0 Nat) arg0) arg1
type Max Nat arg0 arg1 Source #
type Max Nat arg0 arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Max_6989586621679307986Sym0 Nat) arg0) arg1
type (:>=) Nat arg0 arg1 Source #
type (:>=) Nat arg0 arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679307953Sym0 Nat) arg0) arg1
type (:>) Nat arg0 arg1 Source #
type (:>) Nat arg0 arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679307920Sym0 Nat) arg0) arg1
type (:<=) Nat arg0 arg1 Source #
type (:<=) Nat arg0 arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679307887Sym0 Nat) arg0) arg1
type (:<) Nat arg0 arg1 Source #
type (:<) Nat arg0 arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679307854Sym0 Nat) arg0) arg1
type Compare Nat a1 a0 Source #
type Compare Nat a1 a0
type (:/=) Nat x y Source #
type (:/=) Nat x y = Not ((:==) Nat x y)
type (:==) Nat a0 b0 Source #
type (:==) Nat a0 b0
type Apply Nat Nat SSym0 l0 Source #
type Apply Nat Nat SSym0 l0 = SSym1 l0

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

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 ... Source #

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 ... Source #

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 ... Source #

Equations

NatAbs n = n

natPlus :: Nat -> Nat -> Nat Source #

natMul :: Nat -> Nat -> Nat Source #

natMinus :: Nat -> Nat -> Nat Source #

natAbs :: Nat -> Nat Source #

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

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 z0 STrue :: Sing Bool z0
data Sing Ordering
data Sing Ordering where SLT :: Sing Ordering z0 SEQ :: Sing Ordering z0 SGT :: Sing Ordering z0
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 () z0
data Sing Nat #
data Sing Nat where SZ :: Sing Nat z SS :: Sing Nat z
data Sing [a0]
data Sing [a0] where SNil :: Sing [a0] z0 SCons :: Sing [a0] z0
data Sing (Maybe a0)
data Sing (Maybe a0) where SNothing :: Sing (Maybe a0) z0 SJust :: Sing (Maybe a0) z0
data Sing (NonEmpty a0)
data Sing (NonEmpty a0) where (:%\|) :: Sing (NonEmpty a0) z0
data Sing (Either a0 b0)
data Sing (Either a0 b0) where SLeft :: Sing (Either a0 b0) z0 SRight :: Sing (Either a0 b0) z0
data Sing (a0, b0)
data Sing (a0, b0) where STuple2 :: Sing (a0, b0) z0
data Sing ((~>) k1 k2)
data Sing ((~>) k1 k2) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t) }
data Sing (a0, b0, c0)
data Sing (a0, b0, c0) where STuple3 :: Sing (a0, b0, c0) z0
data Sing (a0, b0, c0, d0)
data Sing (a0, b0, c0, d0) where STuple4 :: Sing (a0, b0, c0, d0) z0
data Sing (a0, b0, c0, d0, e0)
data Sing (a0, b0, c0, d0, e0) where STuple5 :: Sing (a0, b0, c0, d0, e0) z0
data Sing (a0, b0, c0, d0, e0, f0)
data Sing (a0, b0, c0, d0, e0, f0) where STuple6 :: Sing (a0, b0, c0, d0, e0, f0) z0
data Sing (a0, b0, c0, d0, e0, f0, g0)
data Sing (a0, b0, c0, d0, e0, f0, g0) where STuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

class (~) (Proxy * a0) kproxy0 (Proxy * a0) => PNum a0 kproxy0 #

Instances

PNum Nat (Proxy * Nat)
Associated Types type ((Proxy * Nat) :+ (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type ((Proxy * Nat) :- (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type ((Proxy * Nat) :* (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type Negate (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type Abs (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type Signum (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type FromInteger (Proxy * Nat) (arg0 :: Nat) :: a0 #
PNum Nat (Proxy * Nat) #
Associated Types type ((Proxy * Nat) :+ (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type ((Proxy * Nat) :- (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type ((Proxy * Nat) :* (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0 # type Negate (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type Abs (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type Signum (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0 # type FromInteger (Proxy * Nat) (arg0 :: Nat) :: a0 #

class SNum a0 #

Minimal complete definition

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

Instances

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

data SSym0 l Source #

Constructors

(KindOf (Apply SSym0 arg) ~ KindOf (SSym1 arg)) => SSym0KindInference

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 Source #
Methods suppressUnusedWarnings :: Proxy SSym0 t -> () #
type Apply Nat Nat SSym0 l0 Source #
type Apply Nat Nat SSym0 l0 = SSym1 l0

type SSym1 t = S t Source #

type ZSym0 = Z Source #

type family Lit n where ... Source #

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) Source #

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

Shorthand for SNat literals using TypeApplications.

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