Modulefin-0.3.2Haskell2010

Data.Type.Nat.LT

classclass LT (n :: Nat) (m :: Nat) where

Less-Than-or. <. Well-founded relation on Nat.

GHC can solve this for us!

Example1 expression

>>> ltProof :: LTProof Nat0 Nat4LESucc LEZero

Example1 expression

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

Example1 expression

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

Instances1LT

typetype LTProof (n :: Nat) (m :: Nat) = LEProof ('S n) m

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

valuewithLTProof :: LTProof n m -> (LT n m => r) -> r

Lemmas

3 declarations

valueltReflAbsurd :: LTProof n n -> a

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

valueltSymAbsurd :: LTProof n m -> LTProof m n -> a

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

valueltTrans :: LTProof n m -> LTProof m p -> LTProof n p

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