natural-arithmetic-0.1.2.0: Arithmetic of natural numbers

Arithmetic.Lt

Synopsis

# Special Inequalities

zero :: 0 < 1 Source #

Zero is less than one.

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

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

# Composition

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

Add a strict inequality to a nonstrict inequality.

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

Compose two strict inequalities using transitivity.

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

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

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

# Convert to Inequality

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

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

# Absurdities

absurd :: (n < 0) -> void Source #

Nothing is less than zero.

# Integration with GHC solver

constant :: forall a b. CmpNat a b ~ LT => a < b Source #

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.