Safe Haskell	Trustworthy
Language	Haskell2010

Data.Constraint.Nat

Description

Utilities for working with KnownNat constraints.

This module is only available on GHC 8.0 or later.

Synopsis

type family Min (m :: Nat) (n :: Nat) :: Nat where ...
type family Max (m :: Nat) (n :: Nat) :: Nat where ...
type family Lcm (m :: Nat) (n :: Nat) :: Nat where ...
type family Gcd (m :: Nat) (n :: Nat) :: Nat where ...
type Divides (n :: Nat) (m :: Nat) = n ~ Gcd n m
type family Div (a :: Natural) (b :: Natural) :: Natural where ...
type family Mod (a :: Natural) (b :: Natural) :: Natural where ...
type family Log2 (a :: Natural) :: Natural where ...
plusNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n + m)
minusNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
timesNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n * m)
powNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
minNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Min n m)
maxNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Max n m)
gcdNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
lcmNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
divNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
modNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
log2Nat :: forall (n :: Nat). (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
plusZero :: forall (n :: Natural). Dict ((n + 0) ~ n)
minusZero :: forall (n :: Natural). Dict ((n - 0) ~ n)
timesZero :: forall (n :: Natural). Dict ((n * 0) ~ 0)
timesOne :: forall (n :: Natural). Dict ((n * 1) ~ n)
powZero :: forall (n :: Natural). Dict ((n ^ 0) ~ 1)
powOne :: forall (n :: Natural). Dict ((n ^ 1) ~ n)
maxZero :: forall (n :: Nat). Dict (Max n 0 ~ n)
minZero :: forall (n :: Nat). Dict (Min n 0 ~ 0)
gcdZero :: forall (a :: Nat). Dict (Gcd 0 a ~ a)
gcdOne :: forall (a :: Nat). Dict (Gcd 1 a ~ 1)
lcmZero :: forall (a :: Nat). Dict (Lcm 0 a ~ 0)
lcmOne :: forall (a :: Nat). Dict (Lcm 1 a ~ a)
plusAssociates :: forall (m :: Natural) (n :: Natural) (o :: Natural). Dict (((m + n) + o) ~ (m + (n + o)))
timesAssociates :: forall (m :: Natural) (n :: Natural) (o :: Natural). Dict (((m * n) * o) ~ (m * (n * o)))
minAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat). Dict (Min (Min m n) o ~ Min m (Min n o))
maxAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat). Dict (Max (Max m n) o ~ Max m (Max n o))
gcdAssociates :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))
lcmAssociates :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
plusCommutes :: forall (n :: Natural) (m :: Natural). Dict ((m + n) ~ (n + m))
timesCommutes :: forall (n :: Natural) (m :: Natural). Dict ((m * n) ~ (n * m))
minCommutes :: forall (n :: Nat) (m :: Nat). Dict (Min m n ~ Min n m)
maxCommutes :: forall (n :: Nat) (m :: Nat). Dict (Max m n ~ Max n m)
gcdCommutes :: forall (a :: Nat) (b :: Nat). Dict (Gcd a b ~ Gcd b a)
lcmCommutes :: forall (a :: Nat) (b :: Nat). Dict (Lcm a b ~ Lcm b a)
plusDistributesOverTimes :: forall (n :: Natural) (m :: Natural) (o :: Natural). Dict ((n * (m + o)) ~ ((n * m) + (n * o)))
timesDistributesOverPow :: forall (n :: Natural) (m :: Natural) (o :: Natural). Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))
timesDistributesOverGcd :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
timesDistributesOverLcm :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
minDistributesOverPlus :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n + Min m o) ~ Min (n + m) (n + o))
minDistributesOverTimes :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Min m o) ~ Min (n * m) (n * o))
minDistributesOverPow1 :: forall (n :: Nat) (m :: Nat) (o :: Natural). Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
minDistributesOverPow2 :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
minDistributesOverMax :: forall (n :: Nat) (m :: Nat) (o :: Nat). Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
maxDistributesOverPlus :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n + Max m o) ~ Max (n + m) (n + o))
maxDistributesOverTimes :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Max m o) ~ Max (n * m) (n * o))
maxDistributesOverPow1 :: forall (n :: Nat) (m :: Nat) (o :: Natural). Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
maxDistributesOverPow2 :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
maxDistributesOverMin :: forall (n :: Nat) (m :: Nat) (o :: Nat). Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
gcdDistributesOverLcm :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
lcmDistributesOverGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
minIsIdempotent :: forall (n :: Nat). Dict (Min n n ~ n)
maxIsIdempotent :: forall (n :: Nat). Dict (Max n n ~ n)
lcmIsIdempotent :: forall (n :: Nat). Dict (Lcm n n ~ n)
gcdIsIdempotent :: forall (n :: Nat). Dict (Gcd n n ~ n)
plusIsCancellative :: forall (n :: Natural) (m :: Natural) (o :: Natural). ((n + m) ~ (n + o)) :- (m ~ o)
timesIsCancellative :: forall (n :: Natural) (m :: Natural) (o :: Natural). (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
dividesPlus :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (b + c)
dividesTimes :: forall (a :: Nat) (b :: Nat) (c :: Natural). Divides a b :- Divides a (b * c)
dividesMin :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Min b c)
dividesMax :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Max b c)
dividesPow :: forall (n :: Natural) (a :: Nat) (b :: Nat). (1 <= n, Divides a b) :- Divides a (b ^ n)
dividesGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Gcd b c)
dividesLcm :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a c, Divides b c) :- Divides (Lcm a b) c
plusMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a + c) <= (b + c))
plusMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a + b) <= (a + c))
timesMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a * c) <= (b * c))
timesMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a * b) <= (a * c))
powMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a ^ c) <= (b ^ c))
powMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a ^ b) <= (a ^ c))
minMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b) :- (Min a c <= Min b c)
minMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c) :- (Min a b <= Min a c)
maxMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b) :- (Max a c <= Max b c)
maxMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c) :- (Max a b <= Max a c)
divMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- (Div a c <= Div b c)
divMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- (Div a c <= Div a b)
euclideanNat :: forall (c :: Natural) (a :: Natural). (1 <= c) :- (a ~ ((c * Div a c) + Mod a c))
plusMod :: forall (a :: Natural) (b :: Natural) (c :: Natural). (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
timesMod :: forall (a :: Natural) (b :: Natural) (c :: Natural). (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
modBound :: forall (m :: Natural) (n :: Natural). (1 <= n) :- (Mod m n <= n)
log2Pow :: forall (n :: Natural). Dict (Log2 (2 ^ n) ~ n)
dividesDef :: forall (a :: Nat) (b :: Nat). Divides a b :- (Mod b a ~ 0)
timesDiv :: forall (a :: Natural) (b :: Natural). Dict ((a * Div b a) <= b)
eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b)
leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)
leId :: forall (a :: Nat). Dict (a <= a)
leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c)
leZero :: forall (a :: Natural). (a <= 0) :- (a ~ 0)
zeroLe :: forall (a :: Nat). Dict (0 <= a)
plusMinusInverse1 :: forall (n :: Natural) (m :: Natural). Dict (((m + n) - n) ~ m)
plusMinusInverse2 :: forall (n :: Natural) (m :: Natural). (m <= n) :- (((m + n) - m) ~ n)
plusMinusInverse3 :: forall (n :: Natural) (m :: Natural). (n <= m) :- (((m - n) + n) ~ m)

