| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Arithmetic.Lte
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.