Safe Haskell	Safe
Language	Haskell2010

Data.Type.Nat.LT

Contents

Synopsis

class LT (n :: Nat) (m :: Nat) where
- ltProof :: LTProof n m
type LTProof (n :: Nat) (m :: Nat) = LEProof ('S n) m
withLTProof :: forall (n :: Nat) (m :: Nat) r. LTProof n m -> (LT n m => r) -> r
ltReflAbsurd :: forall (n :: Nat) a. LTProof n n -> a
ltSymAbsurd :: forall (n :: Nat) (m :: Nat) a. LTProof n m -> LTProof m n -> a
ltTrans :: forall (n :: Nat) (m :: Nat) (p :: Nat). LTProof n m -> LTProof m p -> LTProof n p

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 Nat4
LESucc LEZero

>>> ltProof :: LTProof Nat2 Nat4
LESucc (LESucc (LESucc LEZero))

>>> ltProof :: LTProof Nat3 Nat3
...
...error...
...

Methods

Instances details

LE ('S n) m => LT n m Source #
Instance details Defined in Data.Type.Nat.LT Methods ltProof :: LTProof n m Source #

type LTProof (n :: Nat) (m :: Nat) = LEProof ('S n) m Source #

An evidence \(n < m\) which is the same as (1 + n le m).

withLTProof :: forall (n :: Nat) (m :: Nat) r. LTProof n m -> (LT n m => r) -> r Source #

Lemmas

ltReflAbsurd :: forall (n :: Nat) a. LTProof n n -> a Source #

\(\forall n : \mathbb{N}, n < n \to \bot \)

ltSymAbsurd :: forall (n :: Nat) (m :: Nat) a. LTProof n m -> LTProof m n -> a Source #

\(\forall n\, m : \mathbb{N}, n < m \to m < n \to \bot \)

ltTrans :: forall (n :: Nat) (m :: Nat) (p :: Nat). LTProof n m -> LTProof m p -> LTProof n p Source #

\(\forall n\, m\, p : \mathbb{N}, n < m \to m < p \to n < p \)