Copyright | (C) 2013 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Data.Singletons.Prelude.Ord
Contents
- class (PEq (Proxy :: Proxy a), kproxy ~ Proxy) => POrd kproxy where
- class SEq a => SOrd a where
- thenCmp :: Ordering -> Ordering -> Ordering
- type family ThenCmp (a :: Ordering) (a :: Ordering) :: Ordering where ...
- sThenCmp :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering)
- data family Sing (a :: k)
- data ThenCmpSym0 l
- data ThenCmpSym1 l l
- type ThenCmpSym2 t t = ThenCmp t t
- type LTSym0 = LT
- type EQSym0 = EQ
- type GTSym0 = GT
- data CompareSym0 l
- data CompareSym1 l l
- type CompareSym2 t t = Compare t t
- data (:<$) l
- data l :<$$ l
- type (:<$$$) t t = (:<) t t
- data (:<=$) l
- data l :<=$$ l
- type (:<=$$$) t t = (:<=) t t
- data (:>$) l
- data l :>$$ l
- type (:>$$$) t t = (:>) t t
- data (:>=$) l
- data l :>=$$ l
- type (:>=$$$) t t = (:>=) t t
- data MaxSym0 l
- data MaxSym1 l l
- type MaxSym2 t t = Max t t
- data MinSym0 l
- data MinSym1 l l
- type MinSym2 t t = Min t t
Documentation
class (PEq (Proxy :: Proxy a), kproxy ~ Proxy) => POrd kproxy #
Associated Types
type Compare (arg :: a) (arg :: a) :: Ordering #
type (arg :: a) :< (arg :: a) :: Bool infix 4 #
type (arg :: a) :<= (arg :: a) :: Bool infix 4 #
type (arg :: a) :> (arg :: a) :: Bool infix 4 #
type (arg :: a) :>= (arg :: a) :: Bool infix 4 #
Instances
POrd Bool (Proxy * Bool) # | |
POrd Ordering (Proxy * Ordering) # | |
POrd () (Proxy * ()) # | |
POrd [a0] (Proxy * [a0]) # | |
POrd (Maybe a0) (Proxy * (Maybe a0)) # | |
POrd (NonEmpty a0) (Proxy * (NonEmpty a0)) # | |
POrd (Either a0 b0) (Proxy * (Either a0 b0)) # | |
POrd (a0, b0) (Proxy * (a0, b0)) # | |
POrd (a0, b0, c0) (Proxy * (a0, b0, c0)) # | |
POrd (a0, b0, c0, d0) (Proxy * (a0, b0, c0, d0)) # | |
POrd (a0, b0, c0, d0, e0) (Proxy * (a0, b0, c0, d0, e0)) # | |
POrd (a0, b0, c0, d0, e0, f0) (Proxy * (a0, b0, c0, d0, e0, f0)) # | |
POrd (a0, b0, c0, d0, e0, f0, g0) (Proxy * (a0, b0, c0, d0, e0, f0, g0)) # | |
Methods
sCompare :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) #
(%:<) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:<$) t) t :: Bool) infix 4 #
(%:<=) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:<=$) t) t :: Bool) infix 4 #
(%:>) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:>$) t) t :: Bool) infix 4 #
(%:>=) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:>=$) t) t :: Bool) infix 4 #
sMax :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) #
sMin :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) #
sCompare :: forall t t. (Apply (Apply CompareSym0 t) t ~ Apply (Apply Compare_6989586621679588819Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) #
(%:<) :: forall t t. (Apply (Apply (:<$) t) t ~ Apply (Apply TFHelper_6989586621679588852Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (:<$) t) t :: Bool) infix 4 #
(%:<=) :: forall t t. (Apply (Apply (:<=$) t) t ~ Apply (Apply TFHelper_6989586621679588885Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (:<=$) t) t :: Bool) infix 4 #
(%:>) :: forall t t. (Apply (Apply (:>$) t) t ~ Apply (Apply TFHelper_6989586621679588918Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (:>$) t) t :: Bool) infix 4 #
(%:>=) :: forall t t. (Apply (Apply (:>=$) t) t ~ Apply (Apply TFHelper_6989586621679588951Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (:>=$) t) t :: Bool) infix 4 #
sMax :: forall t t. (Apply (Apply MaxSym0 t) t ~ Apply (Apply Max_6989586621679588984Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) #
sMin :: forall t t. (Apply (Apply MinSym0 t) t ~ Apply (Apply Min_6989586621679589017Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) #
Instances
SOrd Bool # | |
SOrd Ordering # | |
SOrd () # | |
(SOrd a0, SOrd [a0]) => SOrd [a0] # | |
SOrd a0 => SOrd (Maybe a0) # | |
(SOrd a0, SOrd [a0]) => SOrd (NonEmpty a0) # | |
(SOrd a0, SOrd b0) => SOrd (Either a0 b0) # | |
(SOrd a0, SOrd b0) => SOrd (a0, b0) # | |
(SOrd a0, SOrd b0, SOrd c0) => SOrd (a0, b0, c0) # | |
(SOrd a0, SOrd b0, SOrd c0, SOrd d0) => SOrd (a0, b0, c0, d0) # | |
(SOrd a0, SOrd b0, SOrd c0, SOrd d0, SOrd e0) => SOrd (a0, b0, c0, d0, e0) # | |
(SOrd a0, SOrd b0, SOrd c0, SOrd d0, SOrd e0, SOrd f0) => SOrd (a0, b0, c0, d0, e0, f0) # | |
(SOrd a0, SOrd b0, SOrd c0, SOrd d0, SOrd e0, SOrd f0, SOrd g0) => SOrd (a0, b0, c0, d0, e0, f0, g0) # | |
The singleton kind-indexed data family.
Instances
data Sing Bool # | |
data Sing Ordering # | |
data Sing * # | |
data Sing Nat # | |
data Sing Symbol # | |
data Sing () # | |
data Sing [a0] # | |
data Sing (Maybe a0) # | |
data Sing (NonEmpty a0) # | |
data Sing (Either a0 b0) # | |
data Sing (a0, b0) # | |
data Sing ((~>) k1 k2) # | |
data Sing (a0, b0, c0) # | |
data Sing (a0, b0, c0, d0) # | |
data Sing (a0, b0, c0, d0, e0) # | |
data Sing (a0, b0, c0, d0, e0, f0) # | |
data Sing (a0, b0, c0, d0, e0, f0, g0) # | |
Defunctionalization symbols
data ThenCmpSym0 l #
data ThenCmpSym1 l l #
Instances
SuppressUnusedWarnings (Ordering -> TyFun Ordering Ordering -> *) ThenCmpSym1 # | |
type Apply Ordering Ordering (ThenCmpSym1 l1) l0 # | |
type ThenCmpSym2 t t = ThenCmp t t #
data CompareSym0 l #
Instances
SuppressUnusedWarnings (TyFun a6989586621679586420 (TyFun a6989586621679586420 Ordering -> Type) -> *) (CompareSym0 a6989586621679586420) # | |
type Apply a6989586621679586420 (TyFun a6989586621679586420 Ordering -> Type) (CompareSym0 a6989586621679586420) l0 # | |
data CompareSym1 l l #
Instances
SuppressUnusedWarnings (a6989586621679586420 -> TyFun a6989586621679586420 Ordering -> *) (CompareSym1 a6989586621679586420) # | |
type Apply a6989586621679586420 Ordering (CompareSym1 a6989586621679586420 l0) l1 # | |
type CompareSym2 t t = Compare t t #