Copyright | (C) 2013 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Data.Singletons.Prelude.Ord
Synopsis
- class POrd (a :: Type) where
- class SEq a => SOrd a where
- sCompare :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering)
- (%<) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t :: Bool)
- (%<=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool)
- (%>) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool)
- (%>=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool)
- sMax :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a)
- sMin :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a)
- type family Comparing (a :: (~>) b a) (a :: b) (a :: b) :: Ordering where ...
- sComparing :: forall b a (t :: (~>) b a) (t :: b) (t :: b). SOrd a => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ComparingSym0 t) t) t :: Ordering)
- thenCmp :: Ordering -> Ordering -> Ordering
- type family ThenCmp (a :: Ordering) (a :: Ordering) :: Ordering where ...
- sThenCmp :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering)
- type family Sing :: k -> Type
- data SOrdering :: Ordering -> Type where
- data SDown :: forall a. Down a -> Type where
- data ThenCmpSym0 :: (~>) Ordering ((~>) Ordering Ordering)
- data ThenCmpSym1 (a6989586621679400187 :: Ordering) :: (~>) Ordering Ordering
- type ThenCmpSym2 (a6989586621679400187 :: Ordering) (a6989586621679400188 :: Ordering) = ThenCmp a6989586621679400187 a6989586621679400188
- type LTSym0 = 'LT
- type EQSym0 = 'EQ
- type GTSym0 = 'GT
- data CompareSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Ordering)
- data CompareSym1 (arg6989586621679389843 :: a6989586621679389754) :: (~>) a6989586621679389754 Ordering
- type CompareSym2 (arg6989586621679389843 :: a6989586621679389754) (arg6989586621679389844 :: a6989586621679389754) = Compare arg6989586621679389843 arg6989586621679389844
- data (<@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool)
- data (<@#@$$) (arg6989586621679389847 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool
- type (<@#@$$$) (arg6989586621679389847 :: a6989586621679389754) (arg6989586621679389848 :: a6989586621679389754) = (<) arg6989586621679389847 arg6989586621679389848
- data (<=@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool)
- data (<=@#@$$) (arg6989586621679389851 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool
- type (<=@#@$$$) (arg6989586621679389851 :: a6989586621679389754) (arg6989586621679389852 :: a6989586621679389754) = (<=) arg6989586621679389851 arg6989586621679389852
- data (>@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool)
- data (>@#@$$) (arg6989586621679389855 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool
- type (>@#@$$$) (arg6989586621679389855 :: a6989586621679389754) (arg6989586621679389856 :: a6989586621679389754) = (>) arg6989586621679389855 arg6989586621679389856
- data (>=@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool)
- data (>=@#@$$) (arg6989586621679389859 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool
- type (>=@#@$$$) (arg6989586621679389859 :: a6989586621679389754) (arg6989586621679389860 :: a6989586621679389754) = (>=) arg6989586621679389859 arg6989586621679389860
- data MaxSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 a6989586621679389754)
- data MaxSym1 (arg6989586621679389863 :: a6989586621679389754) :: (~>) a6989586621679389754 a6989586621679389754
- type MaxSym2 (arg6989586621679389863 :: a6989586621679389754) (arg6989586621679389864 :: a6989586621679389754) = Max arg6989586621679389863 arg6989586621679389864
- data MinSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 a6989586621679389754)
- data MinSym1 (arg6989586621679389867 :: a6989586621679389754) :: (~>) a6989586621679389754 a6989586621679389754
- type MinSym2 (arg6989586621679389867 :: a6989586621679389754) (arg6989586621679389868 :: a6989586621679389754) = Min arg6989586621679389867 arg6989586621679389868
- data ComparingSym0 :: forall b6989586621679389744 a6989586621679389743. (~>) ((~>) b6989586621679389744 a6989586621679389743) ((~>) b6989586621679389744 ((~>) b6989586621679389744 Ordering))
- data ComparingSym1 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) :: (~>) b6989586621679389744 ((~>) b6989586621679389744 Ordering)
- data ComparingSym2 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) (a6989586621679389835 :: b6989586621679389744) :: (~>) b6989586621679389744 Ordering
- type ComparingSym3 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) (a6989586621679389835 :: b6989586621679389744) (a6989586621679389836 :: b6989586621679389744) = Comparing a6989586621679389834 a6989586621679389835 a6989586621679389836
- data DownSym0 :: forall (a6989586621679089884 :: Type). (~>) a6989586621679089884 (Down (a6989586621679089884 :: Type))
- type DownSym1 (t6989586621679398850 :: a6989586621679089884) = 'Down t6989586621679398850
Documentation
class POrd (a :: Type) Source #
Associated Types
type Compare (arg :: a) (arg :: a) :: Ordering Source #
type (arg :: a) < (arg :: a) :: Bool infix 4 Source #
type (arg :: a) <= (arg :: a) :: Bool infix 4 Source #
type (arg :: a) > (arg :: a) :: Bool infix 4 Source #
type (arg :: a) >= (arg :: a) :: Bool infix 4 Source #
Instances
POrd Bool Source # | |
POrd Ordering Source # | |
POrd Nat Source # | |
POrd Symbol Source # | |
POrd () Source # | |
POrd Void Source # | |
POrd All Source # | |
POrd Any Source # | |
POrd [a] Source # | |
POrd (Maybe a) Source # | |
POrd (NonEmpty a) Source # | |
POrd (Down a) Source # | |
POrd (Identity a) Source # | |
POrd (First a) Source # | |
POrd (Last a) Source # | |
POrd (Max a) Source # | |
POrd (Min a) Source # | |
POrd (Option a) Source # | |
POrd (WrappedMonoid m) Source # | |
POrd (Dual a) Source # | |
POrd (Product a) Source # | |
POrd (Sum a) Source # | |
POrd (First a) Source # | |
POrd (Last a) Source # | |
POrd (Either a b) Source # | |
POrd (a, b) Source # | |
POrd (Arg a b) Source # | |
POrd (a, b, c) Source # | |
POrd (Const a b) Source # | |
POrd (a, b, c, d) Source # | |
POrd (a, b, c, d, e) Source # | |
POrd (a, b, c, d, e, f) Source # | |
POrd (a, b, c, d, e, f, g) Source # | |
class SEq a => SOrd a where Source #
Minimal complete definition
Nothing
Methods
sCompare :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) Source #
default sCompare :: forall (t :: a) (t :: a). (Apply (Apply CompareSym0 t) t :: Ordering) ~ Apply (Apply Compare_6989586621679389873Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) Source #
(%<) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t :: Bool) infix 4 Source #
default (%<) :: forall (t :: a) (t :: a). (Apply (Apply (<@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679389897Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t :: Bool) Source #
(%<=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool) infix 4 Source #
default (%<=) :: forall (t :: a) (t :: a). (Apply (Apply (<=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679389915Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool) Source #
(%>) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool) infix 4 Source #
default (%>) :: forall (t :: a) (t :: a). (Apply (Apply (>@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679389933Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool) Source #
(%>=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool) infix 4 Source #
default (%>=) :: forall (t :: a) (t :: a). (Apply (Apply (>=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679389951Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool) Source #
sMax :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) Source #
default sMax :: forall (t :: a) (t :: a). (Apply (Apply MaxSym0 t) t :: a) ~ Apply (Apply Max_6989586621679389969Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) Source #
sMin :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) Source #
Instances
SOrd Bool Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd Ordering Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd Nat Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd Symbol Source # | |
Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd () Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd Void Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd Bool => SOrd All Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd Bool => SOrd Any Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd [a]) => SOrd [a] Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Maybe a) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd [a]) => SOrd (NonEmpty a) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Down a) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Identity a) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (First a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Last a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Max a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Min a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd (Maybe a) => SOrd (Option a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: Option a) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Option a) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Option a) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Option a) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Option a) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Option a) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Option a) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd m => SOrd (WrappedMonoid m) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Dual a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Product a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Sum a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd (Maybe a) => SOrd (First a) Source # | |
Defined in Data.Singletons.Prelude.Monoid Methods sCompare :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd (Maybe a) => SOrd (Last a) Source # | |
Defined in Data.Singletons.Prelude.Monoid Methods sCompare :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd b) => SOrd (Either a b) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd b) => SOrd (a, b) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Arg a b) Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sCompare :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
SOrd a => SOrd (Const a b) Source # | |
Defined in Data.Singletons.Prelude.Const Methods sCompare :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # | |
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sCompare :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # |
sComparing :: forall b a (t :: (~>) b a) (t :: b) (t :: b). SOrd a => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ComparingSym0 t) t) t :: Ordering) Source #
thenCmp
returns its second argument if its first is EQ
; otherwise,
it returns its first argument.
sThenCmp :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering) Source #
type family Sing :: k -> Type Source #
The singleton kind-indexed type family.
Instances
data SOrdering :: Ordering -> Type where Source #
Instances
TestCoercion SOrdering Source # | |
Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (Coercion a b) | |
TestEquality SOrdering Source # | |
Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (a :~: b) | |
Show (SOrdering z) | |
data SDown :: forall a. Down a -> Type where Source #
Instances
SDecide a => TestCoercion (SDown :: Down a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods testCoercion :: forall (a0 :: k) (b :: k). SDown a0 -> SDown b -> Maybe (Coercion a0 b) | |
SDecide a => TestEquality (SDown :: Down a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods testEquality :: forall (a0 :: k) (b :: k). SDown a0 -> SDown b -> Maybe (a0 :~: b) |
Defunctionalization symbols
data ThenCmpSym0 :: (~>) Ordering ((~>) Ordering Ordering) Source #
Instances
SingI ThenCmpSym0 Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ThenCmpSym0 Source # | |
SuppressUnusedWarnings ThenCmpSym0 Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ThenCmpSym0 (a6989586621679400187 :: Ordering) Source # | |
Defined in Data.Singletons.Prelude.Ord |
data ThenCmpSym1 (a6989586621679400187 :: Ordering) :: (~>) Ordering Ordering Source #
Instances
SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ThenCmpSym1 d) Source # | |
SuppressUnusedWarnings (ThenCmpSym1 a6989586621679400187 :: TyFun Ordering Ordering -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (ThenCmpSym1 a6989586621679400187 :: TyFun Ordering Ordering -> Type) (a6989586621679400188 :: Ordering) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (ThenCmpSym1 a6989586621679400187 :: TyFun Ordering Ordering -> Type) (a6989586621679400188 :: Ordering) = ThenCmp a6989586621679400187 a6989586621679400188 |
type ThenCmpSym2 (a6989586621679400187 :: Ordering) (a6989586621679400188 :: Ordering) = ThenCmp a6989586621679400187 a6989586621679400188 Source #
data CompareSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Ordering) Source #
Instances
SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing CompareSym0 Source # | |
SuppressUnusedWarnings (CompareSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> Ordering) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (CompareSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> Ordering) -> Type) (arg6989586621679389843 :: a6989586621679389754) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> Ordering) -> Type) (arg6989586621679389843 :: a6989586621679389754) = CompareSym1 arg6989586621679389843 |
data CompareSym1 (arg6989586621679389843 :: a6989586621679389754) :: (~>) a6989586621679389754 Ordering Source #
Instances
(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (CompareSym1 d) Source # | |
SuppressUnusedWarnings (CompareSym1 arg6989586621679389843 :: TyFun a6989586621679389754 Ordering -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (CompareSym1 arg6989586621679389843 :: TyFun a Ordering -> Type) (arg6989586621679389844 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym1 arg6989586621679389843 :: TyFun a Ordering -> Type) (arg6989586621679389844 :: a) = Compare arg6989586621679389843 arg6989586621679389844 |
type CompareSym2 (arg6989586621679389843 :: a6989586621679389754) (arg6989586621679389844 :: a6989586621679389754) = Compare arg6989586621679389843 arg6989586621679389844 Source #
data (<@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool) infix 4 Source #
Instances
SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
SuppressUnusedWarnings ((<@#@$) :: TyFun a6989586621679389754 (a6989586621679389754 ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ((<@#@$) :: TyFun a6989586621679389754 (a6989586621679389754 ~> Bool) -> Type) (arg6989586621679389847 :: a6989586621679389754) Source # | |
data (<@#@$$) (arg6989586621679389847 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool infix 4 Source #
Instances
(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type) Source # | |
SuppressUnusedWarnings ((<@#@$$) arg6989586621679389847 :: TyFun a6989586621679389754 Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ((<@#@$$) arg6989586621679389847 :: TyFun a Bool -> Type) (arg6989586621679389848 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord |
type (<@#@$$$) (arg6989586621679389847 :: a6989586621679389754) (arg6989586621679389848 :: a6989586621679389754) = (<) arg6989586621679389847 arg6989586621679389848 Source #
data (<=@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool) infix 4 Source #
Instances
SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
SuppressUnusedWarnings ((<=@#@$) :: TyFun a6989586621679389754 (a6989586621679389754 ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ((<=@#@$) :: TyFun a6989586621679389754 (a6989586621679389754 ~> Bool) -> Type) (arg6989586621679389851 :: a6989586621679389754) Source # | |
data (<=@#@$$) (arg6989586621679389851 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool infix 4 Source #
Instances
(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type) Source # | |
SuppressUnusedWarnings ((<=@#@$$) arg6989586621679389851 :: TyFun a6989586621679389754 Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ((<=@#@$$) arg6989586621679389851 :: TyFun a Bool -> Type) (arg6989586621679389852 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord |
type (<=@#@$$$) (arg6989586621679389851 :: a6989586621679389754) (arg6989586621679389852 :: a6989586621679389754) = (<=) arg6989586621679389851 arg6989586621679389852 Source #
data (>@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool) infix 4 Source #
Instances
SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
SuppressUnusedWarnings ((>@#@$) :: TyFun a6989586621679389754 (a6989586621679389754 ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ((>@#@$) :: TyFun a6989586621679389754 (a6989586621679389754 ~> Bool) -> Type) (arg6989586621679389855 :: a6989586621679389754) Source # | |
data (>@#@$$) (arg6989586621679389855 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool infix 4 Source #
Instances
(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type) Source # | |
SuppressUnusedWarnings ((>@#@$$) arg6989586621679389855 :: TyFun a6989586621679389754 Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ((>@#@$$) arg6989586621679389855 :: TyFun a Bool -> Type) (arg6989586621679389856 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord |
type (>@#@$$$) (arg6989586621679389855 :: a6989586621679389754) (arg6989586621679389856 :: a6989586621679389754) = (>) arg6989586621679389855 arg6989586621679389856 Source #
data (>=@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool) infix 4 Source #
Instances
SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
SuppressUnusedWarnings ((>=@#@$) :: TyFun a6989586621679389754 (a6989586621679389754 ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ((>=@#@$) :: TyFun a6989586621679389754 (a6989586621679389754 ~> Bool) -> Type) (arg6989586621679389859 :: a6989586621679389754) Source # | |
data (>=@#@$$) (arg6989586621679389859 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool infix 4 Source #
Instances
(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type) Source # | |
SuppressUnusedWarnings ((>=@#@$$) arg6989586621679389859 :: TyFun a6989586621679389754 Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply ((>=@#@$$) arg6989586621679389859 :: TyFun a Bool -> Type) (arg6989586621679389860 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord |
type (>=@#@$$$) (arg6989586621679389859 :: a6989586621679389754) (arg6989586621679389860 :: a6989586621679389754) = (>=) arg6989586621679389859 arg6989586621679389860 Source #
data MaxSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 a6989586621679389754) Source #
Instances
SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type) Source # | |
SuppressUnusedWarnings (MaxSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (MaxSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) (arg6989586621679389863 :: a6989586621679389754) Source # | |
data MaxSym1 (arg6989586621679389863 :: a6989586621679389754) :: (~>) a6989586621679389754 a6989586621679389754 Source #
Instances
(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings (MaxSym1 arg6989586621679389863 :: TyFun a6989586621679389754 a6989586621679389754 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (MaxSym1 arg6989586621679389863 :: TyFun a a -> Type) (arg6989586621679389864 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord |
type MaxSym2 (arg6989586621679389863 :: a6989586621679389754) (arg6989586621679389864 :: a6989586621679389754) = Max arg6989586621679389863 arg6989586621679389864 Source #
data MinSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 a6989586621679389754) Source #
Instances
SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type) Source # | |
SuppressUnusedWarnings (MinSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (MinSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) (arg6989586621679389867 :: a6989586621679389754) Source # | |
data MinSym1 (arg6989586621679389867 :: a6989586621679389754) :: (~>) a6989586621679389754 a6989586621679389754 Source #
Instances
(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type) Source # | |
SuppressUnusedWarnings (MinSym1 arg6989586621679389867 :: TyFun a6989586621679389754 a6989586621679389754 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (MinSym1 arg6989586621679389867 :: TyFun a a -> Type) (arg6989586621679389868 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord |
type MinSym2 (arg6989586621679389867 :: a6989586621679389754) (arg6989586621679389868 :: a6989586621679389754) = Min arg6989586621679389867 arg6989586621679389868 Source #
data ComparingSym0 :: forall b6989586621679389744 a6989586621679389743. (~>) ((~>) b6989586621679389744 a6989586621679389743) ((~>) b6989586621679389744 ((~>) b6989586621679389744 Ordering)) Source #
Instances
SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ComparingSym0 Source # | |
SuppressUnusedWarnings (ComparingSym0 :: TyFun (b6989586621679389744 ~> a6989586621679389743) (b6989586621679389744 ~> (b6989586621679389744 ~> Ordering)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (ComparingSym0 :: TyFun (b6989586621679389744 ~> a6989586621679389743) (b6989586621679389744 ~> (b6989586621679389744 ~> Ordering)) -> Type) (a6989586621679389834 :: b6989586621679389744 ~> a6989586621679389743) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym0 :: TyFun (b6989586621679389744 ~> a6989586621679389743) (b6989586621679389744 ~> (b6989586621679389744 ~> Ordering)) -> Type) (a6989586621679389834 :: b6989586621679389744 ~> a6989586621679389743) = ComparingSym1 a6989586621679389834 |
data ComparingSym1 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) :: (~>) b6989586621679389744 ((~>) b6989586621679389744 Ordering) Source #
Instances
(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ComparingSym1 d) Source # | |
SuppressUnusedWarnings (ComparingSym1 a6989586621679389834 :: TyFun b6989586621679389744 (b6989586621679389744 ~> Ordering) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (ComparingSym1 a6989586621679389834 :: TyFun b6989586621679389744 (b6989586621679389744 ~> Ordering) -> Type) (a6989586621679389835 :: b6989586621679389744) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym1 a6989586621679389834 :: TyFun b6989586621679389744 (b6989586621679389744 ~> Ordering) -> Type) (a6989586621679389835 :: b6989586621679389744) = ComparingSym2 a6989586621679389834 a6989586621679389835 |
data ComparingSym2 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) (a6989586621679389835 :: b6989586621679389744) :: (~>) b6989586621679389744 Ordering Source #
Instances
(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ComparingSym2 d1 d2) Source # | |
SuppressUnusedWarnings (ComparingSym2 a6989586621679389835 a6989586621679389834 :: TyFun b6989586621679389744 Ordering -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (ComparingSym2 a6989586621679389835 a6989586621679389834 :: TyFun b Ordering -> Type) (a6989586621679389836 :: b) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym2 a6989586621679389835 a6989586621679389834 :: TyFun b Ordering -> Type) (a6989586621679389836 :: b) = Comparing a6989586621679389835 a6989586621679389834 a6989586621679389836 |
type ComparingSym3 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) (a6989586621679389835 :: b6989586621679389744) (a6989586621679389836 :: b6989586621679389744) = Comparing a6989586621679389834 a6989586621679389835 a6989586621679389836 Source #
data DownSym0 :: forall (a6989586621679089884 :: Type). (~>) a6989586621679089884 (Down (a6989586621679089884 :: Type)) Source #
Instances
SingI (DownSym0 :: TyFun a (Down a) -> Type) Source # | |
SuppressUnusedWarnings (DownSym0 :: TyFun a6989586621679089884 (Down a6989586621679089884) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
type Apply (DownSym0 :: TyFun a (Down a) -> Type) (t6989586621679398850 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord |