| Safe Haskell | None |
|---|---|
| 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
| Eq (LEProof n m) Source # |
|
| Ord (LEProof n m) Source # | |
Defined in Data.Type.Nat.LE.ReflStep | |
| Show (LEProof n m) Source # | |
| (SNatI n, SNatI m) => Decidable (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 \)