| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Arithmetic.Lte
Synopsis
- zero :: 0 <= a
- reflexive :: a <= 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)
- 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)
- 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
- 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
- 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)
- 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)
- weakenR# :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <=# b) -> a <=# (b + c)
- transitive :: (a <= b) -> (b <= c) -> a <= c
- transitive# :: (a <=# b) -> (b <=# c) -> a <=# c
- plus :: (a <= b) -> (c <= d) -> (a + c) <= (b + d)
- plus# :: (a <=# b) -> (c <=# d) -> (a + c) <=# (b + d)
- fromStrict :: (a < b) -> a <= b
- fromStrict# :: (a <# b) -> a <=# b
- fromStrictSucc :: (a < b) -> (a + 1) <= b
- fromStrictSucc# :: (a <# b) -> (a + 1) <=# b
- constant :: forall a b. IsLte (CmpNat a b) ~ 'True => a <= b
- lift :: (a <=# b) -> a <= b
- unlift :: (a <= b) -> a <=# b
Special Inequalities
reflexive# :: (# #) -> a <=# a Source #
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.
fromStrict# :: (a <# b) -> a <=# b Source #
fromStrictSucc :: (a < b) -> (a + 1) <= b Source #
Weaken a strict inequality to a non-strict inequality, incrementing the right-hand argument by one.
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.