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

Instances

PeanoOrder Nat

Defined in Data.Type.Natural.Builtin

Methods

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

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

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

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

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

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

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

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

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

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

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

leqToGT :: Sing a -> 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 -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b)

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

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

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

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

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

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

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

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

leqViewRefl :: Sing n -> LeqView n n

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

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

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

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

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

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

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

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

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

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

plusMonotone :: Sing n -> 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 -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue ((n + l) <= (m + l))

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

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

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

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

plusCancelLeqL :: Sing n -> 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 -> IsTrue (S n <= n) -> Void

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

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

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

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

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

minComm :: Sing n -> Sing m -> Min n m :~: Min m n

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

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

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

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

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

maxComm :: Sing n -> Sing m -> Max n m :~: Max m n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

plusStrictMonotone :: Sing n -> 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 -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)

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

minusPlus :: PeanoOrder Nat => Sing n -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n

PeanoOrder Nat

Defined in Data.Type.Natural

Methods

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

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

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

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

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

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

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

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

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

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

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

leqToGT :: Sing a -> 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 -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b)

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

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

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

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

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

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

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

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

leqViewRefl :: Sing n -> LeqView n n

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

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

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

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

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

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

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

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

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

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

plusMonotone :: Sing n -> 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 -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue ((n + l) <= (m + l))

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

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

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

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

plusCancelLeqL :: Sing n -> 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 -> IsTrue (S n <= n) -> Void

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

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

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

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

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

minComm :: Sing n -> Sing m -> Min n m :~: Min m n

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

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

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

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

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

maxComm :: Sing n -> Sing m -> Max n m :~: Max m n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

plusStrictMonotone :: Sing n -> 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 -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)

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

minusPlus :: PeanoOrder Nat => Sing n -> 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)

data family Sing (a :: k) :: *

The singleton kind-indexed data family.

Instances

Eq (Sing n)

Defined in Data.Type.Natural.Core

Methods

(==) :: Sing n -> Sing n -> Bool

(/=) :: Sing n -> Sing n -> Bool

ShowSing Nat => Show (Sing z)

Defined in Data.Type.Natural.Definitions

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

data Sing (z :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Bool) where

• SFalse :: Sing False
• STrue :: Sing True

data Sing (z :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Ordering) where

• SLT :: Sing LT
• SEQ :: Sing EQ
• SGT :: Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: Sing n

data Sing (z :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: ()) where

• STuple0 :: Sing ()

data Sing (z :: Nat)

Defined in Data.Type.Natural.Definitions

data Sing (z :: Nat) where

• SZ :: Sing Z
• SS :: Sing (S n)

data Sing (z :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Void)

data Sing (z :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: [a]) where

• SNil :: Sing ([] :: [a])
• SCons :: Sing (n1 ': n2)

data Sing (z :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Maybe a) where

• SNothing :: Sing (Nothing :: Maybe a)
• SJust :: Sing (Just n)

data Sing (z :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: NonEmpty a) where

• (:%|) :: Sing (n1 :| n2)

data Sing (z :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Either a b) where

• SLeft :: Sing (Left n :: Either a b)
• SRight :: Sing (Right n :: Either a b)

data Sing (z :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b)) where

• STuple2 :: Sing ((,) n1 n2)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (z :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c)) where

• STuple3 :: Sing ((,,) n1 n2 n3)

data Sing (z :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d)) where

• STuple4 :: Sing ((,,,) n1 n2 n3 n4)

data Sing (z :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e)) where

• STuple5 :: Sing ((,,,,) n1 n2 n3 n4 n5)

data Sing (z :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e, f)) where

• STuple6 :: Sing ((,,,,,) n1 n2 n3 n4 n5 n6)

data Sing (z :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e, f, g)) where

• STuple7 :: Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

type CompareSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Compare t t1

data CompareSym1 (l :: a6989586621679299162) (l1 :: TyFun a6989586621679299162 Ordering) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 Ordering -> *

Instances

SuppressUnusedWarnings (CompareSym1 :: a6989586621679299162 -> TyFun a6989586621679299162 Ordering -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym1 l1 :: TyFun a Ordering -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym1 l1 :: TyFun a Ordering -> *) (l2 :: a) = Compare l1 l2

data CompareSym0 (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Ordering -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 Ordering -> Type) -> *

Instances

SuppressUnusedWarnings (CompareSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Ordering -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Ordering -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Ordering -> Type) -> *) (l :: a6989586621679299162) = CompareSym1 l

