natural-arithmetic-0.1.4.0: Arithmetic of natural numbers
Safe HaskellSafe-Inferred
LanguageHaskell2010

Arithmetic.Lte

Synopsis

Special Inequalities

zero :: 0 <= a Source #

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

reflexive :: a <= a Source #

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

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

Composition

transitive :: (a <= b) -> (b <= c) -> a <= c Source #

Compose two inequalities using transitivity.

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

Add two inequalities.

Convert Strict Inequality

fromStrict :: (a < b) -> a <= b Source #

Weaken a strict inequality to a non-strict inequality.

Integration with GHC solver

constant :: forall a b. IsLte (CmpNat a b) ~ 'True => a <= b Source #

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.