HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

Modulenatural-arithmetic-0.2.1.0Haskell2010

Arithmetic.Lt

  • 35 values

Special Inequalities

2 declarations
valuezero :: 0 < 1
#

Zero is less than one.

Substitution

2 declarations
valuesubstituteL :: b :=: c -> b < a -> c < a
#

Replace the left-hand side of a strict inequality with an equal number.

valuesubstituteR :: b :=: c -> a < b -> a < c
#

Replace the right-hand side of a strict inequality with an equal number.

Increment

4 declarations
valueincrementL :: a < b -> (c + a) < (c + b)
#

Add a constant to the left-hand side of both sides of the strict inequality.

valueincrementR :: a < b -> (a + c) < (b + c)
#

Add a constant to the right-hand side of both sides of the strict inequality.

Decrement

4 declarations
valuedecrementL :: (c + a) < (c + b) -> a < b
#

Subtract a constant from the left-hand side of both sides of the inequality. This is the opposite of incrementL.

valuedecrementR :: (a + c) < (b + c) -> a < b
#

Subtract a constant from the right-hand side of both sides of the inequality. This is the opposite of incrementR.

Weaken

6 declarations
valueweakenL :: a < b -> a < (c + b)
#

Add a constant to the left-hand side of the right-hand side of the strict inequality.

valueweakenR :: a < b -> a < (b + c)
#

Add a constant to the right-hand side of the right-hand side of the strict inequality.

Composition

8 declarations
valueplus :: a < b -> c <= d -> (a + c) < (b + d)
#

Add a strict inequality to a nonstrict inequality.

valuetransitive :: a < b -> b < c -> a < c
#

Compose two strict inequalities using transitivity.

valuetransitiveNonstrictR :: a < b -> b <= c -> a < c
#

Compose a strict inequality (the first argument) with a nonstrict inequality (the second argument).

Multiplication and Division

2 declarations
valuereciprocalA :: m < Div n p -> (p * m) < n
#

Given that m < n/p, we know that p*m < n.

valuereciprocalB :: m < (Div (n - 1) p + 1) -> (p * m) < n
#

Given that m < roundUp(n/p), we know that p*m < n.

Convert to Inequality

2 declarations

Absurdities

1 declaration
valueabsurd :: n < 0 -> void
#

Nothing is less than zero.

Integration with GHC solver

2 declarations
valueconstant :: CmpNat a b ~ 'LT => a < b
#

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.

Lift and Unlift

2 declarations