Data.Type.Integer

data PosNat

data Sign

data LiftedInt

type family LIntSucc (k :: LiftedInt) :: LiftedInt

type family LIntPred (k :: LiftedInt) :: LiftedInt

type family LIntInvert (k :: LiftedInt) :: LiftedInt

type family LIntPlus (k :: LiftedInt) (l :: LiftedInt) :: LiftedInt

type family LIntMinus (k :: LiftedInt) (l :: LiftedInt) :: LiftedInt

posNatVal

liftedIntVal

class KnownPosNat n

class KnownInt n