Zero is less than one.
Modulenatural-arithmetic-0.2.4.0Haskell2010
Arithmetic.Lt
Contents
Synopsis
- value zero
- value zero#
- value substituteL
- value substituteR
- value incrementL
- value incrementL#
- value incrementR
- value incrementR#
- value decrementL
- value decrementL#
- value decrementR
- value decrementR#
- value weakenL
- value weakenL#
- value weakenR
- value weakenR#
- value weakenLhsL#
- value weakenLhsR#
- value plus
- value plus#
- value transitive
- value transitive#
- value transitiveNonstrictL
- value transitiveNonstrictL#
- value transitiveNonstrictR
- value transitiveNonstrictR#
- value reciprocalA
- value reciprocalB
- value toLteL
- value toLteR
- value absurd
- value constant
- value constant#
- value lift
- value unlift
- Packagenatural-arithmetic-0.2.4.0
- Exports35
- LanguageHaskell2010
- LicenceBSD-3-Clause
- SourceLt.hs
Special Inequalities
Substitution
Replace the left-hand side of a strict inequality with an equal number.
Replace the right-hand side of a strict inequality with an equal number.
Increment
Add a constant to the left-hand side of both sides of the strict inequality.
Add a constant to the right-hand side of both sides of the strict inequality.
Decrement
Subtract a constant from the left-hand side of both sides of the inequality. This is the opposite of incrementL.
Subtract a constant from the right-hand side of both sides of the inequality. This is the opposite of incrementR.
Weaken
Add a constant to the left-hand side of the right-hand side of the strict inequality.
Add a constant to the right-hand side of the right-hand side of the strict inequality.
Composition
Add a strict inequality to a nonstrict inequality.
Compose two strict inequalities using transitivity.
Compose a strict inequality (the first argument) with a nonstrict inequality (the second argument).
Multiplication and Division
Given that m < n/p, we know that p*m < n.
Given that m < roundUp(n/p), we know that p*m < n.
Convert to Inequality
Absurdities
Nothing is less than zero.
Integration with GHC solver
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.