Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
This module provides a type-level representation for term-level
Integer
s. 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 Natural
s
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.
Synopsis
- data Integer
- type Z = 'Z :: Integer
- pattern SZ :: SInteger Z
- type N (x :: Natural) = 'N x :: Integer
- pattern SN :: 0 < x => (KnownInteger (N x), KnownNat x) => Sing (x :: Natural) -> SInteger (N x)
- type P (x :: Natural) = 'P x :: Integer
- pattern SP :: 0 < x => (KnownInteger (P x), KnownNat x) => Sing (x :: Natural) -> SInteger (P x)
- type family FromNatural (x :: Natural) :: Integer where ...
- sFromNatural :: Sing (x :: Natural) -> SInteger (FromNatural x)
- type family Fold (z :: k) (n :: Natural ~> k) (p :: Natural ~> k) (i :: Integer) :: k where ...
- sFold :: SingKind k => Sing (z :: k) -> Sing (n :: Natural ~> k) -> Sing (p :: Natural ~> k) -> SInteger i -> Sing (Fold z n p i)
- type KnownInteger (i :: Integer) = (KnownInteger_ i, Normalized i ~ i, KnownNat (Abs i))
- type family Normalized (i :: Integer) :: Integer where ...
- integerSing :: KnownInteger i => SInteger i
- integerVal :: forall i proxy. KnownInteger i => proxy i -> Integer
- withKnownInteger :: forall i rep (x :: TYPE rep). SInteger i -> (KnownInteger i => x) -> x
- data SomeInteger = forall i.KnownInteger i => SomeInteger (Proxy i)
- someIntegerVal :: Integer -> SomeInteger
- data SInteger (i :: Integer)
- pattern SInteger :: forall i. () => KnownInteger i => SInteger i
- fromSInteger :: SInteger i -> Integer
- withSomeSInteger :: forall rep (x :: TYPE rep). Integer -> (forall (i :: Integer). Sing i -> x) -> x
- sNegateRefl :: SInteger i -> i :~: Negate (Negate i)
- sZigZagRefl :: SInteger i -> i :~: ZagZig (ZigZag i)
- sZagZigRefl :: Sing (n :: Natural) -> n :~: ZigZag (ZagZig n)
- type ShowLit (i :: Integer) = ShowsLit i "" :: Symbol
- showLit :: Integer -> String
- sShowLit :: SInteger i -> Sing (ShowLit i)
- type ShowsLit (i :: Integer) (s :: Symbol) = ShowsPrecLit 0 i s :: Symbol
- showsLit :: Integer -> ShowS
- sShowsLit :: SInteger i -> Sing (s :: Symbol) -> Sing (ShowsLit i s)
- type ShowsPrecLit p i s = ShowsPrecLit_ p (Normalized i) s
- showsPrecLit :: Int -> Integer -> ShowS
- sShowsPrecLit :: Sing (p :: Natural) -> SInteger i -> Sing (s :: Symbol) -> Sing (ShowsPrecLit p i s)
- readPrecLit :: ReadPrec Integer
- type (^) (b :: Integer) (p :: Natural) = Pow (Normalized b) p :: Integer
- (%^) :: Sing (b :: Integer) -> Sing (p :: Natural) -> Sing (b ^ p :: Integer)
- type Odd (i :: Integer) = Mod (Abs i) 2 == 1 :: Bool
- sOdd :: SInteger i -> Sing (Odd i :: Bool)
- type Even (i :: Integer) = Mod (Abs i) 2 == 0 :: Bool
- sEven :: SInteger i -> Sing (Even i :: Bool)
- type Abs (i :: Integer) = Fold 0 IdSym0 IdSym0 i :: Natural
- sAbs :: SInteger i -> Sing (Abs i :: Natural)
- type GCD (a :: Integer) (b :: Integer) = NatGCD (Abs a) (Abs b) :: Natural
- sGCD :: SInteger a -> SInteger b -> Sing (GCD a b :: Natural)
- type LCM (a :: Integer) (b :: Integer) = NatLCM (Abs a) (Abs b) :: Natural
- sLCM :: SInteger a -> SInteger b -> Sing (LCM a b :: Natural)
- type Log2 (a :: Integer) = Fold (TypeError ('Text "Logarithm of zero.")) (ConstSym1 (TypeError ('Text "Logarithm of negative number."))) Log2Sym0 a :: Natural
- sLog2 :: SInteger i -> Sing (Log2 i :: Natural)
- type Div (r :: Round) (a :: Integer) (b :: Integer) = Div_ r (Normalized a) (Normalized b) :: Integer
- sDiv :: SRound r -> SInteger a -> SInteger b -> SInteger (Div r a b)
- div :: Round -> Integer -> Integer -> Integer
- type Rem (r :: Round) (a :: Integer) (b :: Integer) = Rem_ r (Normalized a) (Normalized b) :: Integer
- sRem :: SRound r -> SInteger a -> SInteger b -> SInteger (Rem r a b)
- rem :: Round -> Integer -> Integer -> Integer
- type DivRem (r :: Round) (a :: Integer) (b :: Integer) = '(Div r a b, Rem r a b) :: (Integer, Integer)
- sDivRem :: SRound r -> SInteger a -> SInteger b -> (SInteger (Div r a b), SInteger (Rem r a b))
- divRem :: Round -> Integer -> Integer -> (Integer, Integer)
- data Round
- data SRound :: Round -> Type where
- 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)
- cmpInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> OrderingI a b
- sameInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
- type ZigZag (i :: Integer) = ZigZag_ (Normalized i) :: Natural
- sZigZag :: SInteger i -> Sing (ZigZag i :: Natural)
- type ZagZig n = If (Mod n 2 == 1) (Negate (FromNatural (Div (n + 1) 2))) (FromNatural (Div n 2))
- sZagZig :: Sing (n :: Natural) -> SInteger (ZagZig n)
- type ZSym0 = Z
- data NSym0 :: Natural ~> Integer
- type NSym1 x = N x
- data PSym0 :: Natural ~> Integer
- type PSym1 x = P x
- data FromNaturalSym0 :: Natural ~> Integer
- type FromNaturalSym1 i = FromNatural i
- data KnownIntegerSym0 :: Integer ~> Constraint
- type KnownIntegerSym1 i = KnownInteger i
- data NormalizedSym0 :: Integer ~> Integer
- type NormalizedSym1 i = Normalized i
- data FoldSym0 :: k ~> ((Natural ~> k) ~> ((Natural ~> k) ~> (Integer ~> k)))
- data FoldSym1 :: k -> (Natural ~> k) ~> ((Natural ~> k) ~> (Integer ~> k))
- data FoldSym2 :: k -> (Natural ~> k) -> (Natural ~> k) ~> (Integer ~> k)
- data FoldSym3 :: k -> (Natural ~> k) -> (Natural ~> k) -> Integer ~> k
- type FoldSym4 z n p i = Fold z n p i
- data (^@#@$) :: Integer ~> (Natural ~> Integer)
- data (^@#@$$) :: Integer -> Natural ~> Integer
- type (^@#@$$$) b p = b ^ p
- data OddSym0 :: Integer ~> Bool
- type OddSym1 i = Odd i
- data EvenSym0 :: Integer ~> Bool
- type EvenSym1 i = Even i
- data GCDSym0 :: Integer ~> (Integer ~> Natural)
- data GCDSym1 :: Integer -> Integer ~> Natural
- data LCMSym0 :: Integer ~> (Integer ~> Natural)
- data LCMSym1 :: Integer -> Integer ~> Natural
- data Log2Sym0 :: Integer ~> Natural
- type Log2Sym1 a = Log2 a
- data DivSym0 :: Round ~> (Integer ~> (Integer ~> Integer))
- data DivSym1 :: Round -> Integer ~> (Integer ~> Integer)
- data DivSym2 :: Round -> Integer -> Integer ~> Integer
- type DivSym3 r a b = Div r a b
- data RemSym0 :: Round ~> (Integer ~> (Integer ~> Integer))
- data RemSym1 :: Round -> Integer ~> (Integer ~> Integer)
- data RemSym2 :: Round -> Integer -> Integer ~> Integer
- type RemSym3 r a b = Rem r a b
- data DivRemSym0 :: Round ~> (Integer ~> (Integer ~> (Integer, Integer)))
- data DivRemSym1 :: Round -> Integer ~> (Integer ~> (Integer, Integer))
- data DivRemSym2 :: Round -> Integer -> Integer ~> (Integer, Integer)
- type DivRemSym3 r a b = DivRem r a b
- data ShowLitSym0 :: Integer ~> Symbol
- type ShowLitSym1 i = ShowLit i
- data ShowsLitSym0 :: Integer ~> (Symbol ~> Symbol)
- data ShowsLitSym1 :: Integer -> Symbol ~> Symbol
- type ShowsLitSym2 i s = ShowsLit i s
- data ShowsPrecLitSym0 :: Natural ~> (Integer ~> (Symbol ~> Symbol))
- data ShowsPrecLitSym1 :: Natural -> Integer ~> (Symbol ~> Symbol)
- data ShowsPrecLitSym2 :: Natural -> Integer -> Symbol ~> Symbol
- type ShowsPrecLitSym3 p i s = ShowsPrecLit p i s
- type family RoundUpSym0 :: Round where ...
- type family RoundDownSym0 :: Round where ...
- type family RoundZeroSym0 :: Round where ...
- type family RoundAwaySym0 :: Round where ...
- type family RoundHalfUpSym0 :: Round where ...
- type family RoundHalfDownSym0 :: Round where ...
- type family RoundHalfZeroSym0 :: Round where ...
- type family RoundHalfAwaySym0 :: Round where ...
- type family RoundHalfEvenSym0 :: Round where ...
- type family RoundHalfOddSym0 :: Round where ...
Integer
Type-level version of Integer
, only used as a kind.
Instances
type N (x :: Natural) = 'N x :: Integer Source #
A negative number -x is represented as
.N
x
While a standalone
type-checks, it is not considered valid,
so tools like N
0KnownInteger
or Normalized
will reject it.
itself is not rejected so that it can be used to pattern-match
against N
0Integer
s at the type-level if necessary.
pattern SN :: 0 < x => (KnownInteger (N x), KnownNat x) => Sing (x :: Natural) -> SInteger (N x) Source #
type P (x :: Natural) = 'P x :: Integer Source #
A positive number +x is represented as
.P
x
While a standalone
type-checks, it is not considered valid,
so tools like P
0KnownInteger
or Normalized
will reject it.
itself is not rejected so that it can be used to pattern-match
against P
0Integer
s at the type-level if necessary.
pattern SP :: 0 < x => (KnownInteger (P x), KnownNat x) => Sing (x :: Natural) -> SInteger (P x) Source #
type family FromNatural (x :: Natural) :: Integer where ... Source #
FromNatural 0 = Z | |
FromNatural x = P x |
sFromNatural :: Sing (x :: Natural) -> SInteger (FromNatural x) Source #
Singleton version of FromNatural
.
type family Fold (z :: k) (n :: Natural ~> k) (p :: Natural ~> k) (i :: Integer) :: k where ... Source #
sFold :: SingKind k => Sing (z :: k) -> Sing (n :: Natural ~> k) -> Sing (p :: Natural ~> k) -> SInteger i -> Sing (Fold z n p i) Source #
Singleton version of Fold
.
SInteger
type KnownInteger (i :: Integer) = (KnownInteger_ i, Normalized i ~ i, KnownNat (Abs i)) Source #
Type-level Integer
s satisfying KnownInteger
can be converted to
SInteger
s using integerSing
. Every Integer
other than
and
Integer
0
are Integer
0KnownInteger
s.
type family Normalized (i :: Integer) :: Integer where ... Source #
is an identity function that fails to type-check
if Normalized
ii
is not in normalized form. That is, zero is represented with Z
,
not with
or P
0
.N
0
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 Source #
Convert an implicit KnownInteger
to an explicit SInteger
.
integerVal :: forall i proxy. KnownInteger i => proxy i -> Integer Source #
withKnownInteger :: forall i rep (x :: TYPE rep). SInteger i -> (KnownInteger i => x) -> x Source #
Convert an explicit
value into an implicit
SInteger
i
constraint.KnownInteger
i
data SomeInteger Source #
Term-level representation of an existentialized KnownInteger
.
forall i.KnownInteger i => SomeInteger (Proxy i) |
Instances
Read SomeInteger Source # | |
Defined in KindInteger readsPrec :: Int -> ReadS SomeInteger # readList :: ReadS [SomeInteger] # readPrec :: ReadPrec SomeInteger # readListPrec :: ReadPrec [SomeInteger] # | |
Show SomeInteger Source # | |
Defined in KindInteger showsPrec :: Int -> SomeInteger -> ShowS # show :: SomeInteger -> String # showList :: [SomeInteger] -> ShowS # | |
Eq SomeInteger Source # | |
Defined in KindInteger (==) :: SomeInteger -> SomeInteger -> Bool # (/=) :: SomeInteger -> SomeInteger -> Bool # | |
Ord SomeInteger Source # | |
Defined in KindInteger 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 Source #
Convert a term-level Prelude.Integer
into an
extistentialized KnownInteger
wrapped in SomeInteger
.
data SInteger (i :: Integer) Source #
Singleton type for a type-level Integer
i
.
Instances
TestCoercion SInteger Source # | |
Defined in KindInteger | |
TestEquality SInteger Source # | |
Defined in KindInteger | |
KnownInteger i => Read (SInteger i) Source # | |
Show (SInteger i) Source # | |
Eq (SInteger i) Source # | |
Ord (SInteger i) Source # | |
pattern SInteger :: forall i. () => KnownInteger i => SInteger i Source #
A explicitly bidirectional pattern synonym relating an SInteger
to a
KnownInteger
constraint.
As an expression: Constructs an explicit
value from an
implicit SInteger
i
constraint:KnownInteger
i
SInteger
@i ::KnownInteger
i =>SInteger
i
As a pattern: Matches on an explicit
value bringing
an implicit SInteger
i
constraint into scope:KnownInteger
i
f ::SInteger
i -> .. f si@SInteger
= ... both (si ::SInteger
i) and (KnownInteger
i) in scope ...
fromSInteger :: SInteger i -> Integer Source #
withSomeSInteger :: forall rep (x :: TYPE rep). Integer -> (forall (i :: Integer). Sing i -> x) -> x Source #
Proofs
Show
type ShowsLit (i :: Integer) (s :: Symbol) = ShowsPrecLit 0 i s :: Symbol Source #
Displays i
as it would show literally as a type. See 'ShowLit.
Behaves like Shows
.
sShowsLit :: SInteger i -> Sing (s :: Symbol) -> Sing (ShowsLit i s) Source #
Singleton version of ShowsLit
.
type ShowsPrecLit p i s = ShowsPrecLit_ p (Normalized i) s Source #
Displays i
as it would show literally as a type. See 'ShowLit.
Behaves like ShowsPrec
.
showsPrecLit :: Int -> Integer -> ShowS Source #
Demoted version of ShowsPrecLit
.
sShowsPrecLit :: Sing (p :: Natural) -> SInteger i -> Sing (s :: Symbol) -> Sing (ShowsPrecLit p i s) Source #
Singleton version of ShowsPrecLit
.
readPrecLit :: ReadPrec Integer Source #
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 Source #
Exponentiation of type-level Integer
s.
(%^) :: Sing (b :: Integer) -> Sing (p :: Natural) -> Sing (b ^ p :: Integer) infixr 8 Source #
Singleton version of ^
.
type Odd (i :: Integer) = Mod (Abs i) 2 == 1 :: Bool Source #
Whether a type-level Integer
is odd. Zero is not considered odd.
type Even (i :: Integer) = Mod (Abs i) 2 == 0 :: Bool Source #
Whether a type-level Integer
is even. Zero is considered even.
type Log2 (a :: Integer) = Fold (TypeError ('Text "Logarithm of zero.")) (ConstSym1 (TypeError ('Text "Logarithm of negative number."))) Log2Sym0 a :: Natural Source #
type Div (r :: Round) (a :: Integer) (b :: Integer) = Div_ r (Normalized a) (Normalized b) :: Integer infixl 7 Source #
Singleton version of Div
.
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 Source #
Singleton version of Rem
.
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 Source #
:: SRound r | |
-> SInteger a | Dividend. |
-> SInteger b | Divisor. |
-> (SInteger (Div r a b), SInteger (Rem r a b)) |
Singleton version of DivRem
.
Demoted version of DivRem
.
Throws DivdeByZero
where Div
would fail to type-check.
Rounding
Rounding strategy.
RoundUp | Round up towards positive infinity. |
RoundDown | Round down towards negative infinity. Also known as Prelude's
|
RoundZero | Round towards zero. Also known as Prelude's |
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
|
RoundHalfOdd | Round towards the closest integer. If halfway between two integers, round towards the closest odd integer. |
Instances
data SRound :: Round -> Type where Source #
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 Source # | |
Defined in KindInteger.Round | |
TestEquality SRound Source # | |
Defined in KindInteger.Round | |
Show (SRound z) Source # | |
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 Source #
Like sameInteger
, but if the type-level Integer
s 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) Source #
Misc
type ZigZag (i :: Integer) = ZigZag_ (Normalized i) :: Natural Source #
ZigZag encoding of an Integer
.
- 0 is 0
- -x is abs(x) * 2 - 1
- +x is x * 2
type ZagZig n = If (Mod n 2 == 1) (Negate (FromNatural (Div (n + 1) 2))) (FromNatural (Div n 2)) Source #
Inverse of ZigZag
.
Defunctionalization
data FromNaturalSym0 :: Natural ~> Integer Source #
Instances
type Apply FromNaturalSym0 (i :: Natural) Source # | |
Defined in KindInteger |
type FromNaturalSym1 i = FromNatural i Source #
data KnownIntegerSym0 :: Integer ~> Constraint Source #
Instances
type Apply KnownIntegerSym0 (i :: Integer) Source # | |
Defined in KindInteger |
type KnownIntegerSym1 i = KnownInteger i Source #
data NormalizedSym0 :: Integer ~> Integer Source #
Instances
type Apply NormalizedSym0 (i :: Integer) Source # | |
Defined in KindInteger |
type NormalizedSym1 i = Normalized i Source #
data DivRemSym0 :: Round ~> (Integer ~> (Integer ~> (Integer, Integer))) Source #
Instances
type Apply DivRemSym0 (r :: Round) Source # | |
Defined in KindInteger |
data DivRemSym2 :: Round -> Integer -> Integer ~> (Integer, Integer) Source #
Instances
type Apply (DivRemSym2 r a :: TyFun Integer (Integer, Integer) -> Type) (b :: Integer) Source # | |
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 Source #
data ShowLitSym0 :: Integer ~> Symbol Source #
Instances
type Apply ShowLitSym0 (i :: Integer) Source # | |
Defined in KindInteger |
type ShowLitSym1 i = ShowLit i Source #
data ShowsLitSym0 :: Integer ~> (Symbol ~> Symbol) Source #
Instances
type Apply ShowsLitSym0 (i :: Integer) Source # | |
Defined in KindInteger |
data ShowsLitSym1 :: Integer -> Symbol ~> Symbol Source #
Instances
type Apply (ShowsLitSym1 i :: TyFun Symbol Symbol -> Type) (s :: Symbol) Source # | |
Defined in KindInteger |
type ShowsLitSym2 i s = ShowsLit i s Source #
data ShowsPrecLitSym0 :: Natural ~> (Integer ~> (Symbol ~> Symbol)) Source #
Instances
type Apply ShowsPrecLitSym0 (p :: Natural) Source # | |
Defined in KindInteger |
data ShowsPrecLitSym2 :: Natural -> Integer -> Symbol ~> Symbol Source #
Instances
type Apply (ShowsPrecLitSym2 p i :: TyFun Symbol Symbol -> Type) (s :: Symbol) Source # | |
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 Source #
type family RoundUpSym0 :: Round where ... Source #
type family RoundDownSym0 :: Round where ... Source #
type family RoundZeroSym0 :: Round where ... Source #
type family RoundAwaySym0 :: Round where ... Source #
type family RoundHalfUpSym0 :: Round where ... Source #
type family RoundHalfDownSym0 :: Round where ... Source #
type family RoundHalfZeroSym0 :: Round where ... Source #
type family RoundHalfAwaySym0 :: Round where ... Source #
type family RoundHalfEvenSym0 :: Round where ... Source #
type family RoundHalfOddSym0 :: Round where ... Source #