Data.Type.Natural.Class.Order

Documentation

class (SOrd nat, IsPeano nat) => PeanoOrder nat where

Methods

leqToCmp :: Sing (a :: nat) -> Sing b -> IsTrue (a :<= b) -> Either (a :~: b) (Compare a b :~: LT)

eqlCmpEQ :: Sing (a :: nat) -> Sing b -> (a :~: b) -> Compare a b :~: EQ

eqToRefl :: Sing (a :: nat) -> Sing b -> (Compare a b :~: EQ) -> a :~: b

flipCompare :: Sing (a :: nat) -> Sing b -> FlipOrdering (Compare a b) :~: Compare b a

ltToNeq :: Sing (a :: nat) -> Sing b -> (Compare a b :~: LT) -> (a :~: b) -> Void

leqNeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (a :<= b) -> ((a :~: b) -> Void) -> Compare a b :~: LT

succLeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (S a :<= b) -> Compare a b :~: LT

ltToLeq :: Sing (a :: nat) -> Sing b -> (Compare a b :~: LT) -> IsTrue (a :<= b)

gtToLeq :: Sing (a :: nat) -> Sing b -> (Compare a b :~: GT) -> IsTrue (b :<= a)

ltToSuccLeq :: Sing (a :: nat) -> Sing b -> (Compare a b :~: LT) -> IsTrue (Succ a :<= b)

cmpZero :: Sing a -> Compare (Zero nat) (Succ a) :~: LT

leqToGT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ b :<= a) -> Compare a b :~: GT

cmpZero' :: Sing a -> Either (Compare (Zero nat) a :~: EQ) (Compare (Zero nat) a :~: LT)

zeroNoLT :: Sing a -> (Compare a (Zero nat) :~: LT) -> Void

ltRightPredSucc :: Sing (a :: nat) -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b)

cmpSucc :: Sing (n :: nat) -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)

ltSucc :: Sing (a :: nat) -> Compare a (Succ a) :~: LT

cmpSuccStepR :: Sing (n :: nat) -> Sing m -> (Compare n m :~: LT) -> Compare n (Succ m) :~: LT

ltSuccLToLT :: Sing (n :: nat) -> Sing m -> (Compare (Succ n) m :~: LT) -> Compare n m :~: LT

leqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ a :<= b) -> Compare a b :~: LT

leqZero :: Sing n -> IsTrue (Zero nat :<= n)

leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (Succ n :<= Succ m)

fromLeqView :: LeqView (n :: nat) m -> IsTrue (n :<= m)

leqViewRefl :: Sing (n :: nat) -> LeqView n n

viewLeq :: forall n m. Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> LeqView n m

leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> DiffNat n m

leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> ((n :+ l) :~: m) -> IsTrue (n :<= m)

leqNeqToSuccLeq :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> ((n :~: m) -> Void) -> IsTrue (Succ n :<= m)

leqRefl :: Sing (n :: nat) -> IsTrue (n :<= n)

leqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (n :<= Succ m)

leqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n :<= m) -> IsTrue (n :<= m)

leqReflexive :: Sing (n :: nat) -> Sing m -> (n :~: m) -> IsTrue (n :<= m)

leqTrans :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue (n :<= m) -> IsTrue (m :<= l) -> IsTrue (n :<= l)

leqAntisymm :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> IsTrue (m :<= n) -> n :~: m

plusMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k -> IsTrue (n :<= m) -> IsTrue (l :<= k) -> IsTrue ((n :+ l) :<= (m :+ k))

leqZeroElim :: Sing n -> IsTrue (n :<= Zero nat) -> n :~: Zero nat

plusMonotoneL :: Sing (n :: nat) -> Sing m -> Sing (l :: nat) -> IsTrue (n :<= m) -> IsTrue ((n :+ l) :<= (m :+ l))

plusMonotoneR :: Sing n -> Sing m -> Sing (l :: nat) -> IsTrue (m :<= l) -> IsTrue ((n :+ m) :<= (n :+ l))

plusLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= (n :+ m))

plusLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= (n :+ m))

plusCancelLeqR :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue ((n :+ l) :<= (m :+ l)) -> IsTrue (n :<= m)

plusCancelLeqL :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue ((n :+ m) :<= (n :+ l)) -> IsTrue (m :<= l)

succLeqZeroAbsurd :: Sing n -> IsTrue (S n :<= Zero nat) -> Void

succLeqZeroAbsurd' :: Sing n -> (S n :<= Zero nat) :~: False

succLeqAbsurd :: Sing (n :: nat) -> IsTrue (S n :<= n) -> Void

