| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Data.Type.Nat.LE.ReflStep
Synopsis
- data LEProof n m where
- fromZeroSucc :: forall n m. SNatI m => LEProof n m -> LEProof n m
- toZeroSucc :: SNatI n => LEProof n m -> LEProof n m
- decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)
- leZero :: forall n. SNatI n => LEProof 'Z n
- leSucc :: LEProof n m -> LEProof ('S n) ('S m)
- leRefl :: 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
data LEProof n m where Source #
An evidence of \(n \le m\). refl+step definition.
Instances
| Category LEProof Source # | The other variant ( |
| Show (LEProof n m) Source # | |
| (LE m n, n' ~ 'S n, SNatI n) => Absurd (LEProof n' m) Source # | Since: 0.2.1 |
Defined in Data.Type.Nat.LE.ReflStep | |
| (LE n m, SNatI m) => Boring (LEProof n m) Source # | Since: 0.2.1 |
Defined in Data.Type.Nat.LE.ReflStep | |
| (SNatI n, SNatI m) => Decidable (LEProof n m) Source # | |
Defined in Data.Type.Nat.LE.ReflStep | |
| Eq (LEProof n m) Source # | |
| Ord (LEProof n m) Source # | |
Defined in Data.Type.Nat.LE.ReflStep | |
fromZeroSucc :: forall n m. SNatI m => LEProof n m -> LEProof n m Source #
Convert from zero+succ to refl+step definition.
Inverse of toZeroSucc.
toZeroSucc :: SNatI n => LEProof n m -> LEProof n m Source #
Convert refl+step to zero+succ definition.
Inverse of fromZeroSucc.
Decidability
decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m) Source #
Find the LEProof n m
Lemmas
Constructor like
leSucc :: LEProof n m -> LEProof ('S n) ('S m) Source #
\(\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m \)
leStep :: LEProof n m -> LEProof n ('S m) Source #
\(\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m \)
Partial order
leAsym :: LEProof n m -> LEProof m n -> n :~: m Source #
\(\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m \)
leTrans :: LEProof n m -> LEProof m p -> LEProof n p Source #
\(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \)
Total order
leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n Source #
\(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \)
leSwap' :: LEProof n m -> LEProof ('S m) n -> void Source #
\(\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n) \)
More
leStepL :: LEProof ('S n) m -> LEProof n m Source #
\(\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m \)