Safe Haskell	None
Language	Haskell2010

Data.Nat

Synopsis

Documentation

data Nat Source

Constructors

Z
S Nat

Instances

Eq Nat Source
Ord Nat Source
Show Nat Source
SingI Nat Z Source
PNum Nat (KProxy Nat) Source
SNum Nat (KProxy Nat) Source
POrd Nat (KProxy Nat) Source
SOrd Nat (KProxy Nat) => SOrd Nat (KProxy Nat) Source
SEq Nat (KProxy Nat) Source
PEq Nat (KProxy Nat) Source
SDecide Nat (KProxy Nat) Source
SingI Nat n0 => SingI Nat (S n) Source
SingKind Nat (KProxy Nat) Source
SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 Source
data Sing Nat where SZ :: (~) Nat z Z => Sing Nat z SS :: (~) Nat z (S n) => Sing Nat n -> Sing Nat z Source
type FromInteger Nat a = Lit a Source
type Signum Nat a = Error Nat Symbol "Data.Nat: signum not implemented" Source
type Abs Nat a = NatAbs a Source
type Negate Nat arg0 = Apply Nat Nat (Negate_1627753622Sym0 Nat) arg0
type (:*) Nat a b = NatMul a b Source
type (:-) Nat a b = NatMinus a b Source
type (:+) Nat a b = NatPlus a b Source
type Min Nat arg0 arg1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat (Min_1627641704Sym0 Nat) arg0) arg1
type Max Nat arg0 arg1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat (Max_1627641671Sym0 Nat) arg0) arg1
type (:>=) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641638Sym0 Nat) arg0) arg1
type (:>) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641605Sym0 Nat) arg0) arg1
type (:<=) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641572Sym0 Nat) arg0) arg1
type (:<) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641539Sym0 Nat) arg0) arg1
type Compare Nat a0 a1 Source
type (:/=) Nat x y = Not ((:==) Nat x y)
type (:==) Nat a0 b0 Source
type Apply Nat Nat SSym0 l0 = SSym1 l0 Source
type DemoteRep Nat (KProxy Nat) = Nat Source

type family NatPlus a a :: Nat Source

Equations

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

type family NatMul a a :: Nat Source

Equations

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

type family NatMinus a a :: Nat 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 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 -> *) Source

data family Sing a

The singleton kind-indexed data family.

Instances

data Sing Bool where SFalse :: (~) Bool z0 False => Sing Bool z0 STrue :: (~) Bool z0 True => Sing Bool z0
data Sing Ordering where SLT :: (~) Ordering z0 LT => Sing Ordering z0 SEQ :: (~) Ordering z0 EQ => Sing Ordering z0 SGT :: (~) Ordering z0 GT => Sing Ordering z0
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z0 () => Sing () z0
data Sing Nat where SZ :: (~) Nat z Z => Sing Nat z SS :: (~) Nat z (S n) => Sing Nat n -> Sing Nat z
data Sing [a0] where SNil :: (~) [a0] z0 ([] a0) => Sing [a0] z0 SCons :: (~) [a0] z0 ((:) a0 n0 n1) => Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0
data Sing (Maybe a0) where SNothing :: (~) (Maybe a0) z0 (Nothing a0) => Sing (Maybe a0) z0 SJust :: (~) (Maybe a0) z0 (Just a0 n0) => Sing a0 n0 -> Sing (Maybe a0) z0
data Sing (TyFun k1 k2 -> *) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t) }
data Sing (Either a0 b0) where SLeft :: (~) (Either a0 b0) z0 (Left a0 b0 n0) => Sing a0 n0 -> Sing (Either a0 b0) z0 SRight :: (~) (Either a0 b0) z0 (Right a0 b0 n0) => Sing b0 n0 -> Sing (Either a0 b0) z0
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a0 b0) z0 ((,) a0 b0 n0 n1) => Sing a0 n0 -> Sing b0 n1 -> Sing ((,) a0 b0) z0
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a0 b0 c0) z0 ((,,) a0 b0 c0 n0 n1 n2) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing ((,,) a0 b0 c0) z0
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a0 b0 c0 d0) z0 ((,,,) a0 b0 c0 d0 n0 n1 n2 n3) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing ((,,,) a0 b0 c0 d0) z0
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0

class (~) (KProxy a0) kproxy0 (KProxy a0) => PNum kproxy0

Instances

PNum Nat (KProxy Nat)
PNum Nat (KProxy Nat)

class (~) (KProxy a0) kproxy0 (KProxy a0) => SNum kproxy0

Minimal complete definition

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

Instances

SNum Nat (KProxy Nat)
SNum Nat (KProxy Nat)

data SSym0 l Source

Constructors

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

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 Source
type Apply Nat Nat SSym0 l0 = SSym1 l0 Source

type SSym1 t = S t Source

type ZSym0 = Z Source

type family Lit n 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