succLeqAbsurd' :: Sing (n :: nat) -> (S n :<= n) :~: False

notLeqToLeq :: (n :<= m) ~ False => Sing (n :: nat) -> Sing m -> IsTrue (m :<= n)

leqSucc' :: Sing (n :: nat) -> Sing m -> (n :<= m) :~: (Succ n :<= Succ m)

leqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> Min n m :~: n

geqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Min n m :~: m

minComm :: Sing (n :: nat) -> Sing m -> Min n m :~: Min m n

minLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m :<= n)

minLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m :<= m)

minLargest :: Sing (l :: nat) -> Sing n -> Sing m -> IsTrue (l :<= n) -> IsTrue (l :<= m) -> IsTrue (l :<= Min n m)

leqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> Max n m :~: m

geqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Max n m :~: n

maxComm :: Sing (n :: nat) -> Sing m -> Max n m :~: Max m n

maxLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= Max n m)

maxLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= Max n m)

maxLeast :: Sing (l :: nat) -> Sing n -> Sing m -> IsTrue (n :<= l) -> IsTrue (m :<= l) -> IsTrue (Max n m :<= l)

leqReversed :: Sing (n :: nat) -> Sing m -> (n :<= m) :~: (m :>= n)

lneqSuccLeq :: Sing (n :: nat) -> Sing m -> (n :< m) :~: (Succ n :<= m)

lneqReversed :: Sing (n :: nat) -> Sing m -> (n :< m) :~: (m :> n)

lneqToLT :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n :< m) -> Compare n m :~: LT

ltToLneq :: Sing (n :: nat) -> Sing (m :: nat) -> (Compare n m :~: LT) -> IsTrue (n :< m)

lneqZero :: Sing (a :: nat) -> IsTrue (Zero nat :< Succ a)

lneqSucc :: Sing (n :: nat) -> IsTrue (n :< Succ n)

succLneqSucc :: Sing (n :: nat) -> Sing (m :: nat) -> (n :< m) :~: (Succ n :< Succ m)

lneqRightPredSucc :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n :< m) -> m :~: Succ (Pred m)

lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n :< m) -> IsTrue (n :< m)

lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n :< m) -> IsTrue (n :< Succ m)

plusStrictMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k -> IsTrue (n :< m) -> IsTrue (l :< k) -> IsTrue ((n :+ l) :< (m :+ k))

maxZeroL :: Sing n -> Max (Zero nat) n :~: n

maxZeroR :: Sing n -> Max n (Zero nat) :~: n

minZeroL :: Sing n -> Min (Zero nat) n :~: Zero nat

minZeroR :: Sing n -> Min n (Zero nat) :~: Zero nat

minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> (Succ n :- m) :~: Succ (n :- m)

lneqZeroAbsurd :: Sing n -> IsTrue (n :< Zero nat) -> Void

minusPlus :: forall n m. PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> ((n :- m) :+ m) :~: n

data DiffNat n m where

Constructors

DiffNat :: Sing n -> Sing m -> DiffNat n (n :+ m)

data LeqView n m where

Constructors

LeqZero :: Sing n -> LeqView (Zero nat) n

LeqSucc :: Sing n -> Sing m -> IsTrue (n :<= m) -> LeqView (Succ n) (Succ m)

type family FlipOrdering (a :: Ordering) :: Ordering where ...

Equations

FlipOrdering EQ = EQSym0

FlipOrdering LT = GTSym0

FlipOrdering GT = LTSym0

sFlipOrdering :: forall t. Sing t -> Sing (Apply FlipOrderingSym0 t :: Ordering)

coerceLeqL :: forall n m l. IsPeano nat => (n :~: m) -> Sing l -> IsTrue (n :<= l) -> IsTrue (m :<= l)

coerceLeqR :: forall n m l. IsPeano nat => Sing l -> (n :~: m) -> IsTrue (l :<= n) -> IsTrue (l :<= m)

sLeqCongL :: (a :~: b) -> Sing c -> (a :<= c) :~: (b :<= c)

sLeqCongR :: Sing a -> (b :~: c) -> (a :<= b) :~: (a :<= c)

sLeqCong :: (a :~: b) -> (c :~: d) -> (a :<= c) :~: (b :<= d)

type (:-.) n m = Subt n m (m :<= n) infixl 6

Natural subtraction, truncated to zero if m > n.

(%:-.) :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> Sing (n :-. m)

minPlusTruncMinus :: PeanoOrder nat => Sing (n :: nat) -> Sing (m :: nat) -> (Min n m :+ (n :-. m)) :~: n

truncMinusLeq :: PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue ((n :-. m) :<= n)