type-level-0.2.4: Type-level programming librarySource codeContentsIndex
Data.TypeLevel.Num.Ops
Portabilitynon-portable (MPTC, non-standard instances)
Stabilityexperimental
Maintaineralfonso.acosta@gmail.com
Contents
Successor/Predecessor
Addition/Subtraction
Multiplication/Division
Special efficiency cases
Exponientiation/Logarithm
Special efficiency cases
Comparison assertions
General comparison assertion
Type-level values denoting comparison results
Abbreviated comparison assertions
Maximum/Minimum
Greatest Common Divisor
Description
Type-level numerical operations and its value-level reflection functions.
Synopsis
class (Nat x, Pos y) => Succ x y | x -> y, y -> x
succ :: Succ x y => x -> y
class (Pos x, Nat y) => Pred x y | x -> y, y -> x
pred :: Pred x y => x -> y
class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> x
(+) :: Add x y z => x -> y -> z
class Sub x y z | x y -> z, z x -> y, z y -> x
(-) :: Sub x y z => x -> y -> z
class (Nat x, Nat y, Nat z) => Mul x y z | x y -> z
(*) :: Mul x y z => x -> y -> z
class Div x y z | x y -> z, x z -> y, y z -> x
div :: Div x y z => x -> y -> z
class Mod x y r | x y -> r
mod :: Mod x y r => x -> y -> r
class (Nat x, Pos y) => DivMod x y q r | x y -> q r
divMod :: DivMod x y q r => x -> y -> (q, r)
class (Pos d, Nat x) => IsDivBy d x
isDivBy :: IsDivBy d x => d -> x
class (Nat x, Nat q) => Mul10 x q | x -> q, q -> x
mul10 :: Mul10 x q => x -> q
class (Nat x, Nat q) => Div10 x q | x -> q, q -> x
div10 :: Div10 x q => x -> q
class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i l
divMod10 :: DivMod10 x q r => x -> (q, r)
class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> r
(^) :: ExpBase b e r => b -> e -> r
class (Pos b, b :>=: D2, Pos x, Nat e) => LogBase b x e | b x -> e
logBase :: LogBaseF b x e f => b -> x -> e
class (Pos b, b :>=: D2, Pos x, Nat e, Bool f) => LogBaseF b x e f | b x -> e f
logBaseF :: LogBaseF b x e f => b -> x -> (e, f)
class (Pos b, b :>=: D2, Pos x) => IsPowOf b x
isPowOf :: IsPowOf b x => b -> x -> ()
class (Nat x, Pos y) => Exp10 x y | x -> y, y -> x
exp10 :: Exp10 x y => x -> y
class (Pos x, Nat y) => Log10 x y | x -> y
log10 :: Log10 x y => x -> y
class (Nat x, Nat y) => Trich x y r | x y -> r
trich :: Trich x y r => z -> x -> r
data LT
data EQ
data GT
class x :==: y
class x :>: y
class x :<: y
class x :>=: y
class x :<=: y
(==) :: x :==: y => x -> y -> ()
(>) :: x :>: y => x -> y -> ()
(<) :: x :<: y => x -> y -> ()
(>=) :: x :>=: y => x -> y -> ()
(<=) :: x :<=: y => x -> y -> ()
class Max x y z | x y -> z
max :: Max x y z => x -> y -> z
class Min x y z | x y -> z
min :: Min x y z => x -> y -> z
class (Nat x, Nat y, Nat gcd) => GCD x y gcd | x y -> gcd
gcd :: GCD x y z => x -> y -> z
Successor/Predecessor
class (Nat x, Pos y) => Succ x y | x -> y, y -> xSource
Successor type-level relation. Succ x y establishes that succ x = y.
show/hide Instances
(Pos y, IsZero y yz, DivMod10 x xi xl, Succ' xi xl yi yl yz, DivMod10 y yi yl) => Succ x y
succ :: Succ x y => x -> ySource
value-level reflection function for the Succ type-level relation
class (Pos x, Nat y) => Pred x y | x -> y, y -> xSource
Predecessor type-level relation. Pred x y establishes that pred x = y.
show/hide Instances
Succ x y => Pred y x
pred :: Pred x y => x -> ySource
value-level reflection function for the Pred type-level relation
Addition/Subtraction
class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> xSource
Addition type-level relation. Add x y z establishes that x + y = z.
show/hide Instances
(Add' x y z, Add' y x z) => Add x y z
(+) :: Add x y z => x -> y -> zSource
value-level reflection function for the Add type-level relation
class Sub x y z | x y -> z, z x -> y, z y -> xSource
Subtraction type-level relation. Sub x y z establishes that x - y = z
show/hide Instances
Add x y z => Sub z y x
(-) :: Sub x y z => x -> y -> zSource
value-level reflection function for the Sub type-level relation
Multiplication/Division
class (Nat x, Nat y, Nat z) => Mul x y z | x y -> zSource
Multiplication type-level relation. Mul x y z establishes that x * y = z. Note it isn't relational (i.e. its inverse cannot be used for division, however, even if it could, the resulting division would only work for zero-remainder divisions)
show/hide Instances
(Add z y z', Mul D8 y z) => Mul D9 y z'
(Add z y z', Mul D7 y z) => Mul D8 y z'
(Add z y z', Mul D6 y z) => Mul D7 y z'
(Add z y z', Mul D5 y z) => Mul D6 y z'
(Add z y z', Mul D4 y z) => Mul D5 y z'
(Add z y z', Mul D3 y z) => Mul D4 y z'
(Add z y z', Mul D2 y z) => Mul D3 y z'
Add y y z => Mul D2 y z
Nat y => Mul D1 y y
Nat y => Mul D0 y D0
(Pos (:* xi xl), Nat y, Mul xi y z, Mul10 z z10, Mul xl y dy, Add dy z10 z') => Mul (:* xi xl) y z'
(*) :: Mul x y z => x -> y -> zSource
value-level reflection function for the multiplication type-level relation
class Div x y z | x y -> z, x z -> y, y z -> xSource
Division type-level relation. Remainder-discarding version of DivMod. Note it is not relational (due to DivMod not being relational)
show/hide Instances
DivMod x y q r => Div x y q
div :: Div x y z => x -> y -> zSource
value-level reflection function for the Div type-level relation
class Mod x y r | x y -> rSource
Remainder of division, type-level relation. Mod x y r establishes that r is the reminder of dividing x by y.
show/hide Instances
DivMod x y q r => Mod x y r
mod :: Mod x y r => x -> y -> rSource
value-level reflection function for the Mod type-level relation
class (Nat x, Pos y) => DivMod x y q r | x y -> q rSource
Division and Remainder type-level relation. DivMod x y q r establishes that xy = q + ry Note it is not relational (i.e. its inverse cannot be used for multiplication).
show/hide Instances
(Pos y, Trich x y cmp, DivMod' x y q r cmp) => DivMod x y q r
divMod :: DivMod x y q r => x -> y -> (q, r)Source
value-level reflection function for the DivMod type-level relation
class (Pos d, Nat x) => IsDivBy d x Source
Is-divisible-by type-level assertion. e.g IsDivBy d x establishes that x is divisible by d.
show/hide Instances
DivMod x d q D0 => IsDivBy d x
isDivBy :: IsDivBy d x => d -> xSource
value-level reflection function for IsDivBy
Special efficiency cases
class (Nat x, Nat q) => Mul10 x q | x -> q, q -> xSource
Multiplication by 10 type-level relation (based on DivMod10). Mul10 x y establishes that 10 * x = y.
show/hide Instances
DivMod10 x q D0 => Mul10 q x
mul10 :: Mul10 x q => x -> qSource
value-level reflection function for Mul10
class (Nat x, Nat q) => Div10 x q | x -> q, q -> xSource
Division by 10 type-level relation (based on DivMod10)
show/hide Instances
DivMod10 x q r => Div10 x q
div10 :: Div10 x q => x -> qSource
value-level reflection function for Mul10
class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i lSource

Division by 10 and Remainer type-level relation (similar to DivMod).

This operation is much faster than DivMod. Furthermore, it is the general, non-structural, constructor/deconstructor since it splits a decimal numeral into its initial digits and last digit. Thus, it allows to inspect the structure of a number and is normally used to create type-level operations.

Note that contrary to DivMod, DivMod10 is relational (it can be used to multiply by 10)

show/hide Instances
DivMod10 D9 D0 D9
DivMod10 D8 D0 D8
DivMod10 D7 D0 D7
DivMod10 D6 D0 D6
DivMod10 D5 D0 D5
DivMod10 D4 D0 D4
DivMod10 D3 D0 D3
DivMod10 D2 D0 D2
DivMod10 D1 D0 D1
DivMod10 D0 D0 D0
Nat (:* D9 l) => DivMod10 (:* D9 l) D9 l
Nat (:* D8 l) => DivMod10 (:* D8 l) D8 l
Nat (:* D7 l) => DivMod10 (:* D7 l) D7 l
Nat (:* D6 l) => DivMod10 (:* D6 l) D6 l
Nat (:* D5 l) => DivMod10 (:* D5 l) D5 l
Nat (:* D4 l) => DivMod10 (:* D4 l) D4 l
Nat (:* D3 l) => DivMod10 (:* D3 l) D3 l
Nat (:* D2 l) => DivMod10 (:* D2 l) D2 l
Nat (:* D1 l) => DivMod10 (:* D1 l) D1 l
(Nat (:* x l), Nat (:* (:* x l) l')) => DivMod10 (:* (:* x l) l') (:* x l) l'
divMod10 :: DivMod10 x q r => x -> (q, r)Source
value-level reflection function for DivMod10
Exponientiation/Logarithm
class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> rSource
Exponentation type-level relation. ExpBase b e r establishes that b^e = r Note it is not relational (i.e. it cannot be used to express logarithms)
show/hide Instances
(Mul r b r', ExpBase b D8 r) => ExpBase b D9 r'
(Mul r b r', ExpBase b D7 r) => ExpBase b D8 r'
(Mul r b r', ExpBase b D6 r) => ExpBase b D7 r'
(Mul r b r', ExpBase b D5 r) => ExpBase b D6 r'
(Mul r b r', ExpBase b D4 r) => ExpBase b D5 r'
(Mul r b r', ExpBase b D3 r) => ExpBase b D4 r'
(Mul r b r', ExpBase b D2 r) => ExpBase b D3 r'
Mul b b r => ExpBase b D2 r
Nat b => ExpBase b D1 b
Nat b => ExpBase b D0 D1
(Nat b, Pos (:* ei el), Nat r, Mul b r r', Pred (:* ei el) e', ExpBase b e' r) => ExpBase b (:* ei el) r'
(^) :: ExpBase b e r => b -> e -> rSource
value-level reflection function for the ExpBase type-level relation
class (Pos b, b :>=: D2, Pos x, Nat e) => LogBase b x e | b x -> eSource
show/hide Instances
LogBaseF b x e f => LogBase b x e
logBase :: LogBaseF b x e f => b -> x -> eSource
value-level reflection function for LogBase
class (Pos b, b :>=: D2, Pos x, Nat e, Bool f) => LogBaseF b x e f | b x -> e fSource
Version of LogBase which also outputs if the logarithm calculated was exact. f indicates if the resulting logarithm has no fractional part (i.e. tells if the result provided is exact)
show/hide Instances
(Trich x b cmp, LogBaseF' b x e f cmp) => LogBaseF b x e f
logBaseF :: LogBaseF b x e f => b -> x -> (e, f)Source
value-level reflection function for LogBaseF
class (Pos b, b :>=: D2, Pos x) => IsPowOf b x Source
Assert that a number (x) can be expressed as the power of another one (b) (i.e. the fractional part of log_base_b x = 0, or, in a different way, exists y . b^y = x).
show/hide Instances
(Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x
isPowOf :: IsPowOf b x => b -> x -> ()Source
Special efficiency cases
class (Nat x, Pos y) => Exp10 x y | x -> y, y -> xSource
Base-10 Exponentiation type-level relation
show/hide Instances
Exp10 D0 D1
Exp10 D9 (:* (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0) D0)
Exp10 D8 (:* (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0) D0)
Exp10 D7 (:* (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0) D0)
Exp10 D6 (:* (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0) D0)
Exp10 D5 (:* (:* (:* (:* (:* D1 D0) D0) D0) D0) D0)
Exp10 D4 (:* (:* (:* (:* D1 D0) D0) D0) D0)
Exp10 D3 (:* (:* (:* D1 D0) D0) D0)
Exp10 D2 (:* (:* D1 D0) D0)
Exp10 D1 (:* D1 D0)
(Pred (:* xi xl) x', Exp10 x' (:* (:* (:* (:* (:* (:* (:* (:* (:* y D0) D0) D0) D0) D0) D0) D0) D0) D0)) => Exp10 (:* xi xl) (:* (:* (:* (:* (:* (:* (:* (:* (:* (:* y D0) D0) D0) D0) D0) D0) D0) D0) D0) D0)
exp10 :: Exp10 x y => x -> ySource
value-level reflection function for Exp10
class (Pos x, Nat y) => Log10 x y | x -> ySource
Base-10 logarithm type-level relation Note it is not relational (cannot be used to express Exponentation to 10) However, it works with any positive numeral (not just powers of 10)
show/hide Instances
log10 :: Log10 x y => x -> ySource
value-level reflection function for Log10
Comparison assertions
General comparison assertion
class (Nat x, Nat y) => Trich x y r | x y -> rSource
Trichotomy type-level relation. 'Trich x y r' establishes the relation (r) between x and y. The obtained relation (r) Can be LT (if x is lower than y), EQ (if x equals y) or GT (if x is greater than y)
show/hide Instances
Trich D9 D9 EQ
Trich D9 D8 GT
Trich D9 D7 GT
Trich D9 D6 GT
Trich D9 D5 GT
Trich D9 D4 GT
Trich D9 D3 GT
Trich D9 D2 GT
Trich D9 D1 GT
Trich D9 D0 GT
Trich D8 D9 LT
Trich D8 D8 EQ
Trich D8 D7 GT
Trich D8 D6 GT
Trich D8 D5 GT
Trich D8 D4 GT
Trich D8 D3 GT
Trich D8 D2 GT
Trich D8 D1 GT
Trich D8 D0 GT
Trich D7 D9 LT
Trich D7 D8 LT
Trich D7 D7 EQ
Trich D7 D6 GT
Trich D7 D5 GT
Trich D7 D4 GT
Trich D7 D3 GT
Trich D7 D2 GT
Trich D7 D1 GT
Trich D7 D0 GT
Trich D6 D9 LT
Trich D6 D8 LT
Trich D6 D7 LT
Trich D6 D6 EQ
Trich D6 D5 GT
Trich D6 D4 GT
Trich D6 D3 GT
Trich D6 D2 GT
Trich D6 D1 GT
Trich D6 D0 GT
Trich D5 D9 LT
Trich D5 D8 LT
Trich D5 D7 LT
Trich D5 D6 LT
Trich D5 D5 EQ
Trich D5 D4 GT
Trich D5 D3 GT
Trich D5 D2 GT
Trich D5 D1 GT
Trich D5 D0 GT
Trich D4 D9 LT
Trich D4 D8 LT
Trich D4 D7 LT
Trich D4 D6 LT
Trich D4 D5 LT
Trich D4 D4 EQ
Trich D4 D3 GT
Trich D4 D2 GT
Trich D4 D1 GT
Trich D4 D0 GT
Trich D3 D9 LT
Trich D3 D8 LT
Trich D3 D7 LT
Trich D3 D6 LT
Trich D3 D5 LT
Trich D3 D4 LT
Trich D3 D3 EQ
Trich D3 D2 GT
Trich D3 D1 GT
Trich D3 D0 GT
Trich D2 D9 LT
Trich D2 D8 LT
Trich D2 D7 LT
Trich D2 D6 LT
Trich D2 D5 LT
Trich D2 D4 LT
Trich D2 D3 LT
Trich D2 D2 EQ
Trich D2 D1 GT
Trich D2 D0 GT
Trich D1 D9 LT
Trich D1 D8 LT
Trich D1 D7 LT
Trich D1 D6 LT
Trich D1 D5 LT
Trich D1 D4 LT
Trich D1 D3 LT
Trich D1 D2 LT
Trich D1 D1 EQ
Trich D1 D0 GT
Trich D0 D9 LT
Trich D0 D8 LT
Trich D0 D7 LT
Trich D0 D6 LT
Trich D0 D5 LT
Trich D0 D4 LT
Trich D0 D3 LT
Trich D0 D2 LT
Trich D0 D1 LT
Trich D0 D0 EQ
Pos (:* yi yl) => Trich D9 (:* yi yl) LT
Pos (:* yi yl) => Trich D8 (:* yi yl) LT
Pos (:* yi yl) => Trich D7 (:* yi yl) LT
Pos (:* yi yl) => Trich D6 (:* yi yl) LT
Pos (:* yi yl) => Trich D5 (:* yi yl) LT
Pos (:* yi yl) => Trich D4 (:* yi yl) LT
Pos (:* yi yl) => Trich D3 (:* yi yl) LT
Pos (:* yi yl) => Trich D2 (:* yi yl) LT
Pos (:* yi yl) => Trich D1 (:* yi yl) LT
Pos (:* yi yl) => Trich D0 (:* yi yl) LT
Pos (:* yi yl) => Trich (:* yi yl) D9 GT
Pos (:* yi yl) => Trich (:* yi yl) D8 GT
Pos (:* yi yl) => Trich (:* yi yl) D7 GT
Pos (:* yi yl) => Trich (:* yi yl) D6 GT
Pos (:* yi yl) => Trich (:* yi yl) D5 GT
Pos (:* yi yl) => Trich (:* yi yl) D4 GT
Pos (:* yi yl) => Trich (:* yi yl) D3 GT
Pos (:* yi yl) => Trich (:* yi yl) D2 GT
Pos (:* yi yl) => Trich (:* yi yl) D1 GT
Pos (:* yi yl) => Trich (:* yi yl) D0 GT
(Pos (:* xi xl), Pos (:* yi yl), Trich xl yl rl, Trich xi yi ri, CS ri rl r) => Trich (:* xi xl) (:* yi yl) r
trich :: Trich x y r => z -> x -> rSource
value-level reflection function for the comparison type-level assertion
Type-level values denoting comparison results
data LT Source
Lower than
show/hide Instances
CS LT r LT
Trich D8 D9 LT
Trich D7 D9 LT
Trich D7 D8 LT
Trich D6 D9 LT
Trich D6 D8 LT
Trich D6 D7 LT
Trich D5 D9 LT
Trich D5 D8 LT
Trich D5 D7 LT
Trich D5 D6 LT
Trich D4 D9 LT
Trich D4 D8 LT
Trich D4 D7 LT
Trich D4 D6 LT
Trich D4 D5 LT
Trich D3 D9 LT
Trich D3 D8 LT
Trich D3 D7 LT
Trich D3 D6 LT
Trich D3 D5 LT
Trich D3 D4 LT
Trich D2 D9 LT
Trich D2 D8 LT
Trich D2 D7 LT
Trich D2 D6 LT
Trich D2 D5 LT
Trich D2 D4 LT
Trich D2 D3 LT
Trich D1 D9 LT
Trich D1 D8 LT
Trich D1 D7 LT
Trich D1 D6 LT
Trich D1 D5 LT
Trich D1 D4 LT
Trich D1 D3 LT
Trich D1 D2 LT
Trich D0 D9 LT
Trich D0 D8 LT
Trich D0 D7 LT
Trich D0 D6 LT
Trich D0 D5 LT
Trich D0 D4 LT
Trich D0 D3 LT
Trich D0 D2 LT
Trich D0 D1 LT
Max' x y LT y
(Nat x, Nat y, GCD y x gcd) => GCD' x y False LT gcd
(Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT
(Nat x, Pos y) => DivMod' x y D0 x LT
Pos (:* yi yl) => Trich D9 (:* yi yl) LT
Pos (:* yi yl) => Trich D8 (:* yi yl) LT
Pos (:* yi yl) => Trich D7 (:* yi yl) LT
Pos (:* yi yl) => Trich D6 (:* yi yl) LT
Pos (:* yi yl) => Trich D5 (:* yi yl) LT
Pos (:* yi yl) => Trich D4 (:* yi yl) LT
Pos (:* yi yl) => Trich D3 (:* yi yl) LT
Pos (:* yi yl) => Trich D2 (:* yi yl) LT
Pos (:* yi yl) => Trich D1 (:* yi yl) LT
Pos (:* yi yl) => Trich D0 (:* yi yl) LT
data EQ Source
Equal
show/hide Instances
CS EQ r r
Trich D9 D9 EQ
Trich D8 D8 EQ
Trich D7 D7 EQ
Trich D6 D6 EQ
Trich D5 D5 EQ
Trich D4 D4 EQ
Trich D3 D3 EQ
Trich D2 D2 EQ
Trich D1 D1 EQ
Trich D0 D0 EQ
(Pos b, b :>=: D2) => IsPowOf' b b EQ
Max' x y EQ y
Nat x => GCD' x x False EQ x
(Pos b, b :>=: D2) => LogBaseF' b b D1 True EQ
(Nat x, Pos y) => DivMod' x y D1 D0 EQ
data GT Source
Greater than
show/hide Instances
CS GT r GT
Trich D9 D8 GT
Trich D9 D7 GT
Trich D9 D6 GT
Trich D9 D5 GT
Trich D9 D4 GT
Trich D9 D3 GT
Trich D9 D2 GT
Trich D9 D1 GT
Trich D9 D0 GT
Trich D8 D7 GT
Trich D8 D6 GT
Trich D8 D5 GT
Trich D8 D4 GT
Trich D8 D3 GT
Trich D8 D2 GT
Trich D8 D1 GT
Trich D8 D0 GT
Trich D7 D6 GT
Trich D7 D5 GT
Trich D7 D4 GT
Trich D7 D3 GT
Trich D7 D2 GT
Trich D7 D1 GT
Trich D7 D0 GT
Trich D6 D5 GT
Trich D6 D4 GT
Trich D6 D3 GT
Trich D6 D2 GT
Trich D6 D1 GT
Trich D6 D0 GT
Trich D5 D4 GT
Trich D5 D3 GT
Trich D5 D2 GT
Trich D5 D1 GT
Trich D5 D0 GT
Trich D4 D3 GT
Trich D4 D2 GT
Trich D4 D1 GT
Trich D4 D0 GT
Trich D3 D2 GT
Trich D3 D1 GT
Trich D3 D0 GT
Trich D2 D1 GT
Trich D2 D0 GT
Trich D1 D0 GT
(Pos b, b :>=: D2, Pos x, DivMod x b q D0, IsPowOf b q) => IsPowOf' b x GT
Max' x y GT x
(Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCD' x y False GT gcd
(Pos b, b :>=: D2, Pos x, DivMod x b q r, IsZero r rz, And rz f' f, Pred e e', LogBaseF b q e' f') => LogBaseF' b x e f GT
(Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r) => DivMod' x y q r GT
Pos (:* yi yl) => Trich (:* yi yl) D9 GT
Pos (:* yi yl) => Trich (:* yi yl) D8 GT
Pos (:* yi yl) => Trich (:* yi yl) D7 GT
Pos (:* yi yl) => Trich (:* yi yl) D6 GT
Pos (:* yi yl) => Trich (:* yi yl) D5 GT
Pos (:* yi yl) => Trich (:* yi yl) D4 GT
Pos (:* yi yl) => Trich (:* yi yl) D3 GT
Pos (:* yi yl) => Trich (:* yi yl) D2 GT
Pos (:* yi yl) => Trich (:* yi yl) D1 GT
Pos (:* yi yl) => Trich (:* yi yl) D0 GT
Abbreviated comparison assertions
class x :==: y Source
Equality abbreviated type-level assertion
show/hide Instances
Trich x y EQ => x :==: y
class x :>: y Source
Greater-than abbreviated type-level assertion
show/hide Instances
Trich x y GT => x :>: y
class x :<: y Source
Lower-than abbreviated type-level assertion
show/hide Instances
Trich x y LT => x :<: y
class x :>=: y Source
Greater-than or equal abbreviated type-level assertion
show/hide Instances
(Succ x x', Trich x' y GT) => x :>=: y
class x :<=: y Source
Lower-than or equal abbreviated type-level assertion
show/hide Instances
(Succ x' x, Trich x' y LT) => x :<=: y
(==) :: x :==: y => x -> y -> ()Source
value-level reflection function for the equality abbreviated type-level assertion
(>) :: x :>: y => x -> y -> ()Source
value-level reflection function for the equality abbreviated type-level assertion
(<) :: x :<: y => x -> y -> ()Source
value-level reflection function for the lower-than abbreviated type-level assertion
(>=) :: x :>=: y => x -> y -> ()Source
value-level reflection function for the greater-than or equal abbreviated type-level assertion
(<=) :: x :<=: y => x -> y -> ()Source
value-level reflection function for the lower-than or equal abbreviated type-level assertion
Maximum/Minimum
class Max x y z | x y -> zSource
Maximum type-level relation
show/hide Instances
(Max' x y b z, Trich x y b) => Max x y z
max :: Max x y z => x -> y -> zSource
value-level reflection function for the maximum type-level relation
class Min x y z | x y -> zSource
Minimum type-level relation
show/hide Instances
(Max' y x b z, Trich x y b) => Min x y z
min :: Min x y z => x -> y -> zSource
value-level reflection function for the minimum type-level relation
Greatest Common Divisor
class (Nat x, Nat y, Nat gcd) => GCD x y gcd | x y -> gcdSource
Greatest Common Divisor type-level relation
show/hide Instances
(Nat x, Nat y, Trich x y cmp, IsZero y yz, GCD' x y yz cmp gcd) => GCD x y gcd
gcd :: GCD x y z => x -> y -> zSource
value-level reflection function for the GCD type-level relation
Produced by Haddock version 2.6.1