| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Type.Nat.LE
Description
Less-than-or-equal relation for (unary) natural numbers Nat.
There are at least three ways to encode this relation.
- zero:0≤m and succ:n≤m→1+n≤1+m (this module),
- refl:n≤n and step:n≤m→n≤1+m (Data.Type.Nat.LE.ReflStep),
- ex:∃p.n+p≡m (tricky in Haskell).
Depending on a situation, usage ergonomics are different.
Synopsis
- class LE n m where
- data LEProof n m where
- withLEProof :: LEProof n m -> (LE n m => r) -> r
- decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)
- leZero :: LEProof Z n
- leSucc :: LEProof n m -> LEProof (S n) (S m)
- leRefl :: forall n. SNatI n => LEProof n n
- leStep :: LEProof n m -> LEProof n (S m)
- leAsym :: LEProof n m -> LEProof m n -> n :~: m
- leTrans :: LEProof n m -> LEProof m p -> LEProof n p
- leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof (S m) n
- leSwap' :: LEProof n m -> LEProof (S m) n -> void
- leStepL :: LEProof (S n) m -> LEProof n m
- lePred :: LEProof (S n) (S m) -> LEProof n m
- proofZeroLEZero :: LEProof n Z -> n :~: Z
Relation
Total order of Nat, less-than-or-Equal-to, ≤.
data LEProof n m where Source #
An evidence of n≤m. zero+succ definition.
Instances
| Eq (LEProof n m) Source # |
|
| Ord (LEProof n m) Source # | |
Defined in Data.Type.Nat.LE | |
| Show (LEProof n m) Source # | |
| (SNatI n, SNatI m) => Decidable (LEProof n m) Source # | |
Defined in Data.Type.Nat.LE | |
Decidability
decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m) Source #
Find the LEProof n m
Lemmas
Constructor like
Partial order
Total order
leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof (S m) n Source #
∀nm:N,¬(n≤m)→1+m≤n
leSwap' :: LEProof n m -> LEProof (S m) n -> void Source #
∀nm:N,n≤m→¬(1+m≤n)
>>>leProof :: LEProof Nat2 Nat3LESucc (LESucc LEZero)
>>>leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))LESucc (LESucc (LESucc LEZero))
>>>lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))LESucc (LESucc LEZero)