Zero is less-than-or-equal-to any number.
Modulenatural-arithmetic-0.2.4.0Haskell2010
Arithmetic.Lte
Contents
Synopsis
- value zero
- value reflexive
- value reflexive#
- value substituteL
- value substituteL#
- value substituteR
- 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 transitive
- value transitive#
- value plus
- value plus#
- value fromStrict
- value fromStrict#
- value fromStrictSucc
- value fromStrictSucc#
- value constant
- value lift
- value unlift
- Packagenatural-arithmetic-0.2.4.0
- Exports30
- LanguageHaskell2010
- LicenceBSD-3-Clause
- SourceLte.hs
Special Inequalities
Any number is less-than-or-equal-to itself.
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 inequality.
Add a constant to the right-hand side of both sides of the 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 inequality.
Add a constant to the right-hand side of the right-hand side of the inequality.
Composition
Compose two inequalities using transitivity.
Add two inequalities.
Convert Strict Inequality
Weaken a strict inequality to a non-strict inequality.
Weaken a strict inequality to a non-strict inequality, incrementing the right-hand argument by one.
Integration with GHC solver
Use GHC's built-in type-level arithmetic to prove that one number is less-than-or-equal-to another. The type-checker only reduces CmpNat if both arguments are constants.