{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Nat.LT (
LT (..),
LTProof,
withLTProof,
ltReflAbsurd,
ltSymAbsurd,
ltTrans,
) where
import Data.Type.Nat
import Data.Type.Nat.LE
type LTProof n m = LEProof ('S n) m
class LT (n :: Nat) (m :: Nat) where
ltProof :: LTProof n m
instance LE ('S n) m => LT n m where
ltProof :: LTProof n m
ltProof = forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
leProof
withLTProof :: LTProof n m -> (LT n m => r) -> r
withLTProof :: forall (n :: Nat) (m :: Nat) r. LTProof n m -> (LT n m => r) -> r
withLTProof LTProof n m
p LT n m => r
f = forall (n :: Nat) (m :: Nat) r. LEProof n m -> (LE n m => r) -> r
withLEProof LTProof n m
p LT n m => r
f
ltReflAbsurd :: LTProof n n -> a
ltReflAbsurd :: forall (n :: Nat) a. LTProof n n -> a
ltReflAbsurd (LESucc LEProof n m
p) = forall (n :: Nat) a. LTProof n n -> a
ltReflAbsurd LEProof n m
p
ltSymAbsurd :: LTProof n m -> LTProof m n -> a
ltSymAbsurd :: forall (n :: Nat) (m :: Nat) a. LTProof n m -> LTProof m n -> a
ltSymAbsurd (LESucc LEProof n m
p) (LESucc LEProof n m
q) = forall (n :: Nat) (m :: Nat) a. LTProof n m -> LTProof m n -> a
ltSymAbsurd LEProof n m
p LEProof n m
q
ltTrans :: LTProof n m -> LTProof m p -> LTProof n p
ltTrans :: forall (n :: Nat) (m :: Nat) (p :: Nat).
LTProof n m -> LTProof m p -> LTProof n p
ltTrans LTProof n m
p (LESucc LEProof n m
q) = forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
leStep forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (m :: Nat) (p :: Nat).
LEProof n m -> LEProof m p -> LEProof n p
leTrans LTProof n m
p LEProof n m
q