GHC.TypeLits

Kinds

data Nat

data Symbol

Linking type and value level

data family Sing n

class SingI a

class SingE kparam rep

class SingRep a rep

unsafeSingNat

unsafeSingSymbol

type Kind

Working with singletons

withSing

singThat

Functions on type nats

class m (<=) n

type family m (<=?) n :: Bool

type family m (+) n :: Nat

type family m (*) n :: Nat

type family m (^) n :: Nat

Destructing type-nats.

isZero

data IsZero

isEven

data IsEven