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.
Documentation
minusNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, m <= n) :- KnownNat (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 #
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 #
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 #
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 #
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 #