Documentation

type family Min (m :: Nat) (n :: Nat) :: Nat where ... Source #

Equations

Min m n = If (n <=? m) n m

type family Max (m :: Nat) (n :: Nat) :: Nat where ... Source #

Equations

Max m n = If (n <=? m) m n

type family Lcm (m :: Nat) (n :: Nat) :: Nat where ... Source #

Equations

Lcm m m = m

type family Gcd (m :: Nat) (n :: Nat) :: Nat where ... Source #

Equations

Gcd m m = m

type Divides (n :: Nat) (m :: Nat) = n ~ Gcd n m Source #

type family Div (a :: Natural) (b :: Natural) :: Natural where ... infixl 7 #

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Mod (a :: Natural) (b :: Natural) :: Natural where ... infixl 7 #

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Log2 (a :: Natural) :: Natural where ... #

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

plusNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n + m) Source #

minusNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m) Source #

timesNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n * m) Source #

powNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n ^ m) Source #

minNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Min n m) Source #

maxNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Max n m) Source #

gcdNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Gcd n m) Source #

lcmNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Lcm n m) Source #

divNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m) Source #

modNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m) Source #

log2Nat :: forall (n :: Nat). (KnownNat n, 1 <= n) :- KnownNat (Log2 n) Source #

plusZero :: forall (n :: Natural). Dict ((n + 0) ~ n) Source #

