This Haskell package implements naive type level integers. It exposes
the module Data.Type.Integer
which exports a new kind LiftedInt
populated by the types Z
(zero) and LInt Sign PosNat
. In other
words, a (type level) integer is either zero or a positive natural
number together with a sign.
The module exports the type families LIntSucc
, LIntPred
,
LIntInvert
, LIntPlus
and LIntMinus
for manipulating types of
kind LiftedInt
.