| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Type.Nat.LT
Contents
Documentation
class LT (n :: Nat ) (m :: Nat ) where Source #
Less-Than-or.
\(<\)
. Well-founded relation on
Nat
.
GHC can solve this for us!
>>>ltProof :: LTProof Nat0 Nat4LESucc LEZero
>>>ltProof :: LTProof Nat2 Nat4LESucc (LESucc (LESucc LEZero))
>>>ltProof :: LTProof Nat3 Nat3... ...error... ...
type LTProof n m = LEProof (' S n) m Source #
An evidence \(n < m\) which is the same as (1 + n le m).
withLTProof :: LTProof n m -> ( LT n m => r) -> r Source #
Lemmas
ltReflAbsurd :: LTProof n n -> a Source #
\(\forall n : \mathbb{N}, n < n \to \bot \)
ltSymAbsurd :: LTProof n m -> LTProof m n -> a Source #
\(\forall n\, m : \mathbb{N}, n < m \to m < n \to \bot \)