| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Arithmetic.Lte
Synopsis
- zero :: forall (a :: Nat). 0 <= a
- reflexive :: forall (a :: Nat). a <= a
- reflexive# :: forall (a :: Nat). (# #) -> a <=# a
- substituteL :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :=: c) -> (b <= a) -> c <= a
- substituteL# :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :=:# c) -> (b <=# a) -> c <=# a
- substituteR :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :=: c) -> (a <= b) -> a <= c
- substituteR# :: forall (b :: Nat) (c :: Nat) (a :: Nat). (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 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b) -> (b <= c) -> a <= c
- transitive# :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <=# b) -> (b <=# c) -> a <=# c
- plus :: forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat). (a <= b) -> (c <= d) -> (a + c) <= (b + d)
- plus# :: forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat). (a <=# b) -> (c <=# d) -> (a + c) <=# (b + d)
- fromStrict :: forall (a :: Nat) (b :: Nat). (a < b) -> a <= b
- fromStrict# :: forall (a :: Nat) (b :: Nat). (a <# b) -> a <=# b
- fromStrictSucc :: forall (a :: Nat) (b :: Nat). (a < b) -> (a + 1) <= b
- fromStrictSucc# :: forall (a :: Nat) (b :: Nat). (a <# b) -> (a + 1) <=# b
- constant :: forall (a :: Natural) (b :: Natural). IsLte (CmpNat a b) ~ 'True => a <= b
- lift :: forall (a :: Nat) (b :: Nat). (a <=# b) -> a <= b
- unlift :: forall (a :: Nat) (b :: Nat). (a <= b) -> a <=# b
Special Inequalities
reflexive# :: forall (a :: Nat). (# #) -> a <=# a Source #
Substitution
substituteL :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :=: c) -> (b <= a) -> c <= a Source #
Replace the left-hand side of a strict inequality with an equal number.
substituteL# :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :=:# c) -> (b <=# a) -> c <=# a Source #
substituteR :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :=: c) -> (a <= b) -> a <= c Source #
Replace the right-hand side of a strict inequality with an equal number.
substituteR# :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :=:# c) -> (a <=# b) -> a <=# c Source #
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
transitive :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b) -> (b <= c) -> a <= c Source #
Compose two inequalities using transitivity.
plus :: forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat). (a <= b) -> (c <= d) -> (a + c) <= (b + d) Source #
Add two inequalities.
plus# :: forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat). (a <=# b) -> (c <=# d) -> (a + c) <=# (b + d) Source #
Convert Strict Inequality
fromStrict :: forall (a :: Nat) (b :: Nat). (a < b) -> a <= b Source #
Weaken a strict inequality to a non-strict inequality.
fromStrictSucc :: forall (a :: Nat) (b :: Nat). (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 :: Natural) (b :: Natural). 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.