Data.Nat

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_6989586621679400878Sym0 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_6989586621679304448Sym0 Nat) arg) arg1

type Max Nat arg arg1

type Max Nat arg arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Max_6989586621679304415Sym0 Nat) arg) arg1

type (:>=) Nat arg arg1

type (:>=) Nat arg arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679304382Sym0 Nat) arg) arg1

type (:>) Nat arg arg1

type (:>) Nat arg arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679304349Sym0 Nat) arg) arg1

type (:<=) Nat arg arg1

type (:<=) Nat arg arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679304316Sym0 Nat) arg) arg1

type (:<) Nat arg arg1

type (:<) Nat arg arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_6989586621679304283Sym0 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))))