{-# 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 = LTProof n m
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 = LTProof n m -> (LE ('S n) m => r) -> r
forall (n :: Nat) (m :: Nat) r. LEProof n m -> (LE n m => r) -> r
withLEProof LTProof n m
p r
LE ('S n) m => r
LT n m => r
f
ltReflAbsurd :: LTProof n n -> a
ltReflAbsurd :: forall (n :: Nat) a. LTProof n n -> a
ltReflAbsurd (LESucc LEProof n1 m1
p) = LTProof m1 m1 -> a
forall (n :: Nat) a. LTProof n n -> a
ltReflAbsurd LEProof n1 m1
LTProof m1 m1
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 n1 m1
p) (LESucc LEProof n1 m1
q) = LTProof m1 m1 -> LTProof m1 m1 -> a
forall (n :: Nat) (m :: Nat) a. LTProof n m -> LTProof m n -> a
ltSymAbsurd LEProof n1 m1
LTProof m1 m1
p LEProof n1 m1
LTProof m1 m1
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 n1 m1
q) = LEProof ('S n) m1 -> LEProof ('S n) ('S m1)
forall (n :: Nat) (m :: Nat). LEProof n m -> LEProof n ('S m)
leStep (LEProof ('S n) m1 -> LEProof ('S n) ('S m1))
-> LEProof ('S n) m1 -> LEProof ('S n) ('S m1)
forall a b. (a -> b) -> a -> b
$ LTProof n m -> LEProof m m1 -> LEProof ('S n) m1
forall (n :: Nat) (m :: Nat) (p :: Nat).
LEProof n m -> LEProof m p -> LEProof n p
leTrans LTProof n m
p LEProof m m1
LEProof n1 m1
q