minusZero :: forall (n :: Natural). Dict ((n - 0) ~ n) Source #

timesZero :: forall (n :: Natural). Dict ((n * 0) ~ 0) Source #

timesOne :: forall (n :: Natural). Dict ((n * 1) ~ n) Source #

powZero :: forall (n :: Natural). Dict ((n ^ 0) ~ 1) Source #

powOne :: forall (n :: Natural). Dict ((n ^ 1) ~ n) Source #

maxZero :: forall (n :: Nat). Dict (Max n 0 ~ n) Source #

minZero :: forall (n :: Nat). Dict (Min n 0 ~ 0) Source #

gcdZero :: forall (a :: Nat). Dict (Gcd 0 a ~ a) Source #

gcdOne :: forall (a :: Nat). Dict (Gcd 1 a ~ 1) Source #

lcmZero :: forall (a :: Nat). Dict (Lcm 0 a ~ 0) Source #

lcmOne :: forall (a :: Nat). Dict (Lcm 1 a ~ a) Source #

plusAssociates :: forall (m :: Natural) (n :: Natural) (o :: Natural). Dict (((m + n) + o) ~ (m + (n + o))) Source #

timesAssociates :: forall (m :: Natural) (n :: Natural) (o :: Natural). Dict (((m * n) * o) ~ (m * (n * o))) Source #

minAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat). Dict (Min (Min m n) o ~ Min m (Min n o)) Source #

maxAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat). Dict (Max (Max m n) o ~ Max m (Max n o)) Source #

gcdAssociates :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c)) Source #

lcmAssociates :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c)) Source #

plusCommutes :: forall (n :: Natural) (m :: Natural). Dict ((m + n) ~ (n + m)) Source #

timesCommutes :: forall (n :: Natural) (m :: Natural). Dict ((m * n) ~ (n * m)) Source #

minCommutes :: forall (n :: Nat) (m :: Nat). Dict (Min m n ~ Min n m) Source #

maxCommutes :: forall (n :: Nat) (m :: Nat). Dict (Max m n ~ Max n m) Source #

gcdCommutes :: forall (a :: Nat) (b :: Nat). Dict (Gcd a b ~ Gcd b a) Source #

lcmCommutes :: forall (a :: Nat) (b :: Nat). Dict (Lcm a b ~ Lcm b a) Source #

plusDistributesOverTimes :: forall (n :: Natural) (m :: Natural) (o :: Natural). Dict ((n * (m + o)) ~ ((n * m) + (n * o))) Source #

timesDistributesOverPow :: forall (n :: Natural) (m :: Natural) (o :: Natural). Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o))) Source #

timesDistributesOverGcd :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o)) Source #

timesDistributesOverLcm :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o)) Source #

minDistributesOverPlus :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n + Min m o) ~ Min (n + m) (n + o)) Source #

minDistributesOverTimes :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Min m o) ~ Min (n * m) (n * o)) Source #

minDistributesOverPow1 :: forall (n :: Nat) (m :: Nat) (o :: Natural). Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o)) Source #

minDistributesOverPow2 :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o)) Source #

minDistributesOverMax :: forall (n :: Nat) (m :: Nat) (o :: Nat). Dict (Max n (Min m o) ~ Min (Max n m) (Max n o)) Source #

