Data.Nat

data Nat

natPlus

natMul

type SNat z

data family Sing a

type family a :* a :: Nat

data (:*$) l

data l :*$$ l

type family a :+ a :: Nat

data (:+$) l

data l :+$$ l

data SSym0 l

type SSym1 t

type ZSym0

(%:+)

(%:*)

type family Lit n

type SLit n