type (<@#@$$$) (t :: a6989586621679299162) (t1 :: a6989586621679299162) = t < t1

data (l :: a6989586621679299162) <@#@$$ (l1 :: TyFun a6989586621679299162 Bool) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 Bool -> *

Instances

SuppressUnusedWarnings ((<@#@$$) :: a6989586621679299162 -> TyFun a6989586621679299162 Bool -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((<@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 < l2

data (<@#@$) (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *

Instances

SuppressUnusedWarnings ((<@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply ((<@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *) (l :: a6989586621679299162) = (<@#@$$) l

type (<=@#@$$$) (t :: a6989586621679299162) (t1 :: a6989586621679299162) = t <= t1

data (l :: a6989586621679299162) <=@#@$$ (l1 :: TyFun a6989586621679299162 Bool) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 Bool -> *

Instances

SuppressUnusedWarnings ((<=@#@$$) :: a6989586621679299162 -> TyFun a6989586621679299162 Bool -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((<=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 <= l2

data (<=@#@$) (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *

Instances

SuppressUnusedWarnings ((<=@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<=@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply ((<=@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *) (l :: a6989586621679299162) = (<=@#@$$) l

type (>@#@$$$) (t :: a6989586621679299162) (t1 :: a6989586621679299162) = t > t1

data (l :: a6989586621679299162) >@#@$$ (l1 :: TyFun a6989586621679299162 Bool) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 Bool -> *

Instances

SuppressUnusedWarnings ((>@#@$$) :: a6989586621679299162 -> TyFun a6989586621679299162 Bool -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 > l2

data (>@#@$) (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *

Instances

SuppressUnusedWarnings ((>@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *) (l :: a6989586621679299162) = (>@#@$$) l

type (>=@#@$$$) (t :: a6989586621679299162) (t1 :: a6989586621679299162) = t >= t1

data (l :: a6989586621679299162) >=@#@$$ (l1 :: TyFun a6989586621679299162 Bool) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 Bool -> *

Instances

SuppressUnusedWarnings ((>=@#@$$) :: a6989586621679299162 -> TyFun a6989586621679299162 Bool -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 >= l2

data (>=@#@$) (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *

Instances

SuppressUnusedWarnings ((>=@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$) :: TyFun a6989586621679299162 (TyFun a6989586621679299162 Bool -> Type) -> *) (l :: a6989586621679299162) = (>=@#@$$) l

type MaxSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Max t t1

data MaxSym1 (l :: a6989586621679299162) (l1 :: TyFun a6989586621679299162 a6989586621679299162) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *

Instances

SuppressUnusedWarnings (MaxSym1 :: a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a) = Max l1 l2

data MaxSym0 (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *

Instances

SuppressUnusedWarnings (MaxSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *) (l :: a6989586621679299162) = MaxSym1 l

type MinSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Min t t1

data MinSym1 (l :: a6989586621679299162) (l1 :: TyFun a6989586621679299162 a6989586621679299162) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *

Instances

SuppressUnusedWarnings (MinSym1 :: a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a) = Min l1 l2

data MinSym0 (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *

Instances

SuppressUnusedWarnings (MinSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *) (l :: a6989586621679299162) = MinSym1 l

class PEq a => POrd a

Associated Types

type Compare (arg :: a) (arg1 :: a) :: Ordering

type (arg :: a) < (arg1 :: a) :: Bool

type (arg :: a) <= (arg1 :: a) :: Bool

type (arg :: a) > (arg1 :: a) :: Bool

type (arg :: a) >= (arg1 :: a) :: Bool

type Max (arg :: a) (arg1 :: a) :: a

type Min (arg :: a) (arg1 :: a) :: a

Instances

POrd Bool

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Ordering

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd ()

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Nat

Defined in Data.Type.Natural.Definitions

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Void

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd [a]

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Maybe a)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (NonEmpty a)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Either a b)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b, c)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b, c, d)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b, c, d, e)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b, c, d, e, f)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b, c, d, e, f, g)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

class SEq a => SOrd a where

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun a (TyFun a Ordering -> Type) -> *) t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<@#@$) :: TyFun a (TyFun a Bool -> Type) -> *) t1) t2) infix 4

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<=@#@$) :: TyFun a (TyFun a Bool -> Type) -> *) t1) t2) infix 4

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((>@#@$) :: TyFun a (TyFun a Bool -> Type) -> *) t1) t2) infix 4

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((>=@#@$) :: TyFun a (TyFun a Bool -> Type) -> *) t1) t2) infix 4

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (MaxSym0 :: TyFun a (TyFun a a -> Type) -> *) t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (MinSym0 :: TyFun a (TyFun a a -> Type) -> *) t1) t2)

Instances

SOrd Bool

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SOrd Ordering

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SOrd ()

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SOrd Nat

Defined in Data.Type.Natural.Definitions

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SOrd Void

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd [a]) => SOrd [a]

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SOrd a => SOrd (Maybe a)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd [a]) => SOrd (NonEmpty a)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd b) => SOrd (Either a b)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd b) => SOrd (a, b)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g)

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

type LTSym0 = LT

type EQSym0 = EQ

type GTSym0 = GT