| 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 Methods compare :: LEProof n m -> LEProof n m -> Ordering Source # (<) :: LEProof n m -> LEProof n m -> Bool Source # (<=) :: LEProof n m -> LEProof n m -> Bool Source # (>) :: LEProof n m -> LEProof n m -> Bool Source # (>=) :: LEProof n m -> LEProof n m -> Bool Source # |
|
| Show ( LEProof n m) Source # | |
| ( SNatI n, SNatI m) => Decidable ( LEProof n m) Source # | |
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
, i.e. compare numbers.
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 \)