Basement.Nat

data Nat

class KnownNat n

natVal

type x <= y

type family (a :: Nat) <=? (b :: Nat) :: Bool where ...

type family (a :: Nat) + (b :: Nat) :: Nat where ...

type family (a :: Nat) * (b :: Nat) :: Nat where ...

type family (a :: Nat) ^ (b :: Nat) :: Nat where ...

type family (a :: Nat) - (b :: Nat) :: Nat where ...

type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...

# Nat convertion

natValNatural

natValInt

natValInt8

natValInt16

natValInt32

natValInt64

natValWord

natValWord8

natValWord16

natValWord32

natValWord64

# Maximum bounds

type family NatNumMaxBound ty :: Nat

# Constraint

type family NatInBoundOf ty n where ...

type family NatWithinBound ty (n :: Nat) where ...