KindInteger

This module provides a type-level representation for term-level Integers. This type-level representation is also named Integer, So import this module qualified to avoid name conflicts.

import KindInteger qualified as KI

The implementation details are similar to the ones for type-level Naturals as of base-4.18 and singletons-base-3.1.1, and they will continue to evolve together with base and singletons-base, trying to more or less follow their API.

Integer

data Integer

Type-level version of Integer, only used as a kind.

• Zero is represented as Z.
• A positive number +x is represented as P x.
• A negative number -x is represented as N x.

Instances

SingKind Integer

Defined in KindInteger

Associated Types

type Demote Integer = (r :: Type)

Methods

fromSing :: forall (a :: Integer). Sing a -> Demote Integer

toSing :: Demote Integer -> SomeSing Integer

SDecide Integer

Defined in KindInteger

Methods

(%~) :: forall (a :: Integer) (b :: Integer). Sing a -> Sing b -> Decision (a :~: b)

PEq Integer

Defined in KindInteger

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

SEq Integer

Defined in KindInteger

Methods

(%==) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) t1) t2)

POrd Integer

Defined in KindInteger

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

SOrd Integer

Defined in KindInteger

Methods

sCompare :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

PNum Integer

Defined in KindInteger

Associated Types

type arg + arg1 :: a

type arg - arg1 :: a

type arg * arg1 :: a

type Negate arg :: a

type Abs arg :: a

type Signum arg :: a

type FromInteger arg :: a

SNum Integer

Defined in KindInteger

Methods

(%+) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)

(%-) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)

(%*) :: forall (t1 :: Integer) (t2 :: Integer). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)

sNegate :: forall (t :: Integer). Sing t -> Sing (Apply NegateSym0 t)

sAbs :: forall (t :: Integer). Sing t -> Sing (Apply AbsSym0 t)

sSignum :: forall (t :: Integer). Sing t -> Sing (Apply SignumSym0 t)

sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t)

PShow Integer

Displays i as it would show literally as a term.

Show_ ( N 1) ~ "-1"
Show_   Z    ~  "0"
Show_ ( P 1) ~  "1"

N 0 and P 0 fail to type-check.

Defined in KindInteger

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg1 :: Symbol

SShow Integer

Displays i as it would show literally as a term.

fromSing @(sShow_ (SN (sing @1))) == "-1"
fromSing @(sShow_ SZ)             ==  "0"
fromSing @(sShow_ (SP (sing @1))) ==  "1"

Defined in KindInteger

Methods

