HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

Modulenatural-arithmetic-0.2.1.0Haskell2010

Arithmetic.Lte

  • 28 values

Special Inequalities

3 declarations
valuezero :: 0 <= a
#

Zero is less-than-or-equal-to any number.

valuereflexive :: a <= a
#

Any number is less-than-or-equal-to itself.

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 inequality.

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

Add a constant to the right-hand side of both sides of the 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

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

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

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

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

Composition

4 declarations
valuetransitive :: a <= b -> b <= c -> a <= c
#

Compose two inequalities using transitivity.

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

Add two inequalities.

Convert Strict Inequality

4 declarations
valuefromStrict :: a < b -> a <= b
#

Weaken a strict inequality to a non-strict inequality.

valuefromStrictSucc :: a < b -> (a + 1) <= b
#

Weaken a strict inequality to a non-strict inequality, incrementing the right-hand argument by one.

Integration with GHC solver

1 declaration
valueconstant :: IsLte (CmpNat a b) ~ 'True => a <= b
#

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.

Lift and Unlift

2 declarations