maxDistributesOverPlus :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n + Max m o) ~ Max (n + m) (n + o)) Source #

maxDistributesOverTimes :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Max m o) ~ Max (n * m) (n * o)) Source #

maxDistributesOverPow1 :: forall (n :: Nat) (m :: Nat) (o :: Natural). Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o)) Source #

maxDistributesOverPow2 :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o)) Source #

maxDistributesOverMin :: forall (n :: Nat) (m :: Nat) (o :: Nat). Dict (Min n (Max m o) ~ Max (Min n m) (Min n o)) Source #

gcdDistributesOverLcm :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c)) Source #

lcmDistributesOverGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c)) Source #

minIsIdempotent :: forall (n :: Nat). Dict (Min n n ~ n) Source #

maxIsIdempotent :: forall (n :: Nat). Dict (Max n n ~ n) Source #

lcmIsIdempotent :: forall (n :: Nat). Dict (Lcm n n ~ n) Source #

gcdIsIdempotent :: forall (n :: Nat). Dict (Gcd n n ~ n) Source #

plusIsCancellative :: forall (n :: Natural) (m :: Natural) (o :: Natural). ((n + m) ~ (n + o)) :- (m ~ o) Source #

timesIsCancellative :: forall (n :: Natural) (m :: Natural) (o :: Natural). (1 <= n, (n * m) ~ (n * o)) :- (m ~ o) Source #

dividesPlus :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (b + c) Source #

dividesTimes :: forall (a :: Nat) (b :: Nat) (c :: Natural). Divides a b :- Divides a (b * c) Source #

dividesMin :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Min b c) Source #

dividesMax :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Max b c) Source #

dividesPow :: forall (n :: Natural) (a :: Nat) (b :: Nat). (1 <= n, Divides a b) :- Divides a (b ^ n) Source #

dividesGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Gcd b c) Source #

dividesLcm :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a c, Divides b c) :- Divides (Lcm a b) c Source #

plusMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a + c) <= (b + c)) Source #

plusMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a + b) <= (a + c)) Source #

timesMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a * c) <= (b * c)) Source #

timesMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a * b) <= (a * c)) Source #

powMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a ^ c) <= (b ^ c)) Source #

powMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a ^ b) <= (a ^ c)) Source #

minMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b) :- (Min a c <= Min b c) Source #

minMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c) :- (Min a b <= Min a c) Source #

maxMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b) :- (Max a c <= Max b c) Source #

maxMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c) :- (Max a b <= Max a c) Source #

divMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- (Div a c <= Div b c) Source #

divMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- (Div a c <= Div a b) Source #

euclideanNat :: forall (c :: Natural) (a :: Natural). (1 <= c) :- (a ~ ((c * Div a c) + Mod a c)) Source #

plusMod :: forall (a :: Natural) (b :: Natural) (c :: Natural). (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c) Source #

timesMod :: forall (a :: Natural) (b :: Natural) (c :: Natural). (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c) Source #

modBound :: forall (m :: Natural) (n :: Natural). (1 <= n) :- (Mod m n <= n) Source #

log2Pow :: forall (n :: Natural). Dict (Log2 (2 ^ n) ~ n) Source #

dividesDef :: forall (a :: Nat) (b :: Nat). Divides a b :- (Mod b a ~ 0) Source #

timesDiv :: forall (a :: Natural) (b :: Natural). Dict ((a * Div b a) <= b) Source #

eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b) Source #

leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b) Source #

leId :: forall (a :: Nat). Dict (a <= a) Source #

leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c) Source #

leZero :: forall (a :: Natural). (a <= 0) :- (a ~ 0) Source #

zeroLe :: forall (a :: Nat). Dict (0 <= a) Source #

plusMinusInverse1 :: forall (n :: Natural) (m :: Natural). Dict (((m + n) - n) ~ m) Source #

plusMinusInverse2 :: forall (n :: Natural) (m :: Natural). (m <= n) :- (((m + n) - m) ~ n) Source #

plusMinusInverse3 :: forall (n :: Natural) (m :: Natural). (n <= m) :- (((m - n) + n) ~ m) Source #