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

Language | Haskell2010 |

## Synopsis

- zero :: 0 < 1
- 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)
- 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)
- plus :: (a < b) -> (c <= d) -> (a + c) < (b + d)
- transitive :: (a < b) -> (b < c) -> a < c
- transitiveNonstrictL :: (a <= b) -> (b < c) -> a < c
- transitiveNonstrictR :: (a < b) -> (b <= c) -> a < c
- toLteL :: (a < b) -> (1 + a) <= b
- toLteR :: (a < b) -> (a + 1) <= b
- absurd :: (n < 0) -> void
- constant :: forall a b. CmpNat a b ~ LT => 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 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.

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

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