| 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 m = n ~ Gcd n m
- type family Div (a :: Nat ) (b :: Nat ) :: Nat where ...
- type family Mod (a :: Nat ) (b :: Nat ) :: Nat where ...
- plusNat :: forall n m. ( KnownNat n, KnownNat m) :- KnownNat (n + m)
- minusNat :: forall n m. ( KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
- timesNat :: forall n m. ( KnownNat n, KnownNat m) :- KnownNat (n * m)
- powNat :: forall n m. ( KnownNat n, KnownNat m) :- KnownNat (n ^ m)
- minNat :: forall n m. ( KnownNat n, KnownNat m) :- KnownNat ( Min n m)
- maxNat :: forall n m. ( KnownNat n, KnownNat m) :- KnownNat ( Max n m)
- gcdNat :: forall n m. ( KnownNat n, KnownNat m) :- KnownNat ( Gcd n m)
- lcmNat :: forall n m. ( KnownNat n, KnownNat m) :- KnownNat ( Lcm n m)
- divNat :: forall n m. ( KnownNat n, KnownNat m, 1 <= m) :- KnownNat ( Div n m)
- modNat :: forall n m. ( KnownNat n, KnownNat m, 1 <= m) :- KnownNat ( Mod n m)
- plusZero :: forall n. Dict ((n + 0) ~ n)
- minusZero :: forall n. Dict ((n - 0) ~ n)
- timesZero :: forall n. Dict ((n * 0) ~ 0)
- timesOne :: forall n. Dict ((n * 1) ~ n)
- powZero :: forall n. Dict ((n ^ 0) ~ 1)
- powOne :: forall n. Dict ((n ^ 1) ~ n)
- maxZero :: forall n. Dict ( Max n 0 ~ n)
- minZero :: forall n. Dict ( Min n 0 ~ 0)
- gcdZero :: forall a. Dict ( Gcd 0 a ~ a)
- gcdOne :: forall a. Dict ( Gcd 1 a ~ 1)
- lcmZero :: forall a. Dict ( Lcm 0 a ~ 0)
- lcmOne :: forall a. Dict ( Lcm 1 a ~ a)
- plusAssociates :: forall m n o. Dict (((m + n) + o) ~ (m + (n + o)))
- timesAssociates :: forall m n o. Dict (((m * n) * o) ~ (m * (n * o)))
- minAssociates :: forall m n o. Dict ( Min ( Min m n) o ~ Min m ( Min n o))
- maxAssociates :: forall m n o. Dict ( Max ( Max m n) o ~ Max m ( Max n o))
- gcdAssociates :: forall a b c. Dict ( Gcd ( Gcd a b) c ~ Gcd a ( Gcd b c))
- lcmAssociates :: forall a b c. Dict ( Lcm ( Lcm a b) c ~ Lcm a ( Lcm b c))
- plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))
- timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))
- minCommutes :: forall n m. Dict ( Min m n ~ Min n m)
- maxCommutes :: forall n m. Dict ( Max m n ~ Max n m)
- gcdCommutes :: forall a b. Dict ( Gcd a b ~ Gcd b a)
- lcmCommutes :: forall a b. Dict ( Lcm a b ~ Lcm b a)
- plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ ((n * m) + (n * o)))
- timesDistributesOverPow :: forall n m o. Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))
- timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
- timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
- minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))
- minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))
- minDistributesOverPow1 :: forall n m o. Dict (( Min n m ^ o) ~ Min (n ^ o) (m ^ o))
- minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
- minDistributesOverMax :: forall n m o. Dict ( Max n ( Min m o) ~ Min ( Max n m) ( Max n o))
- maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))
- maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))
- maxDistributesOverPow1 :: forall n m o. Dict (( Max n m ^ o) ~ Max (n ^ o) (m ^ o))
- maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
- maxDistributesOverMin :: forall n m o. Dict ( Min n ( Max m o) ~ Max ( Min n m) ( Min n o))
- gcdDistributesOverLcm :: forall a b c. Dict ( Gcd ( Lcm a b) c ~ Lcm ( Gcd a c) ( Gcd b c))
- lcmDistributesOverGcd :: forall a b c. Dict ( Lcm ( Gcd a b) c ~ Gcd ( Lcm a c) ( Lcm b c))
- minIsIdempotent :: forall n. Dict ( Min n n ~ n)
- maxIsIdempotent :: forall n. Dict ( Max n n ~ n)
- lcmIsIdempotent :: forall n. Dict ( Lcm n n ~ n)
- gcdIsIdempotent :: forall n. Dict ( Gcd n n ~ n)
- plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)
- timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
- dividesPlus :: ( Divides a b, Divides a c) :- Divides a (b + c)
- dividesTimes :: Divides a b :- Divides a (b * c)
- dividesMin :: ( Divides a b, Divides a c) :- Divides a ( Min b c)
- dividesMax :: ( Divides a b, Divides a c) :- Divides a ( Max b c)
- dividesPow :: (1 <= n, Divides a b) :- Divides a (b ^ n)
- dividesGcd :: forall a b c. ( Divides a b, Divides a c) :- Divides a ( Gcd b c)
- dividesLcm :: forall a b c. ( Divides a c, Divides b c) :- Divides ( Lcm a b) c
- plusMonotone1 :: forall a b c. (a <= b) :- ((a + c) <= (b + c))
- plusMonotone2 :: forall a b c. (b <= c) :- ((a + b) <= (a + c))
- timesMonotone1 :: forall a b c. (a <= b) :- ((a * c) <= (b * c))
- timesMonotone2 :: forall a b c. (b <= c) :- ((a * b) <= (a * c))
- powMonotone1 :: forall a b c. (a <= b) :- ((a ^ c) <= (b ^ c))
- powMonotone2 :: forall a b c. (b <= c) :- ((a ^ b) <= (a ^ c))
- minMonotone1 :: forall a b c. (a <= b) :- ( Min a c <= Min b c)
- minMonotone2 :: forall a b c. (b <= c) :- ( Min a b <= Min a c)
- maxMonotone1 :: forall a b c. (a <= b) :- ( Max a c <= Max b c)
- maxMonotone2 :: forall a b c. (b <= c) :- ( Max a b <= Max a c)
- divMonotone1 :: forall a b c. (a <= b) :- ( Div a c <= Div b c)
- divMonotone2 :: forall a b c. (b <= c) :- ( Div a c <= Div a b)
- euclideanNat :: (1 <= c) :- (a ~ ((c * Div a c) + Mod a c))
- plusMod :: forall a b c. (1 <= c) :- ( Mod (a + b) c ~ Mod ( Mod a c + Mod b c) c)
- timesMod :: forall a b c. (1 <= c) :- ( Mod (a * b) c ~ Mod ( Mod a c * Mod b c) c)
- modBound :: forall m n. (1 <= n) :- ( Mod m n <= n)
- dividesDef :: forall a b. Divides a b :- ( Mod b a ~ 0)
- timesDiv :: forall a b. 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. (a <= 0) :- (a ~ 0)
- zeroLe :: forall (a :: Nat ). Dict (0 <= a)
- plusMinusInverse1 :: forall n m. Dict (((m + n) - n) ~ m)
- plusMinusInverse2 :: forall n m. (m <= n) :- (((m + n) - m) ~ n)
- plusMinusInverse3 :: forall n m. (n <= m) :- (((m - n) + n) ~ m)
Documentation
type family Div (a :: Nat ) (b :: Nat ) :: Nat where ... infixl 7 Source #
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 :: Nat ) (b :: Nat ) :: Nat where ... infixl 7 Source #
Modulus of natural numbers.
Mod x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
minDistributesOverMax :: forall n m o. Dict ( Max n ( Min m o) ~ Min ( Max n m) ( Max n o)) Source #
maxDistributesOverMin :: forall n m o. Dict ( Min n ( Max m o) ~ Max ( Min n m) ( Min n o)) Source #
gcdDistributesOverLcm :: forall a b c. Dict ( Gcd ( Lcm a b) c ~ Lcm ( Gcd a c) ( Gcd b c)) Source #
lcmDistributesOverGcd :: forall a b c. Dict ( Lcm ( Gcd a b) c ~ Gcd ( Lcm a c) ( Lcm b c)) Source #
minIsIdempotent :: forall n. Dict ( Min n n ~ n) Source #
maxIsIdempotent :: forall n. Dict ( Max n n ~ n) Source #
lcmIsIdempotent :: forall n. Dict ( Lcm n n ~ n) Source #
gcdIsIdempotent :: forall n. Dict ( Gcd n n ~ n) Source #