Data.Nat

data Nat

(+)

(*)

type SNat z

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