| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Arithmetic.Lt
Synopsis
- zero :: 0 < 1
- zero# :: (# #) -> 0 <# 1
- substituteL :: (b :=: c) -> (b < a) -> c < a
- substituteR :: (b :=: c) -> (a < b) -> a < c
- incrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a < b) -> (c + a) < (c + b)
- incrementL# :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <# b) -> (c + a) <# (c + b)
- incrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a < b) -> (a + c) < (b + c)
- incrementR# :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <# b) -> (a + c) <# (b + c)
- decrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((c + a) < (c + b)) -> a < b
- decrementL# :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((c + a) <# (c + b)) -> a <# b
- decrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((a + c) < (b + c)) -> a < b
- decrementR# :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((a + c) <# (b + c)) -> a <# b
- weakenL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a < b) -> a < (c + b)
- weakenL# :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <# b) -> a <# (c + b)
- weakenR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a < b) -> a < (b + c)
- weakenR# :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <# b) -> a <# (b + c)
- weakenLhsL# :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((c + a) <# b) -> a <# b
- weakenLhsR# :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((a + c) <# b) -> a <# b
- plus :: (a < b) -> (c <= d) -> (a + c) < (b + d)
- plus# :: (a <# b) -> (c <=# d) -> (a + c) <# (b + d)
- transitive :: (a < b) -> (b < c) -> a < c
- transitive# :: (a <# b) -> (b <# c) -> a <# c
- transitiveNonstrictL :: (a <= b) -> (b < c) -> a < c
- transitiveNonstrictL# :: (a <=# b) -> (b <# c) -> a <# c
- transitiveNonstrictR :: (a < b) -> (b <= c) -> a < c
- transitiveNonstrictR# :: (a <# b) -> (b <=# c) -> a <# c
- reciprocalA :: forall (m :: Nat) (n :: Nat) (p :: Nat). (m < Div n p) -> (p * m) < n
- reciprocalB :: forall (m :: Nat) (n :: Nat) (p :: Nat). (m < (Div (n - 1) p + 1)) -> (p * m) < n
- toLteL :: (a < b) -> (1 + a) <= b
- toLteR :: (a < b) -> (a + 1) <= b
- absurd :: (n < 0) -> void
- constant :: forall a b. CmpNat a b ~ 'LT => a < b
- constant# :: forall a b. CmpNat a b ~ 'LT => (# #) -> a <# b
- lift :: (a <# b) -> a < b
- unlift :: (a < b) -> a <# b
Special Inequalities
Substitution
substituteL :: (b :=: c) -> (b < a) -> c < a Source #
Replace the left-hand side of a strict inequality with an equal number.
substituteR :: (b :=: c) -> (a < b) -> a < c Source #
Replace the right-hand side of a strict inequality with an equal number.
Increment
incrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a < b) -> (c + a) < (c + b) Source #
Add a constant to the left-hand side of both sides of the strict inequality.
incrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a < b) -> (a + c) < (b + c) Source #
Add a constant to the right-hand side of both sides of the strict inequality.
Decrement
decrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((c + a) < (c + b)) -> a < b Source #
Subtract a constant from the left-hand side of both sides of
the inequality. This is the opposite of incrementL.
decrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((a + c) < (b + c)) -> a < b Source #
Subtract a constant from the right-hand side of both sides of
the inequality. This is the opposite of incrementR.
Weaken
weakenL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a < b) -> a < (c + b) Source #
Add a constant to the left-hand side of the right-hand side of the strict inequality.
weakenR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a < b) -> a < (b + c) Source #
Add a constant to the right-hand side of the right-hand side of the strict inequality.
Composition
plus :: (a < b) -> (c <= d) -> (a + c) < (b + d) Source #
Add a strict inequality to a nonstrict inequality.
transitive :: (a < b) -> (b < c) -> a < c Source #
Compose two strict inequalities using transitivity.
transitiveNonstrictR :: (a < b) -> (b <= c) -> a < c Source #
Compose a strict inequality (the first argument) with a nonstrict inequality (the second argument).
Multiplication and Division
reciprocalA :: forall (m :: Nat) (n :: Nat) (p :: Nat). (m < Div n p) -> (p * m) < n Source #
Given that m < n/p, we know that p*m < n.
reciprocalB :: forall (m :: Nat) (n :: Nat) (p :: Nat). (m < (Div (n - 1) p + 1)) -> (p * m) < n Source #
Given that m < roundUp(n/p), we know that p*m < n.
Convert to Inequality
Absurdities
Integration with GHC solver
constant :: forall a b. CmpNat a b ~ 'LT => a < b Source #
Use GHC's built-in type-level arithmetic to prove
that one number is less than another. The type-checker
only reduces CmpNat if both arguments are constants.