Data.Type.Natural.Class.Order

Documentation

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

Minimal complete definition

(succLeqToLT, cmpZero, leqRefl | leqZero, leqSucc, viewLeq | leqWitness, leqStep), eqlCmpEQ, ltToLeq, eqToRefl, flipCompare, leqToCmp, leqReversed, lneqSuccLeq, lneqReversed, (leqToMin, geqToMin | minLeqL, minLeqR, minLargest), (leqToMax, geqToMax | maxLeqL, maxLeqR, maxLeast)

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 :: nat) 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 :: nat) (m :: nat) 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 :: Ordering). Sing t -> Sing (Apply FlipOrderingSym0 t :: Ordering)

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

coerceLeqR :: forall (n :: nat) 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)

module Data.Singletons.Prelude.Eq

module Data.Singletons.Prelude.Num

module Data.Singletons.Prelude.Ord

type (<) a b = (:<) a b infix 4

type (<@#@$) = (:<$)

type (<@#@$$) = (:<$$)

type (<@#@$$$) a b = (:<$$$) a b

(%<) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<) a b) infix 4

type (>) a b = (:>) a b infix 4

type (>@#@$) = (:>$)

type (>@#@$$) = (:>$$)

type (>@#@$$$) a b = (:>$$$) a b

(%>) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>) a b) infix 4

type (<=) a b = (:<=) a b infix 4

type (<=@#@$) = (:<=$)

type (<=@#@$$) = (:<=$$)

type (<=@#@$$$) a b = (:<=$$$) a b

(%<=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<=) a b) infix 4

type (>=) a b = (:>=) a b infix 4

type (>=@#@$) = (:>=$)

type (>=@#@$$) = (:>=$$)

type (>=@#@$$$) a b = (:>=$$$) a b

(%>=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>=) a b) infix 4

type (/=) a b = (:/=) a b infix 4

type (/=@#@$) = (:/=$)

type (/=@#@$$) = (:/=$$)

type (/=@#@$$$) a b = (:/=$$$) a b

(%/=) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((/=) a b) infix 4

type (==) a b = (:==) a b infix 4

type (==@#@$) = (:==$)

type (==@#@$$) = (:==$$)

type (==@#@$$$) a b = (:==$$$) a b

(%==) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((==) a b) infix 4

type (+) a b = (:+) a b infixl 6

type (+@#@$) = (:+$)

type (+@#@$$) = (:+$$)

type (+@#@$$$) a b = (:+$$$) a b

(%+) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((+) a b) infixl 6

type (-) a b = (:-) a b infixl 6

type (-@#@$) = (:-$)

type (-@#@$$) = (:-$$)

type (-@#@$$$) a b = (:-$$$) a b

(%-) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((-) a b) infixl 6

type * a b = (:*) a b infixl 7

type (*@#@$) = (:*$)

type (*@#@$$) = (:*$$)

type (*@#@$$$) a b = (:*$$$) a b

(%*) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing (* a b) infixl 7