Safe Haskell	Safe
Language	Haskell2010

Data.Type.Integer

Synopsis

Documentation

data PosNat Source #

Model positive natural numbers.

Constructors

PosNatOne
S PosNat

Instances

Eq PosNat Source #
Methods (==) :: PosNat -> PosNat -> Bool # (/=) :: PosNat -> PosNat -> Bool #
Show PosNat Source #
Methods showsPrec :: Int -> PosNat -> ShowS # show :: PosNat -> String # showList :: [PosNat] -> ShowS #

data Sign Source #

Model the signum of an integer.

Constructors

Minus
Plus

Instances

Eq Sign Source #
Methods (==) :: Sign -> Sign -> Bool # (/=) :: Sign -> Sign -> Bool #
Show Sign Source #
Methods showsPrec :: Int -> Sign -> ShowS # show :: Sign -> String # showList :: [Sign] -> ShowS #

data LiftedInt Source #

Model for type level integers: they are either zero or a positive natural number together with a sign.

Constructors

LIntZero
LInt Sign PosNat

Instances

Eq LiftedInt Source #
Methods (==) :: LiftedInt -> LiftedInt -> Bool # (/=) :: LiftedInt -> LiftedInt -> Bool #
Show LiftedInt Source #
Methods showsPrec :: Int -> LiftedInt -> ShowS # show :: LiftedInt -> String # showList :: [LiftedInt] -> ShowS #

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

Computes the successor for a type level integer.

Instances

type LIntSucc LIntZero Source #
type LIntSucc LIntZero = LInt Plus PosNatOne
type LIntSucc (LInt Minus PosNatOne) Source #
type LIntSucc (LInt Minus PosNatOne) = LIntZero
type LIntSucc (LInt Minus (S n)) Source #
type LIntSucc (LInt Minus (S n)) = LInt Minus n
type LIntSucc (LInt Plus n) Source #
type LIntSucc (LInt Plus n) = LInt Plus (S n)

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

Computes the predecessor for a type level integer.

Instances

type LIntPred LIntZero Source #
type LIntPred LIntZero = LInt Minus PosNatOne
type LIntPred (LInt Minus n) Source #
type LIntPred (LInt Minus n) = LInt Minus (S n)
type LIntPred (LInt Plus PosNatOne) Source #
type LIntPred (LInt Plus PosNatOne) = LIntZero
type LIntPred (LInt Plus (S n)) Source #
type LIntPred (LInt Plus (S n)) = LInt Plus n

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

Implement additive inversion for type level integers.

Instances

type LIntInvert LIntZero Source #
type LIntInvert LIntZero = LIntZero
type LIntInvert (LInt Minus n) Source #
type LIntInvert (LInt Minus n) = LInt Plus n
type LIntInvert (LInt Plus n) Source #
type LIntInvert (LInt Plus n) = LInt Minus n

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

Implement addition for type level integers.

Instances

type LIntPlus LIntZero n Source #
type LIntPlus LIntZero n = n
type LIntPlus (LInt Minus PosNatOne) n Source #
type LIntPlus (LInt Minus PosNatOne) n = LIntPred n
type LIntPlus (LInt Minus (S m)) n Source #
type LIntPlus (LInt Minus (S m)) n = LIntPlus (LInt Minus m) (LIntPred n)
type LIntPlus (LInt Plus PosNatOne) n Source #
type LIntPlus (LInt Plus PosNatOne) n = LIntSucc n
type LIntPlus (LInt Plus (S m)) n Source #
type LIntPlus (LInt Plus (S m)) n = LIntPlus (LInt Plus m) (LIntSucc n)

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

Implement subtraction for type level integers.

Instances

type LIntMinus m n Source #
type LIntMinus m n = LIntPlus m (LIntInvert n)

posNatVal :: forall n. KnownPosNat n => Proxy n -> Integer Source #

liftedIntVal :: forall i. KnownInt i => Proxy i -> Integer Source #

class KnownPosNat n Source #

Minimal complete definition

posNatSing

Instances

KnownPosNat PosNatOne Source #
Methods posNatSing :: SPosNat PosNatOne
KnownPosNat n => KnownPosNat (S n) Source #
Methods posNatSing :: SPosNat (S n)

class KnownInt n Source #

Minimal complete definition

intSing

Instances

KnownInt LIntZero Source #
Methods intSing :: SInt LIntZero
KnownPosNat n => KnownInt (LInt Minus n) Source #
Methods intSing :: SInt (LInt Minus n)
KnownPosNat n => KnownInt (LInt Plus n) Source #
Methods intSing :: SInt (LInt Plus n)