Nat

data Nat #

class KnownNat (n :: Nat) #

natVal :: KnownNat n => proxy n -> Integer #

natVal' :: KnownNat n => Proxy# n -> Integer #

data SomeNat where #

someNatVal :: Integer -> Maybe SomeNat #

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) #

type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ True infix 4 #

type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 #

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #

type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #

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 :: Nat) (b :: Nat) :: Nat where ... infixl 7 #

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

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

type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #

plusNat :: (KnownNat n, KnownNat m) :- KnownNat (n + m) #

timesNat :: (KnownNat n, KnownNat m) :- KnownNat (n * m) #

powNat :: (KnownNat n, KnownNat m) :- KnownNat (n ^ m) #

minNat :: (KnownNat n, KnownNat m) :- KnownNat (Min n m) #

maxNat :: (KnownNat n, KnownNat m) :- KnownNat (Max n m) #

gcdNat :: (KnownNat n, KnownNat m) :- KnownNat (Gcd n m) #

lcmNat :: (KnownNat n, KnownNat m) :- KnownNat (Lcm n m) #

divNat :: (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m) #

modNat :: (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m) #

plusZero :: Dict ((n + 0) ~ n) #

timesZero :: Dict ((n * 0) ~ 0) #

timesOne :: Dict ((n * 1) ~ n) #

powZero :: Dict ((n ^ 0) ~ 1) #

powOne :: Dict ((n ^ 1) ~ n) #

maxZero :: Dict (Max n 0 ~ n) #

minZero :: Dict (Min n 0 ~ 0) #

gcdZero :: Dict (Gcd 0 a ~ a) #

gcdOne :: Dict (Gcd 1 a ~ 1) #

lcmZero :: Dict (Lcm 0 a ~ 0) #

lcmOne :: Dict (Lcm 1 a ~ a) #

plusAssociates :: Dict (((m + n) + o) ~ (m + (n + o))) #

timesAssociates :: Dict (((m * n) * o) ~ (m * (n * o))) #

minAssociates :: Dict (Min (Min m n) o ~ Min m (Min n o)) #

maxAssociates :: Dict (Max (Max m n) o ~ Max m (Max n o)) #

gcdAssociates :: Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c)) #

lcmAssociates :: Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c)) #

plusCommutes :: Dict ((m + n) ~ (n + m)) #

timesCommutes :: Dict ((m * n) ~ (n * m)) #

minCommutes :: Dict (Min m n ~ Min n m) #

maxCommutes :: Dict (Max m n ~ Max n m) #

gcdCommutes :: Dict (Gcd a b ~ Gcd b a) #

lcmCommutes :: Dict (Lcm a b ~ Lcm b a) #

plusDistributesOverTimes :: Dict ((n * (m + o)) ~ ((n * m) + (n * o))) #

timesDistributesOverPow :: Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o))) #

timesDistributesOverGcd :: Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o)) #

timesDistributesOverLcm :: Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o)) #

minDistributesOverPlus :: Dict ((n + Min m o) ~ Min (n + m) (n + o)) #

minDistributesOverTimes :: Dict ((n * Min m o) ~ Min (n * m) (n * o)) #

minDistributesOverPow1 :: Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o)) #

minDistributesOverPow2 :: Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o)) #

minDistributesOverMax :: Dict (Max n (Min m o) ~ Min (Max n m) (Max n o)) #

maxDistributesOverPlus :: Dict ((n + Max m o) ~ Max (n + m) (n + o)) #

maxDistributesOverTimes :: Dict ((n * Max m o) ~ Max (n * m) (n * o)) #

maxDistributesOverPow1 :: Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o)) #

maxDistributesOverPow2 :: Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o)) #

maxDistributesOverMin :: Dict (Min n (Max m o) ~ Max (Min n m) (Min n o)) #

gcdDistributesOverLcm :: Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c)) #

lcmDistributesOverGcd :: Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c)) #

minIsIdempotent :: Dict (Min n n ~ n) #

maxIsIdempotent :: Dict (Max n n ~ n) #

lcmIsIdempotent :: Dict (Lcm n n ~ n) #

gcdIsIdempotent :: Dict (Gcd n n ~ n) #

plusIsCancellative :: ((n + m) ~ (n + o)) :- (m ~ o) #

timesIsCancellative :: (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 c) :- 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 :: (Divides a b, Divides a c) :- Divides a (Gcd b c) #

dividesLcm :: (Divides a c, Divides b c) :- Divides (Lcm a b) c #

plusMonotone1 :: (a <= b) :- ((a + c) <= (b + c)) #

plusMonotone2 :: (b <= c) :- ((a + b) <= (a + c)) #

timesMonotone1 :: (a <= b) :- ((a * c) <= (b * c)) #

timesMonotone2 :: (b <= c) :- ((a * b) <= (a * c)) #

powMonotone1 :: (a <= b) :- ((a ^ c) <= (b ^ c)) #

powMonotone2 :: (b <= c) :- ((a ^ b) <= (a ^ c)) #

minMonotone1 :: (a <= b) :- (Min a c <= Min b c) #

minMonotone2 :: (b <= c) :- (Min a b <= Min a c) #

maxMonotone1 :: (a <= b) :- (Max a c <= Max b c) #

maxMonotone2 :: (b <= c) :- (Max a b <= Max a c) #

divMonotone1 :: (a <= b) :- (Div a c <= Div b c) #

divMonotone2 :: (b <= c) :- (Div a c <= Div a b) #

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

plusMod :: (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c) #

timesMod :: (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c) #

modBound :: (1 <= n) :- (Mod m n <= n) #

dividesDef :: Divides a b :- ((a * Div b a) ~ a) #

timesDiv :: Dict ((a * Div b a) <= a) #

eqLe :: (a ~ b) :- (a <= b) #

leEq :: (a <= b, b <= a) :- (a ~ b) #

leId :: Dict (a <= a) #

leTrans :: (b <= c, a <= b) :- (a <= c) #

zeroLe :: Dict (0 <= a) #

plusMinusInverse1 :: Dict (((m + n) - n) ~ m) #

plusMinusInverse2 :: (m <= n) :- (((m + n) - m) ~ n) #

plusMinusInverse3 :: (n <= m) :- (((m - n) + n) ~ m) #