sShowsPrec :: forall (t1 :: Natural) (t2 :: Integer) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: forall (t :: Integer). Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: forall (t1 :: [Integer]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

TestCoercion SInteger

Defined in KindInteger

Methods

testCoercion :: forall (a :: k) (b :: k). SInteger a -> SInteger b -> Maybe (Coercion a b)

TestEquality SInteger

Defined in KindInteger

Methods

testEquality :: forall (a :: k) (b :: k). SInteger a -> SInteger b -> Maybe (a :~: b)

KnownInteger i => SingI (i :: Integer)

Defined in KindInteger

Methods

sing :: Sing i

type Demote Integer

Defined in KindInteger

type Demote Integer = Integer

type Sing

Defined in KindInteger

type Sing = SInteger

type Abs (i :: Integer)

Defined in KindInteger

type Abs (i :: Integer) = FromNatural (Abs i)

type FromInteger i

Defined in KindInteger

type FromInteger i = FromNatural i

type Negate (i :: Integer)

Defined in KindInteger

type Negate (i :: Integer) = Fold Z PSym0 NSym0 i

type Signum (i :: Integer)

Defined in KindInteger

type Signum (i :: Integer) = Fold Z (ConstSym1 (N 1) :: TyFun Natural Integer -> Type) (ConstSym1 (P 1) :: TyFun Natural Integer -> Type) i

type Show_ (arg :: Integer)

Defined in KindInteger

type Show_ (arg :: Integer) = Apply (Show__6989586621680028698Sym0 :: TyFun Integer Symbol -> Type) arg

type Compare (l :: Integer) (r :: Integer)

Defined in KindInteger

type Compare (l :: Integer) (r :: Integer)

type (arg :: Integer) /= (arg1 :: Integer)

Defined in KindInteger

type (arg :: Integer) /= (arg1 :: Integer) = Apply (Apply (TFHelper_6989586621679140582Sym0 :: TyFun Integer (Integer ~> Bool) -> Type) arg) arg1

type (a :: Integer) == (b :: Integer)

Defined in KindInteger

type (a :: Integer) == (b :: Integer) = OrdCond (Compare a b) 'False 'True 'False

type (arg :: Integer) < (arg1 :: Integer)

Defined in KindInteger

type (arg :: Integer) < (arg1 :: Integer) = Apply (Apply (TFHelper_6989586621679338501Sym0 :: TyFun Integer (Integer ~> Bool) -> Type) arg) arg1

type (arg :: Integer) <= (arg1 :: Integer)

Defined in KindInteger

type (arg :: Integer) <= (arg1 :: Integer) = Apply (Apply (TFHelper_6989586621679338543Sym0 :: TyFun Integer (Integer ~> Bool) -> Type) arg) arg1

type (arg :: Integer) > (arg1 :: Integer)

Defined in KindInteger

type (arg :: Integer) > (arg1 :: Integer) = Apply (Apply (TFHelper_6989586621679338562Sym0 :: TyFun Integer (Integer ~> Bool) -> Type) arg) arg1

type (arg :: Integer) >= (arg1 :: Integer)

Defined in KindInteger

type (arg :: Integer) >= (arg1 :: Integer) = Apply (Apply (TFHelper_6989586621679338578Sym0 :: TyFun Integer (Integer ~> Bool) -> Type) arg) arg1

type Compare (l :: Integer) (r :: Integer)

Defined in KindInteger

type Compare (l :: Integer) (r :: Integer) = Compare l r

type Max (arg :: Integer) (arg1 :: Integer)

Defined in KindInteger

type Max (arg :: Integer) (arg1 :: Integer) = Apply (Apply (Max_6989586621679338594Sym0 :: TyFun Integer (Integer ~> Integer) -> Type) arg) arg1

type Min (arg :: Integer) (arg1 :: Integer)

Defined in KindInteger

type Min (arg :: Integer) (arg1 :: Integer) = Apply (Apply (Min_6989586621679338610Sym0 :: TyFun Integer (Integer ~> Integer) -> Type) arg) arg1

type (l :: Integer) * (r :: Integer)

Defined in KindInteger

type (l :: Integer) * (r :: Integer)

type (l :: Integer) + (r :: Integer)

Defined in KindInteger

type (l :: Integer) + (r :: Integer)

type (l :: Integer) - (r :: Integer)

Defined in KindInteger

type (l :: Integer) - (r :: Integer) = l + Negate r

type ShowList (arg :: [Integer]) arg1

Defined in KindInteger

type ShowList (arg :: [Integer]) arg1 = Apply (Apply (ShowList_6989586621680028706Sym0 :: TyFun [Integer] (Symbol ~> Symbol) -> Type) arg) arg1

type Apply NormalizedSym0 (i :: Integer)

Defined in KindInteger

type Apply NormalizedSym0 (i :: Integer) = Normalized i

type Apply Log2Sym0 (a :: Integer)

Defined in KindInteger

type Apply Log2Sym0 (a :: Integer) = Log2Sym1 a

type Apply EvenSym0 (i :: Integer)

Defined in KindInteger

type Apply EvenSym0 (i :: Integer) = Even i

type Apply OddSym0 (i :: Integer)

Defined in KindInteger

type Apply OddSym0 (i :: Integer) = Odd i

type Apply KnownIntegerSym0 (i :: Integer)

Defined in KindInteger

type Apply KnownIntegerSym0 (i :: Integer) = KnownIntegerSym1 i

type Apply ShowLitSym0 (i :: Integer)

Defined in KindInteger

type Apply ShowLitSym0 (i :: Integer) = ShowLitSym1 i

type Apply FromNaturalSym0 (i :: Natural)

Defined in KindInteger

type Apply FromNaturalSym0 (i :: Natural) = FromNatural i

type Apply NSym0 (x :: Natural)

Defined in KindInteger

type Apply NSym0 (x :: Natural) = NSym1 x

type Apply PSym0 (x :: Natural)

Defined in KindInteger

type Apply PSym0 (x :: Natural) = PSym1 x

type ShowsPrec p (i :: Integer) s

Defined in KindInteger

type ShowsPrec p (i :: Integer) s

type Apply (GCDSym1 a :: TyFun Integer Natural -> Type) (b :: Integer)

Defined in KindInteger

type Apply (GCDSym1 a :: TyFun Integer Natural -> Type) (b :: Integer)

type Apply (LCMSym1 a :: TyFun Integer Natural -> Type) (b :: Integer)

Defined in KindInteger

type Apply (LCMSym1 a :: TyFun Integer Natural -> Type) (b :: Integer)

type Apply ((^@#@$$) b :: TyFun Natural Integer -> Type) (p :: Natural)

Defined in KindInteger

type Apply ((^@#@$$) b :: TyFun Natural Integer -> Type) (p :: Natural) = b ^@#@$$$ p

type Apply (DivSym2 r a :: TyFun Integer Integer -> Type) (b :: Integer)

Defined in KindInteger

type Apply (DivSym2 r a :: TyFun Integer Integer -> Type) (b :: Integer) = DivSym3 r a b

type Apply (RemSym2 r a :: TyFun Integer Integer -> Type) (b :: Integer)

Defined in KindInteger

type Apply (RemSym2 r a :: TyFun Integer Integer -> Type) (b :: Integer) = RemSym3 r a b

type Apply (FoldSym3 z n p :: TyFun Integer k -> Type) (i :: Integer)

Defined in KindInteger

type Apply (FoldSym3 z n p :: TyFun Integer k -> Type) (i :: Integer) = FoldSym4 z n p i

type Apply GCDSym0 (a :: Integer)

Defined in KindInteger

type Apply GCDSym0 (a :: Integer) = GCDSym1 a

type Apply LCMSym0 (a :: Integer)

Defined in KindInteger

type Apply LCMSym0 (a :: Integer) = LCMSym1 a

type Apply (^@#@$) (b :: Integer)

Defined in KindInteger

type Apply (^@#@$) (b :: Integer) = (^@#@$$) b

type Apply ShowsLitSym0 (i :: Integer)

Defined in KindInteger

type Apply ShowsLitSym0 (i :: Integer) = ShowsLitSym1 i

type Apply DivSym0 (r :: Round)

Defined in KindInteger

type Apply DivSym0 (r :: Round) = DivSym1 r

type Apply RemSym0 (r :: Round)

Defined in KindInteger

type Apply RemSym0 (r :: Round) = RemSym1 r

type Apply DivRemSym0 (r :: Round)

Defined in KindInteger

type Apply DivRemSym0 (r :: Round) = DivRemSym1 r

type Apply ShowsPrecLitSym0 (p :: Natural)

Defined in KindInteger

type Apply ShowsPrecLitSym0 (p :: Natural) = ShowsPrecLitSym1 p

type Apply (DivSym1 r :: TyFun Integer (Integer ~> Integer) -> Type) (a :: Integer)

Defined in KindInteger

type Apply (DivSym1 r :: TyFun Integer (Integer ~> Integer) -> Type) (a :: Integer) = DivSym2 r a

type Apply (RemSym1 r :: TyFun Integer (Integer ~> Integer) -> Type) (a :: Integer)

Defined in KindInteger

type Apply (RemSym1 r :: TyFun Integer (Integer ~> Integer) -> Type) (a :: Integer) = RemSym2 r a

type Apply (DivRemSym1 r :: TyFun Integer (Integer ~> (Integer, Integer)) -> Type) (a :: Integer)

Defined in KindInteger

type Apply (DivRemSym1 r :: TyFun Integer (Integer ~> (Integer, Integer)) -> Type) (a :: Integer) = DivRemSym2 r a

type Apply (ShowsPrecLitSym1 p :: TyFun Integer (Symbol ~> Symbol) -> Type) (i :: Integer)

Defined in KindInteger

type Apply (ShowsPrecLitSym1 p :: TyFun Integer (Symbol ~> Symbol) -> Type) (i :: Integer) = ShowsPrecLitSym2 p i

type Apply (FoldSym0 :: TyFun k ((Natural ~> k) ~> ((Natural ~> k) ~> (Integer ~> k))) -> Type) (z :: k)

Defined in KindInteger

type Apply (FoldSym0 :: TyFun k ((Natural ~> k) ~> ((Natural ~> k) ~> (Integer ~> k))) -> Type) (z :: k) = FoldSym1 z

type Apply (DivRemSym2 r a :: TyFun Integer (Integer, Integer) -> Type) (b :: Integer)

Defined in KindInteger

type Apply (DivRemSym2 r a :: TyFun Integer (Integer, Integer) -> Type) (b :: Integer) = DivRemSym3 r a b

type Apply (FoldSym1 z :: TyFun (Natural ~> k) ((Natural ~> k) ~> (Integer ~> k)) -> Type) (n :: Natural ~> k)

Defined in KindInteger

type Apply (FoldSym1 z :: TyFun (Natural ~> k) ((Natural ~> k) ~> (Integer ~> k)) -> Type) (n :: Natural ~> k) = FoldSym2 z n

type Apply (FoldSym2 z n :: TyFun (Natural ~> k) (Integer ~> k) -> Type) (p :: Natural ~> k)

Defined in KindInteger

type Apply (FoldSym2 z n :: TyFun (Natural ~> k) (Integer ~> k) -> Type) (p :: Natural ~> k) = FoldSym3 z n p

type Z = 'Z :: Integer

Zero is represented as Z.

pattern SZ :: SInteger Z

SZ == sing @Z

type N (x :: Natural) = 'N x :: Integer

A negative number -x is represented as N x.

While a standalone N 0 type-checks, it is not considered valid, so tools like KnownInteger or Normalized will reject it. N 0 itself is not rejected so that it can be used to pattern-match against Integers at the type-level if necessary.

pattern SN :: 0 < x => (KnownInteger (N x), KnownNat x) => Sing (x :: Natural) -> SInteger (N x)

SN (sing @1) == sing @(N 1)

type P (x :: Natural) = 'P x :: Integer

A positive number +x is represented as P x.

While a standalone P 0 type-checks, it is not considered valid, so tools like KnownInteger or Normalized will reject it. P 0 itself is not rejected so that it can be used to pattern-match against Integers at the type-level if necessary.

pattern SP :: 0 < x => (KnownInteger (P x), KnownNat x) => Sing (x :: Natural) -> SInteger (P x)

SP (sing @1) == sing @(P 1)

type family FromNatural (x :: Natural) :: Integer where ...

Construct a type-level Integer from a type-level Natural.

Equations

FromNatural 0 = Z

FromNatural x = P x

sFromNatural :: Sing (x :: Natural) -> SInteger (FromNatural x)

Singleton version of FromNatural.

type family Fold (z :: k) (n :: Natural ~> k) (p :: Natural ~> k) (i :: Integer) :: k where ...

Fold z n p i evaluates to z if i is zero, otherwise applies n to the absolute value of i if negative, or p to the absolute value of i if positive. N 0 and P 0 fail to type-check.

Equations

Fold _ _ _ (N 0) = TypeError ('Text "Use \8216Z\8217 instead of \8216N 0\8217.")

Fold _ _ _ (P 0) = TypeError ('Text "Use \8216Z\8217 instead of \8216P 0\8217.")

Fold z _ _ Z = z

Fold _ n _ (N x) = n @@ x

Fold _ _ p (P x) = p @@ x

sFold :: SingKind k => Sing (z :: k) -> Sing (n :: Natural ~> k) -> Sing (p :: Natural ~> k) -> SInteger i -> Sing (Fold z n p i)

Singleton version of Fold.

SInteger

type KnownInteger (i :: Integer) = (KnownInteger_ i, Normalized i ~ i, KnownNat (Abs i))

Type-level Integers satisfying KnownInteger can be converted to SIntegers using integerSing. Every Integer other than Integer 0 and Integer 0 are KnownIntegers.

type family Normalized (i :: Integer) :: Integer where ...

Normalized i is an identity function that fails to type-check if i is not in normalized form. That is, zero is represented with Z, not with P 0 or N 0.

Equations

Normalized (N 0) = TypeError ('Text "Use \8216Z\8217 instead of \8216N 0\8217.")

Normalized (P 0) = TypeError ('Text "Use \8216Z\8217 instead of \8216P 0\8217.")

Normalized i = i

integerSing :: KnownInteger i => SInteger i

Convert an implicit KnownInteger to an explicit SInteger.

integerVal :: forall i proxy. KnownInteger i => proxy i -> Integer

Term-level Prelude.Integer representation of the type-level Integer.

withKnownInteger :: forall i rep (x :: TYPE rep). SInteger i -> (KnownInteger i => x) -> x

Convert an explicit SInteger i value into an implicit KnownInteger i constraint.

data SomeInteger

Term-level representation of an existentialized KnownInteger.

Constructors

forall i.KnownInteger i => SomeInteger (Proxy i)

Instances

Read SomeInteger

As for Prelude.Integer.

Defined in KindInteger

Methods

readsPrec :: Int -> ReadS SomeInteger

readList :: ReadS [SomeInteger]

readPrec :: ReadPrec SomeInteger

readListPrec :: ReadPrec [SomeInteger]

Show SomeInteger

As for Prelude.Integer.

Defined in KindInteger

Methods

showsPrec :: Int -> SomeInteger -> ShowS

show :: SomeInteger -> String

showList :: [SomeInteger] -> ShowS

Eq SomeInteger

Defined in KindInteger

Methods

(==) :: SomeInteger -> SomeInteger -> Bool

(/=) :: SomeInteger -> SomeInteger -> Bool

Ord SomeInteger

Defined in KindInteger

Methods

compare :: SomeInteger -> SomeInteger -> Ordering

(<) :: SomeInteger -> SomeInteger -> Bool

(<=) :: SomeInteger -> SomeInteger -> Bool

(>) :: SomeInteger -> SomeInteger -> Bool

(>=) :: SomeInteger -> SomeInteger -> Bool

max :: SomeInteger -> SomeInteger -> SomeInteger

min :: SomeInteger -> SomeInteger -> SomeInteger

someIntegerVal :: Integer -> SomeInteger

Convert a term-level Prelude.Integer into an extistentialized KnownInteger wrapped in SomeInteger.

data SInteger (i :: Integer)

Singleton type for a type-level Integer i.

Instances

TestCoercion SInteger

Defined in KindInteger

Methods

testCoercion :: forall (a :: k) (b :: k). SInteger a -> SInteger b -> Maybe (Coercion a b)

TestEquality SInteger

Defined in KindInteger

Methods

testEquality :: forall (a :: k) (b :: k). SInteger a -> SInteger b -> Maybe (a :~: b)

KnownInteger i => Read (SInteger i)

Defined in KindInteger

Methods

readsPrec :: Int -> ReadS (SInteger i)

readList :: ReadS [SInteger i]

readPrec :: ReadPrec (SInteger i)

readListPrec :: ReadPrec [SInteger i]

Show (SInteger i)

Defined in KindInteger

Methods

showsPrec :: Int -> SInteger i -> ShowS

show :: SInteger i -> String

showList :: [SInteger i] -> ShowS

Eq (SInteger i)

Defined in KindInteger

Methods

(==) :: SInteger i -> SInteger i -> Bool

(/=) :: SInteger i -> SInteger i -> Bool

Ord (SInteger i)

Defined in KindInteger

Methods

compare :: SInteger i -> SInteger i -> Ordering

(<) :: SInteger i -> SInteger i -> Bool

(<=) :: SInteger i -> SInteger i -> Bool

(>) :: SInteger i -> SInteger i -> Bool

(>=) :: SInteger i -> SInteger i -> Bool

max :: SInteger i -> SInteger i -> SInteger i

min :: SInteger i -> SInteger i -> SInteger i

pattern SInteger :: forall i. () => KnownInteger i => SInteger i

A explicitly bidirectional pattern synonym relating an SInteger to a KnownInteger constraint.

As an expression: Constructs an explicit SInteger i value from an implicit KnownInteger i constraint:

SInteger @i :: KnownInteger i => SInteger i

As a pattern: Matches on an explicit SInteger i value bringing an implicit KnownInteger i constraint into scope:

f :: SInteger i -> ..
f si@SInteger = ... both (si :: SInteger i) and (KnownInteger i) in scope ...

fromSInteger :: SInteger i -> Integer

Return the term-level Prelude.Integer number corresponding to i.

withSomeSInteger :: forall rep (x :: TYPE rep). Integer -> (forall (i :: Integer). Sing i -> x) -> x

Convert a Prelude.Integer number into an SInteger n value, where n is a fresh type-level Integer.

Proofs

sNegateRefl :: SInteger i -> i :~: Negate (Negate i)

Double negation is identity.

sZigZagRefl :: SInteger i -> i :~: ZagZig (ZigZag i)

Identity.

sZagZigRefl :: Sing (n :: Natural) -> n :~: ZigZag (ZagZig n)

Identity.

Show

Besides the following *Lit tools, PShow and SShow can be used to display as Prelude.Integer does.

type ShowLit (i :: Integer) = ShowsLit i "" :: Symbol

Displays i as it would show literally as a type.

ShowLit ( N 1) ~ "P 1"
ShowLit   Z    ~ "Z"
ShowLit ( P 1) ~ "P 1"

N 0 and P 0 fail to type-check.

showLit :: Integer -> String

Demoted version of ShowLit.

sShowLit :: SInteger i -> Sing (ShowLit i)

Singleton version of ShowLit.

fromSing @(sShowLit (SN (sing @1))) == "N 1"
fromSing @(sShowLit SZ)             == "Z"
fromSing @(sShowLit (SP (sing @1))) == "P 1"

type ShowsLit (i :: Integer) (s :: Symbol) = ShowsPrecLit 0 i s :: Symbol

Displays i as it would show literally as a type. See 'ShowLit. Behaves like Shows.

showsLit :: Integer -> ShowS

Demoted version of ShowsLit.

sShowsLit :: SInteger i -> Sing (s :: Symbol) -> Sing (ShowsLit i s)

Singleton version of ShowsLit.

type ShowsPrecLit p i s = ShowsPrecLit_ p (Normalized i) s

Displays i as it would show literally as a type. See 'ShowLit. Behaves like ShowsPrec.

showsPrecLit :: Int -> Integer -> ShowS

Demoted version of ShowsPrecLit.

sShowsPrecLit :: Sing (p :: Natural) -> SInteger i -> Sing (s :: Symbol) -> Sing (ShowsPrecLit p i s)

Singleton version of ShowsPrecLit.

readPrecLit :: ReadPrec Integer

Inverse of showsPrecLit.

Operations

Additional arithmetic operations are provided through the PNum and SNum instances. Notably Abs, sAbs, Negate, sNegate, Signum, sSignum, PNum, PNum, PNum, %+, %-, %*.

type (^) (b :: Integer) (p :: Natural) = Pow (Normalized b) p :: Integer infixr 8

Exponentiation of type-level Integers.

(%^) :: Sing (b :: Integer) -> Sing (p :: Natural) -> Sing (b ^ p :: Integer) infixr 8

Singleton version of ^.

type Odd (i :: Integer) = Mod (Abs i) 2 == 1 :: Bool

Whether a type-level Integer is odd. Zero is not considered odd.

sOdd :: SInteger i -> Sing (Odd i :: Bool)

Singleton version of Odd.

type Even (i :: Integer) = Mod (Abs i) 2 == 0 :: Bool

Whether a type-level Integer is even. Zero is considered even.

sEven :: SInteger i -> Sing (Even i :: Bool)

Singleton version of Even.

type Abs (i :: Integer) = Fold 0 IdSym0 IdSym0 i :: Natural

Absolute value of a type-level Integer, as a type-level Natural.

sAbs :: SInteger i -> Sing (Abs i :: Natural)

Singleton version of Abs.

type GCD (a :: Integer) (b :: Integer) = NatGCD (Abs a) (Abs b) :: Natural

Greatest Common Divisor of type-level Integer numbers a and b.

Returns a Natural, since the Greatest Common Divisor is always positive.

sGCD :: SInteger a -> SInteger b -> Sing (GCD a b :: Natural)

Singleton version of GCD.

type LCM (a :: Integer) (b :: Integer) = NatLCM (Abs a) (Abs b) :: Natural

Least Common Multiple of type-level Integer numbers a and b.

Returns a Natural, since the Least Common Multiple is always positive.

sLCM :: SInteger a -> SInteger b -> Sing (LCM a b :: Natural)

Singleton version of LCM.

type Log2 (a :: Integer) = Fold (TypeError ('Text "Logarithm of zero.")) (ConstSym1 (TypeError ('Text "Logarithm of negative number."))) Log2Sym0 a :: Natural

Log base 2 (floored) of type-level Integers.

• Logarithm of zero doesn't type-check.
• Logarithm of negative number doesn't type-check.

sLog2 :: SInteger i -> Sing (Log2 i :: Natural)

Singleton version of Log2.

type Div (r :: Round) (a :: Integer) (b :: Integer) = Div_ r (Normalized a) (Normalized b) :: Integer infixl 7

Divide the type-level Integer a by b, using the specified Rounding r.

• Division by zero doesn't type-check.

sDiv

Arguments

:: SRound r

-> SInteger a

Dividend.

-> SInteger b

Divisor.

-> SInteger (Div r a b)

Singleton version of Div.

div

Arguments

:: Round

-> Integer

Dividend a.

-> Integer

Divisor b.

-> Integer

Quotient q.

Demoted version of Div.

Throws DivdeByZero where Div would fail to type-check.

type Rem (r :: Round) (a :: Integer) (b :: Integer) = Rem_ r (Normalized a) (Normalized b) :: Integer infixl 7

Remainder of the division of type-level Integer a by b, using the specified Rounding r.

forall (r :: Round) (a :: Integer) (b :: Integer).
  (b /= 0) =>
    Rem r a b  ==  a - b * Div r a b

• Division by zero doesn't type-check.

sRem

Arguments

:: SRound r

-> SInteger a

Dividend.

-> SInteger b

Divisor.

-> SInteger (Rem r a b)

Singleton version of Rem.

rem

Arguments

:: Round

-> Integer

Dividend a.

-> Integer

Divisor b.

-> Integer

Remainder m.

Demoted version of Rem.

Throws DivdeByZero where Div would fail to type-check.

type DivRem (r :: Round) (a :: Integer) (b :: Integer) = '(Div r a b, Rem r a b) :: (Integer, Integer) infixl 7

Get both the quotient and the Remainder of the Division of type-level Integers a and b using the specified Rounding r.

forall (r :: Round) (a :: Integer) (b :: Integer).
  (b /= 0) =>
    DivRem r a b ==  '(Div r a b, Rem r a b)

sDivRem

Arguments

:: SRound r

-> SInteger a

Dividend.

-> SInteger b

Divisor.

-> (SInteger (Div r a b), SInteger (Rem r a b))

Singleton version of DivRem.

divRem

Arguments

:: Round

-> Integer

Dividend a.

-> Integer

Divisor b.

-> (Integer, Integer)

Quotient q and remainder m.

Demoted version of DivRem.

Throws DivdeByZero where Div would fail to type-check.

Rounding

data Round

Rounding strategy.

Constructors

RoundUp

Round up towards positive infinity.

RoundDown

Round down towards negative infinity. Also known as Prelude's floor. This is the type of rounding used by Prelude's div, mod, divMod, Div, Mod.

RoundZero

Round towards zero. Also known as Prelude's truncate. This is the type of rounding used by Prelude's quot, rem, quotRem.

RoundAway

Round away from zero.

RoundHalfUp

Round towards the closest integer. If halfway between two integers, round up towards positive infinity.

RoundHalfDown

Round towards the closest integer. If halfway between two integers, round down towards negative infinity.

RoundHalfZero

Round towards the closest integer. If halfway between two integers, round towards zero.

RoundHalfAway

Round towards the closest integer. If halfway between two integers, round away from zero.

RoundHalfEven

Round towards the closest integer. If halfway between two integers, round towards the closest even integer. Also known as Prelude's round.

RoundHalfOdd

Round towards the closest integer. If halfway between two integers, round towards the closest odd integer.

Instances

Bounded Round

Defined in KindInteger.Round

Methods

minBound :: Round

maxBound :: Round

Enum Round

Defined in KindInteger.Round

Methods

succ :: Round -> Round

pred :: Round -> Round

toEnum :: Int -> Round

fromEnum :: Round -> Int

enumFrom :: Round -> [Round]

enumFromThen :: Round -> Round -> [Round]

enumFromTo :: Round -> Round -> [Round]

enumFromThenTo :: Round -> Round -> Round -> [Round]

Read Round

Defined in KindInteger.Round

Methods

readsPrec :: Int -> ReadS Round

readList :: ReadS [Round]

readPrec :: ReadPrec Round

readListPrec :: ReadPrec [Round]

Show Round

Defined in KindInteger.Round

Methods

showsPrec :: Int -> Round -> ShowS

show :: Round -> String

showList :: [Round] -> ShowS

Eq Round

Defined in KindInteger.Round

Methods

(==) :: Round -> Round -> Bool

(/=) :: Round -> Round -> Bool

Ord Round

Defined in KindInteger.Round

Methods

compare :: Round -> Round -> Ordering

(<) :: Round -> Round -> Bool

(<=) :: Round -> Round -> Bool

(>) :: Round -> Round -> Bool

(>=) :: Round -> Round -> Bool

max :: Round -> Round -> Round

min :: Round -> Round -> Round

SingKind Round

Defined in KindInteger.Round

Associated Types

type Demote Round = (r :: Type)

Methods

fromSing :: forall (a :: Round). Sing a -> Demote Round

toSing :: Demote Round -> SomeSing Round

SDecide Round

Defined in KindInteger.Round

Methods

(%~) :: forall (a :: Round) (b :: Round). Sing a -> Sing b -> Decision (a :~: b)

PEq Round

Defined in KindInteger.Round

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

SEq Round

Defined in KindInteger.Round

Methods

(%==) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) t1) t2)

POrd Round

Defined in KindInteger.Round

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

SOrd Round

Defined in KindInteger.Round

Methods

sCompare :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

PBounded Round

Defined in KindInteger.Round

Associated Types

type MinBound :: a

type MaxBound :: a

PEnum Round

Defined in KindInteger.Round

Associated Types

type Succ arg :: a

type Pred arg :: a

type ToEnum arg :: a

type FromEnum arg :: Natural

type EnumFromTo arg arg1 :: [a]

type EnumFromThenTo arg arg1 arg2 :: [a]

SBounded Round

Defined in KindInteger.Round

Methods

sMinBound :: Sing MinBoundSym0

sMaxBound :: Sing MaxBoundSym0

SEnum Round

Defined in KindInteger.Round

Methods

sSucc :: forall (t :: Round). Sing t -> Sing (Apply SuccSym0 t)

sPred :: forall (t :: Round). Sing t -> Sing (Apply PredSym0 t)

sToEnum :: forall (t :: Natural). Sing t -> Sing (Apply ToEnumSym0 t)

sFromEnum :: forall (t :: Round). Sing t -> Sing (Apply FromEnumSym0 t)

sEnumFromTo :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2)

sEnumFromThenTo :: forall (t1 :: Round) (t2 :: Round) (t3 :: Round). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3)

PShow Round

Defined in KindInteger.Round

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg1 :: Symbol

SShow Round

Defined in KindInteger.Round

Methods

sShowsPrec :: forall (t1 :: Natural) (t2 :: Round) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: forall (t :: Round). Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: forall (t1 :: [Round]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

TestCoercion SRound

Defined in KindInteger.Round

Methods

testCoercion :: forall (a :: k) (b :: k). SRound a -> SRound b -> Maybe (Coercion a b)

TestEquality SRound

Defined in KindInteger.Round

Methods

testEquality :: forall (a :: k) (b :: k). SRound a -> SRound b -> Maybe (a :~: b)

SingI 'RoundAway

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundAway

SingI 'RoundDown

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundDown

SingI 'RoundHalfAway

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundHalfAway

SingI 'RoundHalfDown

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundHalfDown

SingI 'RoundHalfEven

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundHalfEven

SingI 'RoundHalfOdd

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundHalfOdd

SingI 'RoundHalfUp

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundHalfUp

SingI 'RoundHalfZero

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundHalfZero

SingI 'RoundUp

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundUp

SingI 'RoundZero

Defined in KindInteger.Round

Methods

sing :: Sing 'RoundZero

type Demote Round

Defined in KindInteger.Round

type Demote Round = Round

type Sing

Defined in KindInteger.Round

type Sing = SRound

type MaxBound

Defined in KindInteger.Round

type MaxBound

type MinBound

Defined in KindInteger.Round

type MinBound

type FromEnum (a :: Round)

Defined in KindInteger.Round

type FromEnum (a :: Round)

type Pred (arg :: Round)

Defined in KindInteger.Round

type Pred (arg :: Round) = Apply (Pred_6989586621679523156Sym0 :: TyFun Round Round -> Type) arg

type Succ (arg :: Round)

Defined in KindInteger.Round

type Succ (arg :: Round) = Apply (Succ_6989586621679523121Sym0 :: TyFun Round Round -> Type) arg

type ToEnum a

Defined in KindInteger.Round

type ToEnum a

type Show_ (arg :: Round)

Defined in KindInteger.Round

type Show_ (arg :: Round) = Apply (Show__6989586621680028698Sym0 :: TyFun Round Symbol -> Type) arg

type (arg :: Round) /= (arg1 :: Round)

Defined in KindInteger.Round

type (arg :: Round) /= (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679140582Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1

type (a1 :: Round) == (a2 :: Round)

Defined in KindInteger.Round

type (a1 :: Round) == (a2 :: Round)

type (arg :: Round) < (arg1 :: Round)

Defined in KindInteger.Round

type (arg :: Round) < (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679338501Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1

type (arg :: Round) <= (arg1 :: Round)

Defined in KindInteger.Round

type (arg :: Round) <= (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679338543Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1

type (arg :: Round) > (arg1 :: Round)

Defined in KindInteger.Round

type (arg :: Round) > (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679338562Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1

type (arg :: Round) >= (arg1 :: Round)

Defined in KindInteger.Round

type (arg :: Round) >= (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679338578Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1

type Compare (a1 :: Round) (a2 :: Round)

Defined in KindInteger.Round

type Compare (a1 :: Round) (a2 :: Round)

type Max (arg :: Round) (arg1 :: Round)

Defined in KindInteger.Round

type Max (arg :: Round) (arg1 :: Round) = Apply (Apply (Max_6989586621679338594Sym0 :: TyFun Round (Round ~> Round) -> Type) arg) arg1

type Min (arg :: Round) (arg1 :: Round)

Defined in KindInteger.Round

type Min (arg :: Round) (arg1 :: Round) = Apply (Apply (Min_6989586621679338610Sym0 :: TyFun Round (Round ~> Round) -> Type) arg) arg1

type EnumFromTo (arg :: Round) (arg1 :: Round)

Defined in KindInteger.Round

type EnumFromTo (arg :: Round) (arg1 :: Round) = Apply (Apply (EnumFromTo_6989586621679523181Sym0 :: TyFun Round (Round ~> [Round]) -> Type) arg) arg1

type ShowList (arg :: [Round]) arg1

Defined in KindInteger.Round

type ShowList (arg :: [Round]) arg1 = Apply (Apply (ShowList_6989586621680028706Sym0 :: TyFun [Round] (Symbol ~> Symbol) -> Type) arg) arg1

type EnumFromThenTo (arg :: Round) (arg1 :: Round) (arg2 :: Round)

Defined in KindInteger.Round

type EnumFromThenTo (arg :: Round) (arg1 :: Round) (arg2 :: Round) = Apply (Apply (Apply (EnumFromThenTo_6989586621679523214Sym0 :: TyFun Round (Round ~> (Round ~> [Round])) -> Type) arg) arg1) arg2

type ShowsPrec a1 (a2 :: Round) a3

Defined in KindInteger.Round

type ShowsPrec a1 (a2 :: Round) a3

type Apply DivSym0 (r :: Round)

Defined in KindInteger

type Apply DivSym0 (r :: Round) = DivSym1 r

type Apply RemSym0 (r :: Round)

Defined in KindInteger

type Apply RemSym0 (r :: Round) = RemSym1 r

type Apply DivRemSym0 (r :: Round)

Defined in KindInteger

type Apply DivRemSym0 (r :: Round) = DivRemSym1 r

data SRound :: Round -> Type where

Constructors

SRoundUp :: SRound ('RoundUp :: Round)

SRoundDown :: SRound ('RoundDown :: Round)

SRoundZero :: SRound ('RoundZero :: Round)

SRoundAway :: SRound ('RoundAway :: Round)

SRoundHalfUp :: SRound ('RoundHalfUp :: Round)

SRoundHalfDown :: SRound ('RoundHalfDown :: Round)

SRoundHalfZero :: SRound ('RoundHalfZero :: Round)

SRoundHalfAway :: SRound ('RoundHalfAway :: Round)

SRoundHalfEven :: SRound ('RoundHalfEven :: Round)

SRoundHalfOdd :: SRound ('RoundHalfOdd :: Round)

Instances

TestCoercion SRound

Defined in KindInteger.Round

Methods

testCoercion :: forall (a :: k) (b :: k). SRound a -> SRound b -> Maybe (Coercion a b)

TestEquality SRound

Defined in KindInteger.Round

Methods

testEquality :: forall (a :: k) (b :: k). SRound a -> SRound b -> Maybe (a :~: b)

Show (SRound z)

Defined in KindInteger.Round

Methods

showsPrec :: Int -> SRound z -> ShowS

show :: SRound z -> String

showList :: [SRound z] -> ShowS

Comparisons

Additional comparison tools are available at SDdecide, TestEquality, TestCoercion, PEq, SEq, POrd, SOrd and Compare.

cmpInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> OrderingI a b

Like sameInteger, but if the type-level Integers aren't equal, this additionally provides proof of LT or GT.

sameInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

We either get evidence that this function was instantiated with the same type-level Integers, or Nothing.

Misc

type ZigZag (i :: Integer) = ZigZag_ (Normalized i) :: Natural

ZigZag encoding of an Integer.

• 0 is 0
• -x is abs(x) * 2 - 1
• +x is x * 2

sZigZag :: SInteger i -> Sing (ZigZag i :: Natural)

Singleton version of ZigZag.

type ZagZig n = If (Mod n 2 == 1) (Negate (FromNatural (Div (n + 1) 2))) (FromNatural (Div n 2))

Inverse of ZigZag.

sZagZig :: Sing (n :: Natural) -> SInteger (ZagZig n)

Singleton version of ZagZig.

Defunctionalization

type ZSym0 = Z

data NSym0 :: Natural ~> Integer

Instances

type Apply NSym0 (x :: Natural)

Defined in KindInteger

type Apply NSym0 (x :: Natural) = NSym1 x

type NSym1 x = N x

data PSym0 :: Natural ~> Integer

Instances

type Apply PSym0 (x :: Natural)

Defined in KindInteger

type Apply PSym0 (x :: Natural) = PSym1 x

type PSym1 x = P x

data FromNaturalSym0 :: Natural ~> Integer

Instances

type Apply FromNaturalSym0 (i :: Natural)

Defined in KindInteger

type Apply FromNaturalSym0 (i :: Natural) = FromNatural i

type FromNaturalSym1 i = FromNatural i

data KnownIntegerSym0 :: Integer ~> Constraint

Instances

type Apply KnownIntegerSym0 (i :: Integer)

Defined in KindInteger

type Apply KnownIntegerSym0 (i :: Integer) = KnownIntegerSym1 i

type KnownIntegerSym1 i = KnownInteger i

data NormalizedSym0 :: Integer ~> Integer

Instances

type Apply NormalizedSym0 (i :: Integer)

Defined in KindInteger

type Apply NormalizedSym0 (i :: Integer) = Normalized i

type NormalizedSym1 i = Normalized i

data FoldSym0 :: k ~> ((Natural ~> k) ~> ((Natural ~> k) ~> (Integer ~> k)))

Instances

type Apply (FoldSym0 :: TyFun k ((Natural ~> k) ~> ((Natural ~> k) ~> (Integer ~> k))) -> Type) (z :: k)

Defined in KindInteger

type Apply (FoldSym0 :: TyFun k ((Natural ~> k) ~> ((Natural ~> k) ~> (Integer ~> k))) -> Type) (z :: k) = FoldSym1 z

data FoldSym1 :: k -> (Natural ~> k) ~> ((Natural ~> k) ~> (Integer ~> k))

Instances

type Apply (FoldSym1 z :: TyFun (Natural ~> k) ((Natural ~> k) ~> (Integer ~> k)) -> Type) (n :: Natural ~> k)

Defined in KindInteger

type Apply (FoldSym1 z :: TyFun (Natural ~> k) ((Natural ~> k) ~> (Integer ~> k)) -> Type) (n :: Natural ~> k) = FoldSym2 z n

data FoldSym2 :: k -> (Natural ~> k) -> (Natural ~> k) ~> (Integer ~> k)

Instances

type Apply (FoldSym2 z n :: TyFun (Natural ~> k) (Integer ~> k) -> Type) (p :: Natural ~> k)

Defined in KindInteger

type Apply (FoldSym2 z n :: TyFun (Natural ~> k) (Integer ~> k) -> Type) (p :: Natural ~> k) = FoldSym3 z n p

data FoldSym3 :: k -> (Natural ~> k) -> (Natural ~> k) -> Integer ~> k

Instances

type Apply (FoldSym3 z n p :: TyFun Integer k -> Type) (i :: Integer)

Defined in KindInteger

type Apply (FoldSym3 z n p :: TyFun Integer k -> Type) (i :: Integer) = FoldSym4 z n p i

type FoldSym4 z n p i = Fold z n p i

data (^@#@$) :: Integer ~> (Natural ~> Integer)

Instances

type Apply (^@#@$) (b :: Integer)

Defined in KindInteger

type Apply (^@#@$) (b :: Integer) = (^@#@$$) b

data (^@#@$$) :: Integer -> Natural ~> Integer

Instances

type Apply ((^@#@$$) b :: TyFun Natural Integer -> Type) (p :: Natural)

Defined in KindInteger

type Apply ((^@#@$$) b :: TyFun Natural Integer -> Type) (p :: Natural) = b ^@#@$$$ p

type (^@#@$$$) b p = b ^ p infixr 8

data OddSym0 :: Integer ~> Bool

Instances

type Apply OddSym0 (i :: Integer)

Defined in KindInteger

type Apply OddSym0 (i :: Integer) = Odd i

type OddSym1 i = Odd i

data EvenSym0 :: Integer ~> Bool

Instances

type Apply EvenSym0 (i :: Integer)

Defined in KindInteger

type Apply EvenSym0 (i :: Integer) = Even i

type EvenSym1 i = Even i

data GCDSym0 :: Integer ~> (Integer ~> Natural)

Instances

type Apply GCDSym0 (a :: Integer)

Defined in KindInteger

type Apply GCDSym0 (a :: Integer) = GCDSym1 a

data GCDSym1 :: Integer -> Integer ~> Natural

Instances

type Apply (GCDSym1 a :: TyFun Integer Natural -> Type) (b :: Integer)

Defined in KindInteger

type Apply (GCDSym1 a :: TyFun Integer Natural -> Type) (b :: Integer)

data LCMSym0 :: Integer ~> (Integer ~> Natural)

Instances

type Apply LCMSym0 (a :: Integer)

Defined in KindInteger

type Apply LCMSym0 (a :: Integer) = LCMSym1 a

data LCMSym1 :: Integer -> Integer ~> Natural

Instances

type Apply (LCMSym1 a :: TyFun Integer Natural -> Type) (b :: Integer)

Defined in KindInteger

type Apply (LCMSym1 a :: TyFun Integer Natural -> Type) (b :: Integer)

data Log2Sym0 :: Integer ~> Natural

Instances

type Apply Log2Sym0 (a :: Integer)

Defined in KindInteger

type Apply Log2Sym0 (a :: Integer) = Log2Sym1 a

type Log2Sym1 a = Log2 a

data DivSym0 :: Round ~> (Integer ~> (Integer ~> Integer))

Instances

type Apply DivSym0 (r :: Round)

Defined in KindInteger

type Apply DivSym0 (r :: Round) = DivSym1 r

data DivSym1 :: Round -> Integer ~> (Integer ~> Integer)

Instances

type Apply (DivSym1 r :: TyFun Integer (Integer ~> Integer) -> Type) (a :: Integer)

Defined in KindInteger

type Apply (DivSym1 r :: TyFun Integer (Integer ~> Integer) -> Type) (a :: Integer) = DivSym2 r a

data DivSym2 :: Round -> Integer -> Integer ~> Integer

Instances

type Apply (DivSym2 r a :: TyFun Integer Integer -> Type) (b :: Integer)

Defined in KindInteger

type Apply (DivSym2 r a :: TyFun Integer Integer -> Type) (b :: Integer) = DivSym3 r a b

type DivSym3 r a b = Div r a b

data RemSym0 :: Round ~> (Integer ~> (Integer ~> Integer))

Instances

type Apply RemSym0 (r :: Round)

Defined in KindInteger

type Apply RemSym0 (r :: Round) = RemSym1 r

data RemSym1 :: Round -> Integer ~> (Integer ~> Integer)

Instances

type Apply (RemSym1 r :: TyFun Integer (Integer ~> Integer) -> Type) (a :: Integer)

Defined in KindInteger

type Apply (RemSym1 r :: TyFun Integer (Integer ~> Integer) -> Type) (a :: Integer) = RemSym2 r a

data RemSym2 :: Round -> Integer -> Integer ~> Integer

Instances

type Apply (RemSym2 r a :: TyFun Integer Integer -> Type) (b :: Integer)

Defined in KindInteger

type Apply (RemSym2 r a :: TyFun Integer Integer -> Type) (b :: Integer) = RemSym3 r a b

type RemSym3 r a b = Rem r a b

data DivRemSym0 :: Round ~> (Integer ~> (Integer ~> (Integer, Integer)))

Instances

type Apply DivRemSym0 (r :: Round)

Defined in KindInteger

type Apply DivRemSym0 (r :: Round) = DivRemSym1 r

data DivRemSym1 :: Round -> Integer ~> (Integer ~> (Integer, Integer))

Instances

type Apply (DivRemSym1 r :: TyFun Integer (Integer ~> (Integer, Integer)) -> Type) (a :: Integer)

Defined in KindInteger

type Apply (DivRemSym1 r :: TyFun Integer (Integer ~> (Integer, Integer)) -> Type) (a :: Integer) = DivRemSym2 r a

data DivRemSym2 :: Round -> Integer -> Integer ~> (Integer, Integer)

Instances

type Apply (DivRemSym2 r a :: TyFun Integer (Integer, Integer) -> Type) (b :: Integer)

Defined in KindInteger

type Apply (DivRemSym2 r a :: TyFun Integer (Integer, Integer) -> Type) (b :: Integer) = DivRemSym3 r a b

type DivRemSym3 r a b = DivRem r a b

data ShowLitSym0 :: Integer ~> Symbol

Instances

type Apply ShowLitSym0 (i :: Integer)

Defined in KindInteger

type Apply ShowLitSym0 (i :: Integer) = ShowLitSym1 i

type ShowLitSym1 i = ShowLit i

data ShowsLitSym0 :: Integer ~> (Symbol ~> Symbol)

Instances

type Apply ShowsLitSym0 (i :: Integer)

Defined in KindInteger

type Apply ShowsLitSym0 (i :: Integer) = ShowsLitSym1 i

data ShowsLitSym1 :: Integer -> Symbol ~> Symbol

Instances

type Apply (ShowsLitSym1 i :: TyFun Symbol Symbol -> Type) (s :: Symbol)

Defined in KindInteger

type Apply (ShowsLitSym1 i :: TyFun Symbol Symbol -> Type) (s :: Symbol) = ShowsLitSym2 i s

type ShowsLitSym2 i s = ShowsLit i s

data ShowsPrecLitSym0 :: Natural ~> (Integer ~> (Symbol ~> Symbol))

Instances

type Apply ShowsPrecLitSym0 (p :: Natural)

Defined in KindInteger

type Apply ShowsPrecLitSym0 (p :: Natural) = ShowsPrecLitSym1 p

data ShowsPrecLitSym1 :: Natural -> Integer ~> (Symbol ~> Symbol)

Instances

type Apply (ShowsPrecLitSym1 p :: TyFun Integer (Symbol ~> Symbol) -> Type) (i :: Integer)

Defined in KindInteger

type Apply (ShowsPrecLitSym1 p :: TyFun Integer (Symbol ~> Symbol) -> Type) (i :: Integer) = ShowsPrecLitSym2 p i

data ShowsPrecLitSym2 :: Natural -> Integer -> Symbol ~> Symbol

Instances

type Apply (ShowsPrecLitSym2 p i :: TyFun Symbol Symbol -> Type) (s :: Symbol)

Defined in KindInteger

type Apply (ShowsPrecLitSym2 p i :: TyFun Symbol Symbol -> Type) (s :: Symbol) = ShowsPrecLitSym3 p i s

type ShowsPrecLitSym3 p i s = ShowsPrecLit p i s

type family RoundUpSym0 :: Round where ...

Equations

RoundUpSym0 = 'RoundUp

type family RoundDownSym0 :: Round where ...

Equations

RoundDownSym0 = 'RoundDown

type family RoundZeroSym0 :: Round where ...

Equations

RoundZeroSym0 = 'RoundZero

type family RoundAwaySym0 :: Round where ...

Equations

RoundAwaySym0 = 'RoundAway

type family RoundHalfUpSym0 :: Round where ...

Equations

RoundHalfUpSym0 = 'RoundHalfUp

type family RoundHalfDownSym0 :: Round where ...

Equations

RoundHalfDownSym0 = 'RoundHalfDown

type family RoundHalfZeroSym0 :: Round where ...

Equations

RoundHalfZeroSym0 = 'RoundHalfZero

type family RoundHalfAwaySym0 :: Round where ...

Equations

RoundHalfAwaySym0 = 'RoundHalfAway

type family RoundHalfEvenSym0 :: Round where ...

Equations

RoundHalfEvenSym0 = 'RoundHalfEven

type family RoundHalfOddSym0 :: Round where ...

Equations

RoundHalfOddSym0 = 'RoundHalfOdd