Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- zero :: 0 <= a
- reflexive :: a <= a
- substituteL :: (b :=: c) -> (b <= a) -> c <= a
- substituteR :: (b :=: c) -> (a <= b) -> a <= c
- incrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> (c + a) <= (c + b)
- incrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> (a + c) <= (b + c)
- decrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((c + a) <= (c + b)) -> a <= b
- decrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat). ((a + c) <= (b + c)) -> a <= b
- weakenL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> a <= (c + b)
- weakenR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> a <= (b + c)
- transitive :: (a <= b) -> (b <= c) -> a <= c
- plus :: (a <= b) -> (c <= d) -> (a + c) <= (b + d)
- fromStrict :: (a < b) -> a <= b
- constant :: forall a b. IsLte (CmpNat a b) ~ True => a <= b

# Special Inequalities

# 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

# Convert Strict Inequality

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

Weaken a strict inequality to a non-strict inequality.