| 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.TH
Contents
Description
This module contains everything you need to derive your own singletons via Template Haskell.
TURN ON -XScopedTypeVariables IN YOUR MODULE IF YOU WANT THIS TO WORK.
Synopsis
- singletons :: OptionsMonad q => q [Dec] -> q [Dec]
- singletonsOnly :: OptionsMonad q => q [Dec] -> q [Dec]
- genSingletons :: OptionsMonad q => [Name] -> q [Dec]
- promote :: OptionsMonad q => q [Dec] -> q [Dec]
- promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]
- genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec]
- genPromotions :: OptionsMonad q => [Name] -> q [Dec]
- promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteEqInstance :: OptionsMonad q => Name -> q [Dec]
- singEqInstances :: OptionsMonad q => [Name] -> q [Dec]
- singEqInstance :: OptionsMonad q => Name -> q [Dec]
- singEqInstancesOnly :: OptionsMonad q => [Name] -> q [Dec]
- singEqInstanceOnly :: OptionsMonad q => Name -> q [Dec]
- singDecideInstances :: OptionsMonad q => [Name] -> q [Dec]
- singDecideInstance :: OptionsMonad q => Name -> q [Dec]
- promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]
- singOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
- singOrdInstance :: OptionsMonad q => Name -> q [Dec]
- promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]
- singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
- singBoundedInstance :: OptionsMonad q => Name -> q [Dec]
- promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]
- singEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
- singEnumInstance :: OptionsMonad q => Name -> q [Dec]
- promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteShowInstance :: OptionsMonad q => Name -> q [Dec]
- singShowInstances :: OptionsMonad q => [Name] -> q [Dec]
- singShowInstance :: OptionsMonad q => Name -> q [Dec]
- showSingInstances :: OptionsMonad q => [Name] -> q [Dec]
- showSingInstance :: OptionsMonad q => Name -> q [Dec]
- singITyConInstances :: DsMonad q => [Int] -> q [Dec]
- singITyConInstance :: DsMonad q => Int -> q [Dec]
- cases :: DsMonad q => Name -> q Exp -> q Exp -> q Exp
- sCases :: OptionsMonad q => Name -> q Exp -> q Exp -> q Exp
- data SBool z where
- data STuple0 z where
- data STuple2 z where
- data STuple3 z where
- data STuple4 z where
- data STuple5 z where
- data STuple6 z where
- STuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple6 ('(n, n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type))
- data STuple7 z where
- STuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple7 ('(n, n, n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type))
- data SOrdering z where
- module Data.Singletons
- class PEq a where
- type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
- sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
- type family (a :: Bool) && (b :: Bool) :: Bool where ...
- (%&&) :: Sing a -> Sing b -> Sing (a && b)
- class SEq k where
- class POrd a 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 ThenCmp a a where ...
- sThenCmp :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering)
- class SDecide k where
- data (a :: k) :~: (b :: k) where
- data Void
- type Refuted a = a -> Void
- data Decision a
- class PBounded a where
- class SBounded a where
- sMinBound :: Sing (MinBoundSym0 :: a)
- sMaxBound :: Sing (MaxBoundSym0 :: a)
- class PEnum a where
- class SEnum a where
- class PShow a where
- class SShow a where
- sShowsPrec :: forall (t :: Nat) (t :: a) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t :: Symbol)
- sShow_ :: forall (t :: a). Sing t -> Sing (Apply Show_Sym0 t :: Symbol)
- sShowList :: forall (t :: [a]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t :: Symbol)
- type family ShowString a a where ...
- sShowString :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowStringSym0 t) t :: Symbol)
- type family ShowParen a a a where ...
- sShowParen :: forall (t :: Bool) (t :: (~>) Symbol Symbol) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowParenSym0 t) t) t :: Symbol)
- type family ShowSpace a where ...
- sShowSpace :: forall (t :: Symbol). Sing t -> Sing (Apply ShowSpaceSym0 t :: Symbol)
- type family ShowChar a a where ...
- sShowChar :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowCharSym0 t) t :: Symbol)
- type family ShowCommaSpace a where ...
- sShowCommaSpace :: forall (t :: Symbol). Sing t -> Sing (Apply ShowCommaSpaceSym0 t :: Symbol)
- class PFunctor f where
- class SFunctor f where
- class PFoldable t where
- type Fold (arg :: t m) :: m
- type FoldMap (arg :: (~>) a m) (arg :: t a) :: m
- type Foldr (arg :: (~>) a ((~>) b b)) (arg :: b) (arg :: t a) :: b
- type Foldr' (arg :: (~>) a ((~>) b b)) (arg :: b) (arg :: t a) :: b
- type Foldl (arg :: (~>) b ((~>) a b)) (arg :: b) (arg :: t a) :: b
- type Foldl' (arg :: (~>) b ((~>) a b)) (arg :: b) (arg :: t a) :: b
- type Foldr1 (arg :: (~>) a ((~>) a a)) (arg :: t a) :: a
- type Foldl1 (arg :: (~>) a ((~>) a a)) (arg :: t a) :: a
- type ToList (arg :: t a) :: [a]
- type Null (arg :: t a) :: Bool
- type Length (arg :: t a) :: Nat
- type Elem (arg :: a) (arg :: t a) :: Bool
- type Maximum (arg :: t a) :: a
- type Minimum (arg :: t a) :: a
- type Sum (arg :: t a) :: a
- type Product (arg :: t a) :: a
- class SFoldable t where
- sFold :: forall m (t :: t m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t :: m)
- sFoldMap :: forall a m (t :: (~>) a m) (t :: t a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t :: m)
- sFoldr :: forall a b (t :: (~>) a ((~>) b b)) (t :: b) (t :: t a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t :: b)
- sFoldr' :: forall a b (t :: (~>) a ((~>) b b)) (t :: b) (t :: t a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t :: b)
- sFoldl :: forall b a (t :: (~>) b ((~>) a b)) (t :: b) (t :: t a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t :: b)
- sFoldl' :: forall b a (t :: (~>) b ((~>) a b)) (t :: b) (t :: t a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t :: b)
- sFoldr1 :: forall a (t :: (~>) a ((~>) a a)) (t :: t a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t :: a)
- sFoldl1 :: forall a (t :: (~>) a ((~>) a a)) (t :: t a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t :: a)
- sToList :: forall a (t :: t a). Sing t -> Sing (Apply ToListSym0 t :: [a])
- sNull :: forall a (t :: t a). Sing t -> Sing (Apply NullSym0 t :: Bool)
- sLength :: forall a (t :: t a). Sing t -> Sing (Apply LengthSym0 t :: Nat)
- sElem :: forall a (t :: a) (t :: t a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t :: Bool)
- sMaximum :: forall a (t :: t a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t :: a)
- sMinimum :: forall a (t :: t a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t :: a)
- sSum :: forall a (t :: t a). SNum a => Sing t -> Sing (Apply SumSym0 t :: a)
- sProduct :: forall a (t :: t a). SNum a => Sing t -> Sing (Apply ProductSym0 t :: a)
- class PMonoid a where
- class SSemigroup a => SMonoid a where
- sMempty :: Sing (MemptySym0 :: a)
- sMappend :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t :: a)
- sMconcat :: forall (t :: [a]). Sing t -> Sing (Apply MconcatSym0 t :: a)
- class PTraversable t where
- class (SFunctor t, SFoldable t) => STraversable t where
- sTraverse :: forall a f b (t :: (~>) a (f b)) (t :: t a). SApplicative f => Sing t -> Sing t -> Sing (Apply (Apply TraverseSym0 t) t :: f (t b))
- sSequenceA :: forall f a (t :: t (f a)). SApplicative f => Sing t -> Sing (Apply SequenceASym0 t :: f (t a))
- sMapM :: forall a m b (t :: (~>) a (m b)) (t :: t a). SMonad m => Sing t -> Sing t -> Sing (Apply (Apply MapMSym0 t) t :: m (t b))
- sSequence :: forall m a (t :: t (m a)). SMonad m => Sing t -> Sing (Apply SequenceSym0 t :: m (t a))
- class PApplicative f where
- class SFunctor f => SApplicative f where
- sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t :: f a)
- (%<*>) :: forall a b (t :: f ((~>) a b)) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t :: f b)
- sLiftA2 :: forall a b c (t :: (~>) a ((~>) b c)) (t :: f a) (t :: f b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t :: f c)
- (%*>) :: forall a b (t :: f a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t :: f b)
- (%<*) :: forall a b (t :: f a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t :: f a)
- type family (a . a) a where ...
- (%.) :: forall b c a (t :: (~>) b c) (t :: (~>) a b) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (.@#@$) t) t) t :: c)
- data SomeSing k where
- type family Error str where ...
- sError :: HasCallStack => Sing (str :: Symbol) -> a
- data ErrorSym0 a6989586621679472252
- type ErrorSym1 (a6989586621679472252 :: k0) = Error a6989586621679472252 :: k
- type family Undefined where ...
- sUndefined :: HasCallStack => a
- type UndefinedSym0 = Undefined :: k
- type TrueSym0 = 'True :: Bool
- type FalseSym0 = 'False :: Bool
- data (==@#@$) a6989586621679370055
- data a6989586621679370055 ==@#@$$ a6989586621679370056
- type (==@#@$$$) (a6989586621679370055 :: a) (a6989586621679370056 :: a) = (==) a6989586621679370055 a6989586621679370056 :: Bool
- data (>@#@$) a6989586621679383655
- data a6989586621679383655 >@#@$$ a6989586621679383656
- type (>@#@$$$) (a6989586621679383655 :: a) (a6989586621679383656 :: a) = (>) a6989586621679383655 a6989586621679383656 :: Bool
- type LTSym0 = 'LT :: Ordering
- type EQSym0 = 'EQ :: Ordering
- type GTSym0 = 'GT :: Ordering
- type Tuple0Sym0 = '() :: ()
- data Tuple2Sym0 a6989586621679304233
- data Tuple2Sym1 a6989586621679304233 a6989586621679304234
- type Tuple2Sym2 (a6989586621679304233 :: a) (a6989586621679304234 :: b) = '(a6989586621679304233, a6989586621679304234) :: (a :: Type, b :: Type)
- data Tuple3Sym0 a6989586621679304264
- data Tuple3Sym1 a6989586621679304264 a6989586621679304265
- data Tuple3Sym2 a6989586621679304264 a6989586621679304265 a6989586621679304266
- type Tuple3Sym3 (a6989586621679304264 :: a) (a6989586621679304265 :: b) (a6989586621679304266 :: c) = '(a6989586621679304264, a6989586621679304265, a6989586621679304266) :: (a :: Type, b :: Type, c :: Type)
- data Tuple4Sym0 a6989586621679304310
- data Tuple4Sym1 a6989586621679304310 a6989586621679304311
- data Tuple4Sym2 a6989586621679304310 a6989586621679304311 a6989586621679304312
- data Tuple4Sym3 a6989586621679304310 a6989586621679304311 a6989586621679304312 a6989586621679304313
- type Tuple4Sym4 (a6989586621679304310 :: a) (a6989586621679304311 :: b) (a6989586621679304312 :: c) (a6989586621679304313 :: d) = '(a6989586621679304310, a6989586621679304311, a6989586621679304312, a6989586621679304313) :: (a :: Type, b :: Type, c :: Type, d :: Type)
- data Tuple5Sym0 a6989586621679304373
- data Tuple5Sym1 a6989586621679304373 a6989586621679304374
- data Tuple5Sym2 a6989586621679304373 a6989586621679304374 a6989586621679304375
- data Tuple5Sym3 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376
- data Tuple5Sym4 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376 a6989586621679304377
- type Tuple5Sym5 (a6989586621679304373 :: a) (a6989586621679304374 :: b) (a6989586621679304375 :: c) (a6989586621679304376 :: d) (a6989586621679304377 :: e) = '(a6989586621679304373, a6989586621679304374, a6989586621679304375, a6989586621679304376, a6989586621679304377) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type)
- data Tuple6Sym0 a6989586621679304455
- data Tuple6Sym1 a6989586621679304455 a6989586621679304456
- data Tuple6Sym2 a6989586621679304455 a6989586621679304456 a6989586621679304457
- data Tuple6Sym3 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458
- data Tuple6Sym4 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459
- data Tuple6Sym5 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459 a6989586621679304460
- type Tuple6Sym6 (a6989586621679304455 :: a) (a6989586621679304456 :: b) (a6989586621679304457 :: c) (a6989586621679304458 :: d) (a6989586621679304459 :: e) (a6989586621679304460 :: f) = '(a6989586621679304455, a6989586621679304456, a6989586621679304457, a6989586621679304458, a6989586621679304459, a6989586621679304460) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type)
- data Tuple7Sym0 a6989586621679304558
- data Tuple7Sym1 a6989586621679304558 a6989586621679304559
- data Tuple7Sym2 a6989586621679304558 a6989586621679304559 a6989586621679304560
- data Tuple7Sym3 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561
- data Tuple7Sym4 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562
- data Tuple7Sym5 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563
- data Tuple7Sym6 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563 a6989586621679304564
- type Tuple7Sym7 (a6989586621679304558 :: a) (a6989586621679304559 :: b) (a6989586621679304560 :: c) (a6989586621679304561 :: d) (a6989586621679304562 :: e) (a6989586621679304563 :: f) (a6989586621679304564 :: g) = '(a6989586621679304558, a6989586621679304559, a6989586621679304560, a6989586621679304561, a6989586621679304562, a6989586621679304563, a6989586621679304564) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)
- data CompareSym0 a6989586621679383640
- data CompareSym1 a6989586621679383640 a6989586621679383641
- type CompareSym2 (a6989586621679383640 :: a) (a6989586621679383641 :: a) = Compare a6989586621679383640 a6989586621679383641 :: Ordering
- data ThenCmpSym0 a6989586621679394586
- data ThenCmpSym1 a6989586621679394586 a6989586621679394587
- type ThenCmpSym2 (a6989586621679394586 :: Ordering) (a6989586621679394587 :: Ordering) = ThenCmp a6989586621679394586 a6989586621679394587 :: Ordering
- data FoldlSym0 a6989586621680492465
- data FoldlSym1 a6989586621680492465 a6989586621680492466
- data FoldlSym2 a6989586621680492465 a6989586621680492466 a6989586621680492467
- type FoldlSym3 (a6989586621680492465 :: (~>) b ((~>) a b)) (a6989586621680492466 :: b) (a6989586621680492467 :: t a) = Foldl a6989586621680492465 a6989586621680492466 a6989586621680492467 :: b
- type MinBoundSym0 = MinBound :: a
- type MaxBoundSym0 = MaxBound :: a
- data ShowsPrecSym0 a6989586621680279568
- data ShowsPrecSym1 a6989586621680279568 a6989586621680279569
- data ShowsPrecSym2 a6989586621680279568 a6989586621680279569 a6989586621680279570
- type ShowsPrecSym3 (a6989586621680279568 :: Nat) (a6989586621680279569 :: a) (a6989586621680279570 :: Symbol) = ShowsPrec a6989586621680279568 a6989586621680279569 a6989586621680279570 :: Symbol
- data ShowStringSym0 a6989586621680279523
- data ShowStringSym1 a6989586621680279523 a6989586621680279524
- type ShowStringSym2 (a6989586621680279523 :: Symbol) (a6989586621680279524 :: Symbol) = ShowString a6989586621680279523 a6989586621680279524 :: Symbol
- data ShowParenSym0 a6989586621680279507
- data ShowParenSym1 a6989586621680279507 a6989586621680279508
- data ShowParenSym2 a6989586621680279507 a6989586621680279508 a6989586621680279509
- data ShowSpaceSym0 a6989586621680279495
- type ShowSpaceSym1 (a6989586621680279495 :: Symbol) = ShowSpace a6989586621680279495 :: Symbol
- data ShowCharSym0 a6989586621680279534
- data ShowCharSym1 a6989586621680279534 a6989586621680279535
- type ShowCharSym2 (a6989586621680279534 :: Symbol) (a6989586621680279535 :: Symbol) = ShowChar a6989586621680279534 a6989586621680279535 :: Symbol
- data ShowCommaSpaceSym0 a6989586621680279489
- type ShowCommaSpaceSym1 (a6989586621680279489 :: Symbol) = ShowCommaSpace a6989586621680279489 :: Symbol
- data FmapSym0 a6989586621679559667
- data FmapSym1 a6989586621679559667 a6989586621679559668
- type FmapSym2 (a6989586621679559667 :: (~>) a b) (a6989586621679559668 :: f a) = Fmap a6989586621679559667 a6989586621679559668 :: f b
- data (<$@#@$) a6989586621679559672
- data a6989586621679559672 <$@#@$$ a6989586621679559673
- type (<$@#@$$$) (a6989586621679559672 :: a) (a6989586621679559673 :: f b) = (<$) a6989586621679559672 a6989586621679559673 :: f a
- data FoldMapSym0 a6989586621680492445
- data FoldMapSym1 a6989586621680492445 a6989586621680492446
- type FoldMapSym2 (a6989586621680492445 :: (~>) a m) (a6989586621680492446 :: t a) = FoldMap a6989586621680492445 a6989586621680492446 :: m
- type MemptySym0 = Mempty :: a
- data MappendSym0 a6989586621680347244
- data MappendSym1 a6989586621680347244 a6989586621680347245
- type MappendSym2 (a6989586621680347244 :: a) (a6989586621680347245 :: a) = Mappend a6989586621680347244 a6989586621680347245 :: a
- data FoldrSym0 a6989586621680492451
- data FoldrSym1 a6989586621680492451 a6989586621680492452
- data FoldrSym2 a6989586621680492451 a6989586621680492452 a6989586621680492453
- type FoldrSym3 (a6989586621680492451 :: (~>) a ((~>) b b)) (a6989586621680492452 :: b) (a6989586621680492453 :: t a) = Foldr a6989586621680492451 a6989586621680492452 a6989586621680492453 :: b
- data TraverseSym0 a6989586621680816742
- data TraverseSym1 a6989586621680816742 a6989586621680816743
- type TraverseSym2 (a6989586621680816742 :: (~>) a (f b)) (a6989586621680816743 :: t a) = Traverse a6989586621680816742 a6989586621680816743 :: f (t b)
- data PureSym0 a6989586621679559691
- type PureSym1 (a6989586621679559691 :: a) = Pure a6989586621679559691 :: f a
- data (<*>@#@$) a6989586621679559695
- data a6989586621679559695 <*>@#@$$ a6989586621679559696
- type (<*>@#@$$$) (a6989586621679559695 :: f ((~>) a b)) (a6989586621679559696 :: f a) = (<*>) a6989586621679559695 a6989586621679559696 :: f b
- data LiftA2Sym0 a6989586621679559701
- data LiftA2Sym1 a6989586621679559701 a6989586621679559702
- data LiftA2Sym2 a6989586621679559701 a6989586621679559702 a6989586621679559703
- type LiftA2Sym3 (a6989586621679559701 :: (~>) a ((~>) b c)) (a6989586621679559702 :: f a) (a6989586621679559703 :: f b) = LiftA2 a6989586621679559701 a6989586621679559702 a6989586621679559703 :: f c
- data (.@#@$) a6989586621679534187
- data a6989586621679534187 .@#@$$ a6989586621679534188
- data (a6989586621679534187 .@#@$$$ a6989586621679534188) a6989586621679534189
- type (.@#@$$$$) (a6989586621679534187 :: (~>) b c) (a6989586621679534188 :: (~>) a b) (a6989586621679534189 :: a) = (.) a6989586621679534187 a6989586621679534188 a6989586621679534189 :: c
- type NilSym0 = '[] :: [a :: Type]
- data (:@#@$) a6989586621679304138
- data a6989586621679304138 :@#@$$ a6989586621679304139
- type (:@#@$$$) (a6989586621679304138 :: a) (a6989586621679304139 :: [a]) = '(:) a6989586621679304138 a6989586621679304139 :: [a :: Type]
- class SuppressUnusedWarnings t where
- suppressUnusedWarnings :: ()
Primary Template Haskell generation functions
singletons :: OptionsMonad q => q [Dec] -> q [Dec] Source #
Make promoted and singled versions of all declarations given, retaining
the original declarations. See the
README
for further explanation.
singletonsOnly :: OptionsMonad q => q [Dec] -> q [Dec] Source #
Make promoted and singled versions of all declarations given, discarding the original declarations. Note that a singleton based on a datatype needs the original datatype, so this will fail if it sees any datatype declarations. Classes, instances, and functions are all fine.
genSingletons :: OptionsMonad q => [Name] -> q [Dec] Source #
Generate singled definitions for each of the provided type-level
declaration Names. For example, the singletons package itself uses
$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])
to generate singletons for Prelude types.
promote :: OptionsMonad q => q [Dec] -> q [Dec] Source #
Promote every declaration given to the type level, retaining the originals.
See the
README
for further explanation.
promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec] Source #
Promote each declaration, discarding the originals. Note that a promoted datatype uses the same definition as an original datatype, so this will not work with datatypes. Classes, instances, and functions are all fine.
genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec] Source #
genPromotions :: OptionsMonad q => [Name] -> q [Dec] Source #
Generate promoted definitions for each of the provided type-level
declaration Names. This is generally only useful with classes.
Functions to generate equality instances
promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for (==) (type-level equality) from the given types
promoteEqInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for (==) (type-level equality) from the given type
singEqInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SEq and type-level (==) for each type in the list
singEqInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SEq and type-level (==) for the given type
singEqInstancesOnly :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SEq (only -- no instance for (==), which SEq generally
relies on) for each type in the list
singEqInstanceOnly :: OptionsMonad q => Name -> q [Dec] Source #
Create instances of SEq (only -- no instance for (==), which SEq generally
relies on) for the given type
singDecideInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SDecide, TestEquality, and TestCoercion for each
type in the list.
singDecideInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SDecide, TestEquality, and TestCoercion for the
given type.
Functions to generate Ord instances
promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for POrd from the given types
promoteOrdInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for POrd from the given type
singOrdInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SOrd for the given types
singOrdInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SOrd for the given type
Functions to generate Bounded instances
promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for PBounded from the given types
promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for PBounded from the given type
singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SBounded for the given types
singBoundedInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SBounded for the given type
Functions to generate Enum instances
promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for PEnum from the given types
promoteEnumInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for PEnum from the given type
singEnumInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SEnum for the given types
singEnumInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SEnum for the given type
Functions to generate Show instances
promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for PShow from the given types
promoteShowInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for PShow from the given type
singShowInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SShow for the given types
(Not to be confused with showSingInstances.)
singShowInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SShow for the given type
(Not to be confused with showShowInstance.)
showSingInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of Show for the given singleton types
(Not to be confused with singShowInstances.)
showSingInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of Show for the given singleton type
(Not to be confused with singShowInstance.)
Utility functions
singITyConInstances :: DsMonad q => [Int] -> q [Dec] Source #
Create an instance for , where SingI TyCon{N}N is the positive
number provided as an argument.
Note that the generated code requires the use of the QuantifiedConstraints
language extension.
singITyConInstance :: DsMonad q => Int -> q [Dec] Source #
Create an instance for , where SingI TyCon{N}N is the positive
number provided as an argument.
Note that the generated code requires the use of the QuantifiedConstraints
language extension.
Arguments
| :: DsMonad q | |
| => Name | The head of the type of the scrutinee. (Like |
| -> q Exp | The scrutinee, in a Template Haskell quote |
| -> q Exp | The body, in a Template Haskell quote |
| -> q Exp |
The function cases generates a case expression where each right-hand side
is identical. This may be useful if the type-checker requires knowledge of which
constructor is used to satisfy equality or type-class constraints, but where
each constructor is treated the same.
Arguments
| :: OptionsMonad q | |
| => Name | The head of the type the scrutinee's type is based on.
(Like |
| -> q Exp | The scrutinee, in a Template Haskell quote |
| -> q Exp | The body, in a Template Haskell quote |
| -> q Exp |
The function sCases generates a case expression where each right-hand side
is identical. This may be useful if the type-checker requires knowledge of which
constructor is used to satisfy equality or type-class constraints, but where
each constructor is treated the same. For sCases, unlike cases, the
scrutinee is a singleton. But make sure to pass in the name of the original
datatype, preferring ''Maybe over ''SMaybe.
Basic singleton definitions
Instances
| TestCoercion SBool Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| TestEquality SBool Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| Show (SBool z) Source # | |
Instances
| TestCoercion STuple0 Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| TestEquality STuple0 Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| Show (STuple0 z) Source # | |
Constructors
| STuple2 :: forall (a :: Type) (b :: Type) (n :: a) (n :: b). (Sing n) -> (Sing n) -> STuple2 ('(n, n) :: (a :: Type, b :: Type)) |
Instances
Constructors
| STuple3 :: forall (a :: Type) (b :: Type) (c :: Type) (n :: a) (n :: b) (n :: c). (Sing n) -> (Sing n) -> (Sing n) -> STuple3 ('(n, n, n) :: (a :: Type, b :: Type, c :: Type)) |
Instances
| (SDecide a, SDecide b, SDecide c) => TestCoercion (STuple3 :: (a, b, c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (SDecide a, SDecide b, SDecide c) => TestEquality (STuple3 :: (a, b, c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (ShowSing a, ShowSing b, ShowSing c) => Show (STuple3 z) Source # | |
Constructors
| STuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (n :: a) (n :: b) (n :: c) (n :: d). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple4 ('(n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type)) |
Instances
| (SDecide a, SDecide b, SDecide c, SDecide d) => TestCoercion (STuple4 :: (a, b, c, d) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (SDecide a, SDecide b, SDecide c, SDecide d) => TestEquality (STuple4 :: (a, b, c, d) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (STuple4 z) Source # | |
Constructors
| STuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple5 ('(n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type)) |
Instances
| (SDecide a, SDecide b, SDecide c, SDecide d, SDecide e) => TestCoercion (STuple5 :: (a, b, c, d, e) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (SDecide a, SDecide b, SDecide c, SDecide d, SDecide e) => TestEquality (STuple5 :: (a, b, c, d, e) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (STuple5 z) Source # | |
Constructors
| STuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple6 ('(n, n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type)) |
Instances
| (SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f) => TestCoercion (STuple6 :: (a, b, c, d, e, f) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f) => TestEquality (STuple6 :: (a, b, c, d, e, f) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (STuple6 z) Source # | |
Constructors
| STuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> (Sing n) -> STuple7 ('(n, n, n, n, n, n, n) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type)) |
Instances
| (SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f, SDecide g) => TestCoercion (STuple7 :: (a, b, c, d, e, f, g) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f, SDecide g) => TestEquality (STuple7 :: (a, b, c, d, e, f, g) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| (ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (STuple7 z) Source # | |
data SOrdering z where Source #
Constructors
| SLT :: SOrdering ('LT :: Ordering) | |
| SEQ :: SOrdering ('EQ :: Ordering) | |
| SGT :: SOrdering ('GT :: Ordering) |
Instances
| TestCoercion SOrdering Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| TestEquality SOrdering Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| Show (SOrdering z) Source # | |
module Data.Singletons
Auxiliary definitions
These definitions might be mentioned in code generated by Template Haskell, so they must be in scope.
The promoted analogue of Eq. If you supply no definition for (==),
then it defaults to a use of DefaultEq.
Associated Types
type (x :: a) == (y :: a) :: Bool infix 4 Source #
type (x :: a) == (y :: a) = x `DefaultEq` y
Instances
| PEq Bool Source # | |
| PEq Ordering Source # | |
| PEq Nat Source # | |
| PEq Symbol Source # | |
| PEq () Source # | |
| PEq Void Source # | |
| PEq All Source # | |
| PEq Any Source # | |
| PEq [a] Source # | |
| PEq (Maybe a) Source # | |
| PEq (TYPE rep) Source # | |
| PEq (Min a) Source # | |
| PEq (Max a) Source # | |
| PEq (First a) Source # | |
| PEq (Last a) Source # | |
| PEq (WrappedMonoid m) Source # | |
| PEq (Option a) Source # | |
| PEq (Identity a) Source # | |
| PEq (First a) Source # | |
| PEq (Last a) Source # | |
| PEq (Dual a) Source # | |
| PEq (Sum a) Source # | |
| PEq (Product a) Source # | |
| PEq (Down a) Source # | |
| PEq (NonEmpty a) Source # | |
| PEq (Either a b) Source # | |
| PEq (a, b) Source # | |
| PEq (Arg a b) Source # | |
| PEq (Proxy s) Source # | |
| PEq (a, b, c) Source # | |
| PEq (Const a b) Source # | |
| PEq (a, b, c, d) Source # | |
| PEq (a, b, c, d, e) Source # | |
| PEq (a, b, c, d, e, f) Source # | |
| PEq (a, b, c, d, e, f, g) Source # | |
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #
Type-level If. If True a b ==> a; If False a b ==> b
The singleton analogue of Eq. Unlike the definition for Eq, it is required
that instances define a body for (%==). You may also supply a body for (%/=).
Minimal complete definition
Methods
(%==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a == b) infix 4 Source #
Boolean equality on singletons
(%/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a /= b) infix 4 Source #
Boolean disequality on singletons
Instances
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 (Min a) Source # | |
| POrd (Max a) Source # | |
| POrd (First a) Source # | |
| POrd (Last a) Source # | |
| POrd (WrappedMonoid m) Source # | |
| POrd (Option a) Source # | |
| POrd (Identity a) Source # | |
| POrd (First a) Source # | |
| POrd (Last a) Source # | |
| POrd (Dual a) Source # | |
| POrd (Sum a) Source # | |
| POrd (Product a) Source # | |
| POrd (Down a) Source # | |
| POrd (NonEmpty a) Source # | |
| POrd (Either a b) Source # | |
| POrd (a, b) Source # | |
| POrd (Arg a b) Source # | |
| POrd (Proxy s) 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_6989586621679383674Sym0 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_6989586621679383695Sym0 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_6989586621679383711Sym0 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_6989586621679383727Sym0 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_6989586621679383743Sym0 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_6989586621679383759Sym0 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 (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 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 (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 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 (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 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 (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 (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 (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 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 (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 [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 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 (Proxy s) Source # | |
Defined in Data.Singletons.Prelude.Proxy Methods sCompare :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Proxy s) (t :: Proxy s). 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 # | |
sThenCmp :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering) Source #
class SDecide k where Source #
Members of the SDecide "kind" class support decidable equality. Instances
of this class are generated alongside singleton definitions for datatypes that
derive an Eq instance.
Methods
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) infix 4 Source #
Compute a proof or disproof of equality, given two singletons.
Instances
data (a :: k) :~: (b :: k) where infix 4 #
Propositional equality. If a :~: b is inhabited by some terminating
value, then the type a is the same as the type b. To use this equality
in practice, pattern-match on the a :~: b to get out the Refl constructor;
in the body of the pattern-match, the compiler knows that a ~ b.
Since: base-4.7.0.0
Instances
| TestCoercion ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Coercion | |
| TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
| a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> a :~: b # fromEnum :: (a :~: b) -> Int # enumFrom :: (a :~: b) -> [a :~: b] # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] # | |
| Eq (a :~: b) | Since: base-4.7.0.0 |
| (a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) # toConstr :: (a :~: b) -> Constr # dataTypeOf :: (a :~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # | |
| Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |
| Show (a :~: b) | Since: base-4.7.0.0 |
Uninhabited data type
Since: base-4.8.0.0
Instances
| Eq Void | Since: base-4.8.0.0 |
| Data Void | Since: base-4.8.0.0 |
Defined in Data.Void Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Void -> c Void # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Void # dataTypeOf :: Void -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Void) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Void) # gmapT :: (forall b. Data b => b -> b) -> Void -> Void # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r # gmapQ :: (forall d. Data d => d -> u) -> Void -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Void -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Void -> m Void # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void # | |
| Ord Void | Since: base-4.8.0.0 |
| Read Void | Reading a Since: base-4.8.0.0 |
| Show Void | Since: base-4.8.0.0 |
| Ix Void | Since: base-4.8.0.0 |
| Generic Void | Since: base-4.8.0.0 |
| Semigroup Void | Since: base-4.9.0.0 |
| Exception Void | Since: base-4.8.0.0 |
Defined in Data.Void Methods toException :: Void -> SomeException # fromException :: SomeException -> Maybe Void # displayException :: Void -> String # | |
| SingKind Void Source # | |
| SDecide Void Source # | |
| PEq Void Source # | |
| SEq Void 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 # | |
| POrd Void Source # | |
| SSemigroup Void Source # | |
| PSemigroup Void Source # | |
| SShow Void Source # | |
Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Void) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Void). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Void]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source # | |
| PShow Void Source # | |
| Lift Void | Since: template-haskell-2.15.0.0 |
| TestCoercion SVoid Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| TestEquality SVoid Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| SingI (AbsurdSym0 :: TyFun Void a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Void Methods sing :: Sing AbsurdSym0 Source # | |
| SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Void Methods suppressUnusedWarnings :: () Source # | |
| type Rep Void | |
| type Demote Void Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| type Sing Source # | |
Defined in Data.Singletons.Prelude.Instances | |
| type Sconcat (arg :: NonEmpty Void) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
| type Show_ (arg :: Void) Source # | |
Defined in Data.Singletons.Prelude.Show | |
| type (a :: Void) == (b :: Void) Source # | |
Defined in Data.Singletons.Prelude.Eq | |
| type (x :: Void) /= (y :: Void) Source # | |
| type Compare (a1 :: Void) (a2 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Ord | |
| type (arg1 :: Void) < (arg2 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Ord | |
| type (arg1 :: Void) <= (arg2 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Ord | |
| type (arg1 :: Void) > (arg2 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Ord | |
| type (arg1 :: Void) >= (arg2 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Ord | |
| type Max (arg1 :: Void) (arg2 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Ord | |
| type Min (arg1 :: Void) (arg2 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Ord | |
| type (a1 :: Void) <> (a2 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal | |
| type ShowList (arg1 :: [Void]) arg2 Source # | |
Defined in Data.Singletons.Prelude.Show | |
| type ShowsPrec a1 (a2 :: Void) a3 Source # | |
Defined in Data.Singletons.Prelude.Show | |
| type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679359469 :: Void) Source # | |
Defined in Data.Singletons.Prelude.Void type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679359469 :: Void) = AbsurdSym1 a6989586621679359469 :: k2 | |
A Decision about a type a is either a proof of existence or a proof that a
cannot exist.
Instances
| PBounded Bool Source # | |
| PBounded Ordering Source # | |
| PBounded () Source # | |
| PBounded All Source # | |
| PBounded Any Source # | |
| PBounded (Min a) Source # | |
| PBounded (Max a) Source # | |
| PBounded (First a) Source # | |
| PBounded (Last a) Source # | |
| PBounded (WrappedMonoid m) Source # | |
| PBounded (Identity a) Source # | |
| PBounded (Dual a) Source # | |
| PBounded (Sum a) Source # | |
| PBounded (Product a) Source # | |
| PBounded (a, b) Source # | |
| PBounded (Proxy s) Source # | |
| PBounded (a, b, c) Source # | |
| PBounded (Const a b) Source # | |
| PBounded (a, b, c, d) Source # | |
| PBounded (a, b, c, d, e) Source # | |
| PBounded (a, b, c, d, e, f) Source # | |
| PBounded (a, b, c, d, e, f, g) Source # | |
class SBounded a where Source #
Instances
Methods
sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t :: a) Source #
sFromEnum :: forall (t :: a). Sing t -> Sing (Apply FromEnumSym0 t :: Nat) Source #
Instances
Associated Types
type ShowsPrec (arg :: Nat) (arg :: a) (arg :: Symbol) :: Symbol Source #
type Show_ (arg :: a) :: Symbol Source #
type ShowList (arg :: [a]) (arg :: Symbol) :: Symbol Source #
Instances
| PShow Bool Source # | |
| PShow Ordering Source # | |
| PShow Nat Source # | |
| PShow Symbol Source # | |
| PShow () Source # | |
| PShow Void Source # | |
| PShow All Source # | |
| PShow Any Source # | |
| PShow [a] Source # | |
| PShow (Maybe a) Source # | |
| PShow (Min a) Source # | |
| PShow (Max a) Source # | |
| PShow (First a) Source # | |
| PShow (Last a) Source # | |
| PShow (WrappedMonoid m) Source # | |
| PShow (Option a) Source # | |
| PShow (Identity a) Source # | |
| PShow (First a) Source # | |
| PShow (Last a) Source # | |
| PShow (Dual a) Source # | |
| PShow (Sum a) Source # | |
| PShow (Product a) Source # | |
| PShow (NonEmpty a) Source # | |
| PShow (Either a b) Source # | |
| PShow (a, b) Source # | |
| PShow (Arg a b) Source # | |
| PShow (Proxy s) Source # | |
| PShow (a, b, c) Source # | |
| PShow (Const a b) Source # | |
| PShow (a, b, c, d) Source # | |
| PShow (a, b, c, d, e) Source # | |
| PShow (a, b, c, d, e, f) Source # | |
| PShow (a, b, c, d, e, f, g) Source # | |
Minimal complete definition
Nothing
Methods
sShowsPrec :: forall (t :: Nat) (t :: a) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t :: Symbol) Source #
default sShowsPrec :: forall (t :: Nat) (t :: a) (t :: Symbol). (Apply (Apply (Apply ShowsPrecSym0 t) t) t :: Symbol) ~ Apply (Apply (Apply ShowsPrec_6989586621680279582Sym0 t) t) t => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t :: Symbol) Source #
sShow_ :: forall (t :: a). Sing t -> Sing (Apply Show_Sym0 t :: Symbol) Source #
default sShow_ :: forall (t :: a). (Apply Show_Sym0 t :: Symbol) ~ Apply Show__6989586621680279594Sym0 t => Sing t -> Sing (Apply Show_Sym0 t :: Symbol) Source #
sShowList :: forall (t :: [a]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t :: Symbol) Source #
Instances
type family ShowString a a where ... Source #
Equations
| ShowString a_6989586621680279516 a_6989586621680279518 = Apply (Apply (<>@#@$) a_6989586621680279516) a_6989586621680279518 |
sShowString :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowStringSym0 t) t :: Symbol) Source #
sShowParen :: forall (t :: Bool) (t :: (~>) Symbol Symbol) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowParenSym0 t) t) t :: Symbol) Source #
sShowSpace :: forall (t :: Symbol). Sing t -> Sing (Apply ShowSpaceSym0 t :: Symbol) Source #
sShowChar :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowCharSym0 t) t :: Symbol) Source #
type family ShowCommaSpace a where ... Source #
Equations
| ShowCommaSpace a_6989586621680279485 = Apply (Apply ShowStringSym0 ", ") a_6989586621680279485 |
sShowCommaSpace :: forall (t :: Symbol). Sing t -> Sing (Apply ShowCommaSpaceSym0 t :: Symbol) Source #
Instances
| PFunctor [] Source # | |
| PFunctor Maybe Source # | |
| PFunctor Min Source # | |
| PFunctor Max Source # | |
| PFunctor First Source # | |
| PFunctor Last Source # | |
| PFunctor Option Source # | |
| PFunctor Identity Source # | |
| PFunctor First Source # | |
| PFunctor Last Source # | |
| PFunctor Dual Source # | |
| PFunctor Sum Source # | |
| PFunctor Product Source # | |
| PFunctor Down Source # | |
| PFunctor NonEmpty Source # | |
| PFunctor (Either a) Source # | |
| PFunctor ((,) a) Source # | |
| PFunctor (Arg a) Source # | |
| PFunctor (Proxy :: Type -> Type) Source # | |
| PFunctor (Const m :: Type -> Type) Source # | |
class SFunctor f where Source #
Minimal complete definition
Methods
sFmap :: forall a b (t :: (~>) a b) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t :: f b) Source #
(%<$) :: forall a b (t :: a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a) infixl 4 Source #
Instances
| SFunctor [] Source # | |
| SFunctor Maybe Source # | |
| SFunctor Min Source # | |
| SFunctor Max Source # | |
| SFunctor First Source # | |
| SFunctor Last Source # | |
| SFunctor Option Source # | |
| SFunctor Identity Source # | |
| SFunctor First Source # | |
| SFunctor Last Source # | |
| SFunctor Dual Source # | |
| SFunctor Sum Source # | |
| SFunctor Product Source # | |
| SFunctor Down Source # | |
| SFunctor NonEmpty Source # | |
| SFunctor (Either a) Source # | |
| SFunctor ((,) a) Source # | |
| SFunctor (Arg a) Source # | |
| SFunctor (Proxy :: Type -> Type) Source # | |
| SFunctor (Const m :: Type -> Type) Source # | |
Associated Types
type Fold (arg :: t m) :: m Source #
type FoldMap (arg :: (~>) a m) (arg :: t a) :: m Source #
type Foldr (arg :: (~>) a ((~>) b b)) (arg :: b) (arg :: t a) :: b Source #
type Foldr' (arg :: (~>) a ((~>) b b)) (arg :: b) (arg :: t a) :: b Source #
type Foldl (arg :: (~>) b ((~>) a b)) (arg :: b) (arg :: t a) :: b Source #
type Foldl' (arg :: (~>) b ((~>) a b)) (arg :: b) (arg :: t a) :: b Source #
type Foldr1 (arg :: (~>) a ((~>) a a)) (arg :: t a) :: a Source #
type Foldl1 (arg :: (~>) a ((~>) a a)) (arg :: t a) :: a Source #
type ToList (arg :: t a) :: [a] Source #
type Null (arg :: t a) :: Bool Source #
type Length (arg :: t a) :: Nat Source #
type Elem (arg :: a) (arg :: t a) :: Bool Source #
type Maximum (arg :: t a) :: a Source #
type Minimum (arg :: t a) :: a Source #
Instances
| PFoldable [] Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Maybe Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Min Source # | |
Defined in Data.Singletons.Prelude.Semigroup Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Max Source # | |
Defined in Data.Singletons.Prelude.Semigroup Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable First Source # | |
Defined in Data.Singletons.Prelude.Semigroup Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Last Source # | |
Defined in Data.Singletons.Prelude.Semigroup Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Option Source # | |
Defined in Data.Singletons.Prelude.Semigroup Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Identity Source # | |
Defined in Data.Singletons.Prelude.Identity Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable First Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Last Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Dual Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Sum Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable Product Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable NonEmpty Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable (Either a) Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable ((,) a) Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable (Arg a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable (Proxy :: Type -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
| PFoldable (Const m :: Type -> Type) Source # | |
Defined in Data.Singletons.Prelude.Const Associated Types type FoldMap arg arg :: m Source # type Foldr arg arg arg :: b Source # type Foldr' arg arg arg :: b Source # type Foldl arg arg arg :: b Source # type Foldl' arg arg arg :: b Source # type Foldr1 arg arg :: a Source # type Foldl1 arg arg :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Nat Source # type Elem arg arg :: Bool Source # type Maximum arg :: a Source # | |
class SFoldable t where Source #
Minimal complete definition
Nothing
Methods
sFold :: forall m (t :: t m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t :: m) Source #
default sFold :: forall m (t :: t m). ((Apply FoldSym0 t :: m) ~ Apply Fold_6989586621680492512Sym0 t, SMonoid m) => Sing t -> Sing (Apply FoldSym0 t :: m) Source #
sFoldMap :: forall a m (t :: (~>) a m) (t :: t a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t :: m) Source #
default sFoldMap :: forall a m (t :: (~>) a m) (t :: t a). ((Apply (Apply FoldMapSym0 t) t :: m) ~ Apply (Apply FoldMap_6989586621680492522Sym0 t) t, SMonoid m) => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t :: m) Source #
sFoldr :: forall a b (t :: (~>) a ((~>) b b)) (t :: b) (t :: t a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t :: b) Source #
default sFoldr :: forall a b (t :: (~>) a ((~>) b b)) (t :: b) (t :: t a). (Apply (Apply (Apply FoldrSym0 t) t) t :: b) ~ Apply (Apply (Apply Foldr_6989586621680492536Sym0 t) t) t => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t :: b) Source #
sFoldr' :: forall a b (t :: (~>) a ((~>) b b)) (t :: b) (t :: t a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t :: b) Source #
default sFoldr' :: forall a b (t :: (~>) a ((~>) b b)) (t :: b) (t :: t a). (Apply (Apply (Apply Foldr'Sym0 t) t) t :: b) ~ Apply (Apply (Apply Foldr'_6989586621680492551Sym0 t) t) t => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t :: b) Source #
sFoldl :: forall b a (t :: (~>) b ((~>) a b)) (t :: b) (t :: t a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t :: b) Source #
default sFoldl :: forall b a (t :: (~>) b ((~>) a b)) (t :: b) (t :: t a). (Apply (Apply (Apply FoldlSym0 t) t) t :: b) ~ Apply (Apply (Apply Foldl_6989586621680492574Sym0 t) t) t => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t :: b) Source #
sFoldl' :: forall b a (t :: (~>) b ((~>) a b)) (t :: b) (t :: t a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t :: b) Source #
default sFoldl' :: forall b a (t :: (~>) b ((~>) a b)) (t :: b) (t :: t a). (Apply (Apply (Apply Foldl'Sym0 t) t) t :: b) ~ Apply (Apply (Apply Foldl'_6989586621680492589Sym0 t) t) t => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t :: b) Source #
sFoldr1 :: forall a (t :: (~>) a ((~>) a a)) (t :: t a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t :: a) Source #
default sFoldr1 :: forall a (t :: (~>) a ((~>) a a)) (t :: t a). (Apply (Apply Foldr1Sym0 t) t :: a) ~ Apply (Apply Foldr1_6989586621680492611Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t :: a) Source #
sFoldl1 :: forall a (t :: (~>) a ((~>) a a)) (t :: t a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t :: a) Source #
default sFoldl1 :: forall a (t :: (~>) a ((~>) a a)) (t :: t a). (Apply (Apply Foldl1Sym0 t) t :: a) ~ Apply (Apply Foldl1_6989586621680492632Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t :: a) Source #
sToList :: forall a (t :: t a). Sing t -> Sing (Apply ToListSym0 t :: [a]) Source #
default sToList :: forall a (t :: t a). (Apply ToListSym0 t :: [a]) ~ Apply ToList_6989586621680492652Sym0 t => Sing t -> Sing (Apply ToListSym0 t :: [a]) Source #
sNull :: forall a (t :: t a). Sing t -> Sing (Apply NullSym0 t :: Bool) Source #
default sNull :: forall a (t :: t a). (Apply NullSym0 t :: Bool) ~ Apply Null_6989586621680492661Sym0 t => Sing t -> Sing (Apply NullSym0 t :: Bool) Source #
sLength :: forall a (t :: t a). Sing t -> Sing (Apply LengthSym0 t :: Nat) Source #
default sLength :: forall a (t :: t a). (Apply LengthSym0 t :: Nat) ~ Apply Length_6989586621680492678Sym0 t => Sing t -> Sing (Apply LengthSym0 t :: Nat) Source #
sElem :: forall a (t :: a) (t :: t a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t :: Bool) Source #
default sElem :: forall a (t :: a) (t :: t a). ((Apply (Apply ElemSym0 t) t :: Bool) ~ Apply (Apply Elem_6989586621680492697Sym0 t) t, SEq a) => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t :: Bool) Source #
sMaximum :: forall a (t :: t a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t :: a) Source #
default sMaximum :: forall a (t :: t a). ((Apply MaximumSym0 t :: a) ~ Apply Maximum_6989586621680492711Sym0 t, SOrd a) => Sing t -> Sing (Apply MaximumSym0 t :: a) Source #
sMinimum :: forall a (t :: t a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t :: a) Source #
default sMinimum :: forall a (t :: t a). ((Apply MinimumSym0 t :: a) ~ Apply Minimum_6989586621680492726Sym0 t, SOrd a) => Sing t -> Sing (Apply MinimumSym0 t :: a) Source #
sSum :: forall a (t :: t a). SNum a => Sing t -> Sing (Apply SumSym0 t :: a) Source #
default sSum :: forall a (t :: t a). ((Apply SumSym0 t :: a) ~ Apply Sum_6989586621680492741Sym0 t, SNum a) => Sing t -> Sing (Apply SumSym0 t :: a) Source #
sProduct :: forall a (t :: t a). SNum a => Sing t -> Sing (Apply ProductSym0 t :: a) Source #
Instances
| SFoldable [] Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: [m]). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: [a]). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: [a]). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: [a]). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: [a]). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: [a]). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: [a]). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: [a]). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: [a]). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Maybe Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: Maybe m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Maybe a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Maybe a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Maybe a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Maybe a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Maybe a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Maybe a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Maybe a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Maybe a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Maybe a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Maybe a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Maybe a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Maybe a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Maybe a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Min Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sFold :: forall m (t :: Min m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Min a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Min a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Min a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Min a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Min a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Min a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Min a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Min a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Min a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Min a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Min a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Min a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Min a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Max Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sFold :: forall m (t :: Max m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Max a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Max a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Max a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Max a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Max a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Max a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Max a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Max a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Max a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Max a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Max a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Max a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Max a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable First Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sFold :: forall m (t :: First m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: First a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: First a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: First a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: First a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: First a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: First a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: First a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: First a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: First a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Last Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sFold :: forall m (t :: Last m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Last a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Last a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Last a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Last a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Last a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Last a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Last a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Last a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Last a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Option Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sFold :: forall m (t :: Option m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Option a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Option a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Option a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Option a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Option a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Option a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Option a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Option a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Option a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Option a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Option a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Option a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Option a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Identity Source # | |
Defined in Data.Singletons.Prelude.Identity Methods sFold :: forall m (t :: Identity m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Identity a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Identity a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Identity a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Identity a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Identity a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Identity a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Identity a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Identity a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Identity a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable First Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: First m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: First a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: First a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: First a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: First a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: First a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: First a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: First a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: First a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: First a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Last Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: Last m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Last a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Last a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Last a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Last a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Last a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Last a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Last a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Last a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Last a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Dual Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: Dual m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Dual a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Dual a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Dual a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Dual a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Dual a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Dual a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Dual a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Dual a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Dual a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Dual a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Dual a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Dual a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Dual a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Sum Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: Sum m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Sum a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Sum a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Sum a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Sum a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Sum a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Sum a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Sum a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Sum a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Sum a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Sum a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Sum a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Sum a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Sum a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable Product Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: Product m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Product a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Product a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Product a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Product a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Product a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Product a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Product a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Product a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Product a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Product a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Product a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Product a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Product a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable NonEmpty Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: NonEmpty m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: NonEmpty a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: NonEmpty a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: NonEmpty a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: NonEmpty a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: NonEmpty a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: NonEmpty a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: NonEmpty a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: NonEmpty a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: NonEmpty a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: NonEmpty a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: NonEmpty a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: NonEmpty a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: NonEmpty a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable (Either a) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: Either a m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a0 m (t :: a0 ~> m) (t :: Either a a0). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a0 b (t :: a0 ~> (b ~> b)) (t :: b) (t :: Either a a0). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a0 b (t :: a0 ~> (b ~> b)) (t :: b) (t :: Either a a0). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a0 (t :: b ~> (a0 ~> b)) (t :: b) (t :: Either a a0). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a0 (t :: b ~> (a0 ~> b)) (t :: b) (t :: Either a a0). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a0 (t :: a0 ~> (a0 ~> a0)) (t :: Either a a0). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a0 (t :: a0 ~> (a0 ~> a0)) (t :: Either a a0). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a0 (t :: Either a a0). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a0 (t :: Either a a0). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a0 (t :: Either a a0). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a0 (t :: a0) (t :: Either a a0). SEq a0 => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a0 (t :: Either a a0). SOrd a0 => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a0 (t :: Either a a0). SOrd a0 => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a0 (t :: Either a a0). SNum a0 => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a0 (t :: Either a a0). SNum a0 => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable ((,) a) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: (a, m)). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a0 m (t :: a0 ~> m) (t :: (a, a0)). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a0 b (t :: a0 ~> (b ~> b)) (t :: b) (t :: (a, a0)). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a0 b (t :: a0 ~> (b ~> b)) (t :: b) (t :: (a, a0)). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a0 (t :: b ~> (a0 ~> b)) (t :: b) (t :: (a, a0)). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a0 (t :: b ~> (a0 ~> b)) (t :: b) (t :: (a, a0)). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a0 (t :: a0 ~> (a0 ~> a0)) (t :: (a, a0)). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a0 (t :: a0 ~> (a0 ~> a0)) (t :: (a, a0)). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a0 (t :: (a, a0)). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a0 (t :: (a, a0)). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a0 (t :: (a, a0)). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a0 (t :: a0) (t :: (a, a0)). SEq a0 => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a0 (t :: (a, a0)). SOrd a0 => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a0 (t :: (a, a0)). SOrd a0 => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a0 (t :: (a, a0)). SNum a0 => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a0 (t :: (a, a0)). SNum a0 => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable (Arg a) Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sFold :: forall m (t :: Arg a m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a0 m (t :: a0 ~> m) (t :: Arg a a0). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a0 b (t :: a0 ~> (b ~> b)) (t :: b) (t :: Arg a a0). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a0 b (t :: a0 ~> (b ~> b)) (t :: b) (t :: Arg a a0). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a0 (t :: b ~> (a0 ~> b)) (t :: b) (t :: Arg a a0). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a0 (t :: b ~> (a0 ~> b)) (t :: b) (t :: Arg a a0). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a0 (t :: a0 ~> (a0 ~> a0)) (t :: Arg a a0). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a0 (t :: a0 ~> (a0 ~> a0)) (t :: Arg a a0). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a0 (t :: Arg a a0). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a0 (t :: Arg a a0). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a0 (t :: Arg a a0). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a0 (t :: a0) (t :: Arg a a0). SEq a0 => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a0 (t :: Arg a a0). SOrd a0 => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a0 (t :: Arg a a0). SOrd a0 => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a0 (t :: Arg a a0). SNum a0 => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a0 (t :: Arg a a0). SNum a0 => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable (Proxy :: Type -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sFold :: forall m (t :: Proxy m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Proxy a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Proxy a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Proxy a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Proxy a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Proxy a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Proxy a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Proxy a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Proxy a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Proxy a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Proxy a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Proxy a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Proxy a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Proxy a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Proxy a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Proxy a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
| SFoldable (Const m :: Type -> Type) Source # | |
Defined in Data.Singletons.Prelude.Const Methods sFold :: forall m0 (t :: Const m m0). SMonoid m0 => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m0 (t :: a ~> m0) (t :: Const m a). SMonoid m0 => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source # sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Const m a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source # sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Const m a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source # sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Const m a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source # sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Const m a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source # sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Const m a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Const m a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Const m a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Const m a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Const m a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Const m a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Const m a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Const m a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Const m a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Const m a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source # | |
Instances
| PMonoid Ordering Source # | |
| PMonoid Symbol Source # | |
| PMonoid () Source # | |
| PMonoid All Source # | |
| PMonoid Any Source # | |
| PMonoid [a] Source # | |
| PMonoid (Maybe a) Source # | |
| PMonoid (Min a) Source # | |
| PMonoid (Max a) Source # | |
| PMonoid (WrappedMonoid m) Source # | |
| PMonoid (Option a) Source # | |
| PMonoid (Identity a) Source # | |
| PMonoid (First a) Source # | |
| PMonoid (Last a) Source # | |
| PMonoid (Dual a) Source # | |
| PMonoid (Sum a) Source # | |
| PMonoid (Product a) Source # | |
| PMonoid (Down a) Source # | |
| PMonoid (a, b) Source # | |
| PMonoid (Proxy s) Source # | |
| PMonoid (a ~> b) Source # | |
| PMonoid (a, b, c) Source # | |
| PMonoid (Const a b) Source # | |
| PMonoid (a, b, c, d) Source # | |
| PMonoid (a, b, c, d, e) Source # | |
class SSemigroup a => SMonoid a where Source #
Minimal complete definition
Methods
sMempty :: Sing (MemptySym0 :: a) Source #
sMappend :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t :: a) Source #
default sMappend :: forall (t :: a) (t :: a). (Apply (Apply MappendSym0 t) t :: a) ~ Apply (Apply Mappend_6989586621680347251Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t :: a) Source #
sMconcat :: forall (t :: [a]). Sing t -> Sing (Apply MconcatSym0 t :: a) Source #
default sMconcat :: forall (t :: [a]). (Apply MconcatSym0 t :: a) ~ Apply Mconcat_6989586621680347265Sym0 t => Sing t -> Sing (Apply MconcatSym0 t :: a) Source #
Instances
class PTraversable t Source #
Associated Types
type Traverse (arg :: (~>) a (f b)) (arg :: t a) :: f (t b) Source #
type SequenceA (arg :: t (f a)) :: f (t a) Source #
type MapM (arg :: (~>) a (m b)) (arg :: t a) :: m (t b) Source #
Instances
class (SFunctor t, SFoldable t) => STraversable t where Source #
Minimal complete definition
Nothing
Methods
sTraverse :: forall a f b (t :: (~>) a (f b)) (t :: t a). SApplicative f => Sing t -> Sing t -> Sing (Apply (Apply TraverseSym0 t) t :: f (t b)) Source #
default sTraverse :: forall a f b (t :: (~>) a (f b)) (t :: t a). ((Apply (Apply TraverseSym0 t) t :: f (t b)) ~ Apply (Apply Traverse_6989586621680816757Sym0 t) t, SApplicative f) => Sing t -> Sing t -> Sing (Apply (Apply TraverseSym0 t) t :: f (t b)) Source #
sSequenceA :: forall f a (t :: t (f a)). SApplicative f => Sing t -> Sing (Apply SequenceASym0 t :: f (t a)) Source #
default sSequenceA :: forall f a (t :: t (f a)). ((Apply SequenceASym0 t :: f (t a)) ~ Apply SequenceA_6989586621680816769Sym0 t, SApplicative f) => Sing t -> Sing (Apply SequenceASym0 t :: f (t a)) Source #
sMapM :: forall a m b (t :: (~>) a (m b)) (t :: t a). SMonad m => Sing t -> Sing t -> Sing (Apply (Apply MapMSym0 t) t :: m (t b)) Source #
default sMapM :: forall a m b (t :: (~>) a (m b)) (t :: t a). ((Apply (Apply MapMSym0 t) t :: m (t b)) ~ Apply (Apply MapM_6989586621680816779Sym0 t) t, SMonad m) => Sing t -> Sing t -> Sing (Apply (Apply MapMSym0 t) t :: m (t b)) Source #
sSequence :: forall m a (t :: t (m a)). SMonad m => Sing t -> Sing (Apply SequenceSym0 t :: m (t a)) Source #
Instances
class PApplicative f Source #
Associated Types
type Pure (arg :: a) :: f a Source #
type (arg :: f ((~>) a b)) <*> (arg :: f a) :: f b infixl 4 Source #
type LiftA2 (arg :: (~>) a ((~>) b c)) (arg :: f a) (arg :: f b) :: f c Source #
Instances
class SFunctor f => SApplicative f where Source #
Minimal complete definition
Methods
sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t :: f a) Source #
(%<*>) :: forall a b (t :: f ((~>) a b)) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t :: f b) infixl 4 Source #
default (%<*>) :: forall a b (t :: f ((~>) a b)) (t :: f a). (Apply (Apply (<*>@#@$) t) t :: f b) ~ Apply (Apply TFHelper_6989586621679559716Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t :: f b) Source #
sLiftA2 :: forall a b c (t :: (~>) a ((~>) b c)) (t :: f a) (t :: f b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t :: f c) Source #
default sLiftA2 :: forall a b c (t :: (~>) a ((~>) b c)) (t :: f a) (t :: f b). (Apply (Apply (Apply LiftA2Sym0 t) t) t :: f c) ~ Apply (Apply (Apply LiftA2_6989586621679559732Sym0 t) t) t => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t :: f c) Source #
(%*>) :: forall a b (t :: f a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t :: f b) infixl 4 Source #
default (%*>) :: forall a b (t :: f a) (t :: f b). (Apply (Apply (*>@#@$) t) t :: f b) ~ Apply (Apply TFHelper_6989586621679559748Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t :: f b) Source #
(%<*) :: forall a b (t :: f a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t :: f a) infixl 4 Source #
Instances
| SApplicative [] Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: [a ~> b]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Maybe Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Maybe (a ~> b)) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Maybe a) (t :: Maybe b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Maybe a) (t :: Maybe b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Maybe a) (t :: Maybe b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Min Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Min (a ~> b)) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Min a) (t :: Min b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Min a) (t :: Min b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Min a) (t :: Min b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Max Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Max (a ~> b)) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Max a) (t :: Max b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Max a) (t :: Max b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Max a) (t :: Max b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative First Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: First (a ~> b)) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: First a) (t :: First b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: First a) (t :: First b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: First a) (t :: First b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Last Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Last (a ~> b)) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Last a) (t :: Last b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Last a) (t :: Last b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Last a) (t :: Last b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Option Source # | |
Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Option (a ~> b)) (t :: Option a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Option a) (t :: Option b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Option a) (t :: Option b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Option a) (t :: Option b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Identity Source # | |
Defined in Data.Singletons.Prelude.Identity Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Identity (a ~> b)) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Identity a) (t :: Identity b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Identity a) (t :: Identity b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Identity a) (t :: Identity b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative First Source # | |
Defined in Data.Singletons.Prelude.Monoid Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: First (a ~> b)) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: First a) (t :: First b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: First a) (t :: First b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: First a) (t :: First b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Last Source # | |
Defined in Data.Singletons.Prelude.Monoid Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Last (a ~> b)) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Last a) (t :: Last b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Last a) (t :: Last b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Last a) (t :: Last b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Dual Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Dual (a ~> b)) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Dual a) (t :: Dual b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Dual a) (t :: Dual b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Dual a) (t :: Dual b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Sum Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Sum (a ~> b)) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Sum a) (t :: Sum b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Sum a) (t :: Sum b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Sum a) (t :: Sum b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Product Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Product (a ~> b)) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Product a) (t :: Product b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Product a) (t :: Product b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Product a) (t :: Product b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative Down Source # | |
Defined in Data.Singletons.Prelude.Applicative Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Down (a ~> b)) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Down a) (t :: Down b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Down a) (t :: Down b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Down a) (t :: Down b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative NonEmpty Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: NonEmpty (a ~> b)) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: NonEmpty a) (t :: NonEmpty b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: NonEmpty a) (t :: NonEmpty b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: NonEmpty a) (t :: NonEmpty b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative (Either e) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Either e (a ~> b)) (t :: Either e a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Either e a) (t :: Either e b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Either e a) (t :: Either e b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Either e a) (t :: Either e b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SMonoid a => SApplicative ((,) a) Source # | |
Defined in Data.Singletons.Prelude.Applicative Methods sPure :: forall a0 (t :: a0). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a0 b (t :: (a, a0 ~> b)) (t :: (a, a0)). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a0 b c (t :: a0 ~> (b ~> c)) (t :: (a, a0)) (t :: (a, b)). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a0 b (t :: (a, a0)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a0 b (t :: (a, a0)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SApplicative (Proxy :: Type -> Type) Source # | |
Defined in Data.Singletons.Prelude.Proxy Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Proxy (a ~> b)) (t :: Proxy a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Proxy a) (t :: Proxy b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Proxy a) (t :: Proxy b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Proxy a) (t :: Proxy b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
| SMonoid m => SApplicative (Const m :: Type -> Type) Source # | |
Defined in Data.Singletons.Prelude.Const Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t :: Const m (a ~> b)) (t :: Const m a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Const m a) (t :: Const m b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%*>) :: forall a b (t :: Const m a) (t :: Const m b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source # (%<*) :: forall a b (t :: Const m a) (t :: Const m b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source # | |
(%.) :: forall b c a (t :: (~>) b c) (t :: (~>) a b) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (.@#@$) t) t) t :: c) infixr 9 Source #
data SomeSing k where Source #
An existentially-quantified singleton. This type is useful when you want a singleton type, but there is no way of knowing, at compile-time, what the type index will be. To make use of this type, you will generally have to use a pattern-match:
foo :: Bool -> ...
foo b = case toSing b of
SomeSing sb -> {- fancy dependently-typed code with sb -}An example like the one above may be easier to write using withSomeSing.
Instances
| SBounded k => Bounded (SomeSing k) Source # | |
| SEnum k => Enum (SomeSing k) Source # | |
Defined in Data.Singletons Methods succ :: SomeSing k -> SomeSing k # pred :: SomeSing k -> SomeSing k # fromEnum :: SomeSing k -> Int # enumFrom :: SomeSing k -> [SomeSing k] # enumFromThen :: SomeSing k -> SomeSing k -> [SomeSing k] # enumFromTo :: SomeSing k -> SomeSing k -> [SomeSing k] # enumFromThenTo :: SomeSing k -> SomeSing k -> SomeSing k -> [SomeSing k] # | |
| SEq k => Eq (SomeSing k) Source # | |
| SNum k => Num (SomeSing k) Source # | |
Defined in Data.Singletons | |
| SOrd k => Ord (SomeSing k) Source # | |
| ShowSing k => Show (SomeSing k) Source # | |
| SIsString k => IsString (SomeSing k) Source # | |
Defined in Data.Singletons Methods fromString :: String -> SomeSing k # | |
| SSemigroup k => Semigroup (SomeSing k) Source # | |
| SMonoid k => Monoid (SomeSing k) Source # | |
type family Error str where ... Source #
The promotion of error. This version is more poly-kinded for
easier use.
data ErrorSym0 a6989586621679472252 Source #
Instances
sUndefined :: HasCallStack => a Source #
The singleton for undefined.
type UndefinedSym0 = Undefined :: k Source #
data (==@#@$) a6989586621679370055 infix 4 Source #
Instances
| SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
| SuppressUnusedWarnings ((==@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679370055 :: a) Source # | |
data a6989586621679370055 ==@#@$$ a6989586621679370056 infix 4 Source #
Instances
| (SEq a, SingI x) => SingI ((==@#@$$) x :: TyFun a Bool -> Type) Source # | |
| SuppressUnusedWarnings ((==@#@$$) a6989586621679370055 :: TyFun a Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((==@#@$$) a6989586621679370055 :: TyFun a Bool -> Type) (a6989586621679370056 :: a) Source # | |
type (==@#@$$$) (a6989586621679370055 :: a) (a6989586621679370056 :: a) = (==) a6989586621679370055 a6989586621679370056 :: Bool infix 4 Source #
data (>@#@$) a6989586621679383655 infix 4 Source #
Instances
| SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
| SuppressUnusedWarnings ((>@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((>@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679383655 :: a) Source # | |
data a6989586621679383655 >@#@$$ a6989586621679383656 infix 4 Source #
Instances
| (SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type) Source # | |
| SuppressUnusedWarnings ((>@#@$$) a6989586621679383655 :: TyFun a Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((>@#@$$) a6989586621679383655 :: TyFun a Bool -> Type) (a6989586621679383656 :: a) Source # | |
type (>@#@$$$) (a6989586621679383655 :: a) (a6989586621679383656 :: a) = (>) a6989586621679383655 a6989586621679383656 :: Bool infix 4 Source #
type Tuple0Sym0 = '() :: () Source #
data Tuple2Sym0 a6989586621679304233 Source #
Instances
| SingI (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple2Sym0 Source # | |
| SuppressUnusedWarnings (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) (a6989586621679304233 :: a) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) (a6989586621679304233 :: a) = Tuple2Sym1 a6989586621679304233 :: TyFun b (a, b) -> Type | |
data Tuple2Sym1 a6989586621679304233 a6989586621679304234 Source #
Instances
| SingI d => SingI (Tuple2Sym1 d :: TyFun b (a, b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple2Sym1 d) Source # | |
| SuppressUnusedWarnings (Tuple2Sym1 a6989586621679304233 :: TyFun b (a, b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple2Sym1 a6989586621679304233 :: TyFun b (a, b) -> Type) (a6989586621679304234 :: b) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple2Sym1 a6989586621679304233 :: TyFun b (a, b) -> Type) (a6989586621679304234 :: b) = Tuple2Sym2 a6989586621679304233 a6989586621679304234 | |
type Tuple2Sym2 (a6989586621679304233 :: a) (a6989586621679304234 :: b) = '(a6989586621679304233, a6989586621679304234) :: (a :: Type, b :: Type) Source #
data Tuple3Sym0 a6989586621679304264 Source #
Instances
| SingI (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple3Sym0 Source # | |
| SuppressUnusedWarnings (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) (a6989586621679304264 :: a) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) (a6989586621679304264 :: a) = Tuple3Sym1 a6989586621679304264 :: TyFun b (c ~> (a, b, c)) -> Type | |
data Tuple3Sym1 a6989586621679304264 a6989586621679304265 Source #
Instances
| SingI d => SingI (Tuple3Sym1 d :: TyFun b (c ~> (a, b, c)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple3Sym1 d) Source # | |
| SuppressUnusedWarnings (Tuple3Sym1 a6989586621679304264 :: TyFun b (c ~> (a, b, c)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple3Sym1 a6989586621679304264 :: TyFun b (c ~> (a, b, c)) -> Type) (a6989586621679304265 :: b) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple3Sym1 a6989586621679304264 :: TyFun b (c ~> (a, b, c)) -> Type) (a6989586621679304265 :: b) = Tuple3Sym2 a6989586621679304264 a6989586621679304265 :: TyFun c (a, b, c) -> Type | |
data Tuple3Sym2 a6989586621679304264 a6989586621679304265 a6989586621679304266 Source #
Instances
| (SingI d1, SingI d2) => SingI (Tuple3Sym2 d1 d2 :: TyFun c (a, b, c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple3Sym2 d1 d2) Source # | |
| SuppressUnusedWarnings (Tuple3Sym2 a6989586621679304264 a6989586621679304265 :: TyFun c (a, b, c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple3Sym2 a6989586621679304264 a6989586621679304265 :: TyFun c (a, b, c) -> Type) (a6989586621679304266 :: c) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple3Sym2 a6989586621679304264 a6989586621679304265 :: TyFun c (a, b, c) -> Type) (a6989586621679304266 :: c) = Tuple3Sym3 a6989586621679304264 a6989586621679304265 a6989586621679304266 | |
type Tuple3Sym3 (a6989586621679304264 :: a) (a6989586621679304265 :: b) (a6989586621679304266 :: c) = '(a6989586621679304264, a6989586621679304265, a6989586621679304266) :: (a :: Type, b :: Type, c :: Type) Source #
data Tuple4Sym0 a6989586621679304310 Source #
Instances
| SingI (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple4Sym0 Source # | |
| SuppressUnusedWarnings (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) (a6989586621679304310 :: a) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Tuple4Sym1 a6989586621679304310 a6989586621679304311 Source #
Instances
| SingI d1 => SingI (Tuple4Sym1 d1 :: TyFun b (c ~> (d2 ~> (a, b, c, d2))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple4Sym1 d1) Source # | |
| SuppressUnusedWarnings (Tuple4Sym1 a6989586621679304310 :: TyFun b (c ~> (d ~> (a, b, c, d))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple4Sym1 a6989586621679304310 :: TyFun b (c ~> (d ~> (a, b, c, d))) -> Type) (a6989586621679304311 :: b) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple4Sym1 a6989586621679304310 :: TyFun b (c ~> (d ~> (a, b, c, d))) -> Type) (a6989586621679304311 :: b) = Tuple4Sym2 a6989586621679304310 a6989586621679304311 :: TyFun c (d ~> (a, b, c, d)) -> Type | |
data Tuple4Sym2 a6989586621679304310 a6989586621679304311 a6989586621679304312 Source #
Instances
| (SingI d1, SingI d2) => SingI (Tuple4Sym2 d1 d2 :: TyFun c (d3 ~> (a, b, c, d3)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple4Sym2 d1 d2) Source # | |
| SuppressUnusedWarnings (Tuple4Sym2 a6989586621679304310 a6989586621679304311 :: TyFun c (d ~> (a, b, c, d)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple4Sym2 a6989586621679304310 a6989586621679304311 :: TyFun c (d ~> (a, b, c, d)) -> Type) (a6989586621679304312 :: c) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple4Sym2 a6989586621679304310 a6989586621679304311 :: TyFun c (d ~> (a, b, c, d)) -> Type) (a6989586621679304312 :: c) = Tuple4Sym3 a6989586621679304310 a6989586621679304311 a6989586621679304312 :: TyFun d (a, b, c, d) -> Type | |
data Tuple4Sym3 a6989586621679304310 a6989586621679304311 a6989586621679304312 a6989586621679304313 Source #
Instances
| (SingI d1, SingI d2, SingI d3) => SingI (Tuple4Sym3 d1 d2 d3 :: TyFun d4 (a, b, c, d4) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple4Sym3 d1 d2 d3) Source # | |
| SuppressUnusedWarnings (Tuple4Sym3 a6989586621679304310 a6989586621679304311 a6989586621679304312 :: TyFun d (a, b, c, d) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple4Sym3 a6989586621679304310 a6989586621679304311 a6989586621679304312 :: TyFun d (a, b, c, d) -> Type) (a6989586621679304313 :: d) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple4Sym3 a6989586621679304310 a6989586621679304311 a6989586621679304312 :: TyFun d (a, b, c, d) -> Type) (a6989586621679304313 :: d) = Tuple4Sym4 a6989586621679304310 a6989586621679304311 a6989586621679304312 a6989586621679304313 | |
type Tuple4Sym4 (a6989586621679304310 :: a) (a6989586621679304311 :: b) (a6989586621679304312 :: c) (a6989586621679304313 :: d) = '(a6989586621679304310, a6989586621679304311, a6989586621679304312, a6989586621679304313) :: (a :: Type, b :: Type, c :: Type, d :: Type) Source #
data Tuple5Sym0 a6989586621679304373 Source #
Instances
| SingI (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple5Sym0 Source # | |
| SuppressUnusedWarnings (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) (a6989586621679304373 :: a) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Tuple5Sym1 a6989586621679304373 a6989586621679304374 Source #
Instances
| SingI d1 => SingI (Tuple5Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (a, b, c, d2, e)))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym1 d1) Source # | |
| SuppressUnusedWarnings (Tuple5Sym1 a6989586621679304373 :: TyFun b (c ~> (d ~> (e ~> (a, b, c, d, e)))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple5Sym1 a6989586621679304373 :: TyFun b (c ~> (d ~> (e ~> (a, b, c, d, e)))) -> Type) (a6989586621679304374 :: b) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Tuple5Sym2 a6989586621679304373 a6989586621679304374 a6989586621679304375 Source #
Instances
| (SingI d1, SingI d2) => SingI (Tuple5Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (a, b, c, d3, e))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym2 d1 d2) Source # | |
| SuppressUnusedWarnings (Tuple5Sym2 a6989586621679304373 a6989586621679304374 :: TyFun c (d ~> (e ~> (a, b, c, d, e))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple5Sym2 a6989586621679304373 a6989586621679304374 :: TyFun c (d ~> (e ~> (a, b, c, d, e))) -> Type) (a6989586621679304375 :: c) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple5Sym2 a6989586621679304373 a6989586621679304374 :: TyFun c (d ~> (e ~> (a, b, c, d, e))) -> Type) (a6989586621679304375 :: c) = Tuple5Sym3 a6989586621679304373 a6989586621679304374 a6989586621679304375 :: TyFun d (e ~> (a, b, c, d, e)) -> Type | |
data Tuple5Sym3 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376 Source #
Instances
| (SingI d1, SingI d2, SingI d3) => SingI (Tuple5Sym3 d1 d2 d3 :: TyFun d4 (e ~> (a, b, c, d4, e)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym3 d1 d2 d3) Source # | |
| SuppressUnusedWarnings (Tuple5Sym3 a6989586621679304373 a6989586621679304374 a6989586621679304375 :: TyFun d (e ~> (a, b, c, d, e)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple5Sym3 a6989586621679304373 a6989586621679304374 a6989586621679304375 :: TyFun d (e ~> (a, b, c, d, e)) -> Type) (a6989586621679304376 :: d) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple5Sym3 a6989586621679304373 a6989586621679304374 a6989586621679304375 :: TyFun d (e ~> (a, b, c, d, e)) -> Type) (a6989586621679304376 :: d) = Tuple5Sym4 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376 :: TyFun e (a, b, c, d, e) -> Type | |
data Tuple5Sym4 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376 a6989586621679304377 Source #
Instances
| (SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple5Sym4 d1 d2 d3 d5 :: TyFun e (a, b, c, d4, e) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym4 d1 d2 d3 d5) Source # | |
| SuppressUnusedWarnings (Tuple5Sym4 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376 :: TyFun e (a, b, c, d, e) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple5Sym4 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376 :: TyFun e (a, b, c, d, e) -> Type) (a6989586621679304377 :: e) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple5Sym4 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376 :: TyFun e (a, b, c, d, e) -> Type) (a6989586621679304377 :: e) = Tuple5Sym5 a6989586621679304373 a6989586621679304374 a6989586621679304375 a6989586621679304376 a6989586621679304377 | |
type Tuple5Sym5 (a6989586621679304373 :: a) (a6989586621679304374 :: b) (a6989586621679304375 :: c) (a6989586621679304376 :: d) (a6989586621679304377 :: e) = '(a6989586621679304373, a6989586621679304374, a6989586621679304375, a6989586621679304376, a6989586621679304377) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type) Source #
data Tuple6Sym0 a6989586621679304455 Source #
Instances
| SingI (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple6Sym0 Source # | |
| SuppressUnusedWarnings (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type) (a6989586621679304455 :: a) Source # | |
data Tuple6Sym1 a6989586621679304455 a6989586621679304456 Source #
Instances
| SingI d1 => SingI (Tuple6Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (f ~> (a, b, c, d2, e, f))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym1 d1) Source # | |
| SuppressUnusedWarnings (Tuple6Sym1 a6989586621679304455 :: TyFun b (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple6Sym1 a6989586621679304455 :: TyFun b (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f))))) -> Type) (a6989586621679304456 :: b) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Tuple6Sym2 a6989586621679304455 a6989586621679304456 a6989586621679304457 Source #
Instances
| (SingI d1, SingI d2) => SingI (Tuple6Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (f ~> (a, b, c, d3, e, f)))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym2 d1 d2) Source # | |
| SuppressUnusedWarnings (Tuple6Sym2 a6989586621679304455 a6989586621679304456 :: TyFun c (d ~> (e ~> (f ~> (a, b, c, d, e, f)))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple6Sym2 a6989586621679304455 a6989586621679304456 :: TyFun c (d ~> (e ~> (f ~> (a, b, c, d, e, f)))) -> Type) (a6989586621679304457 :: c) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Tuple6Sym3 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 Source #
Instances
| (SingI d1, SingI d2, SingI d3) => SingI (Tuple6Sym3 d1 d2 d3 :: TyFun d4 (e ~> (f ~> (a, b, c, d4, e, f))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym3 d1 d2 d3) Source # | |
| SuppressUnusedWarnings (Tuple6Sym3 a6989586621679304455 a6989586621679304456 a6989586621679304457 :: TyFun d (e ~> (f ~> (a, b, c, d, e, f))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple6Sym3 a6989586621679304455 a6989586621679304456 a6989586621679304457 :: TyFun d (e ~> (f ~> (a, b, c, d, e, f))) -> Type) (a6989586621679304458 :: d) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple6Sym3 a6989586621679304455 a6989586621679304456 a6989586621679304457 :: TyFun d (e ~> (f ~> (a, b, c, d, e, f))) -> Type) (a6989586621679304458 :: d) = Tuple6Sym4 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 :: TyFun e (f ~> (a, b, c, d, e, f)) -> Type | |
data Tuple6Sym4 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459 Source #
Instances
| (SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple6Sym4 d1 d2 d3 d5 :: TyFun e (f ~> (a, b, c, d4, e, f)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym4 d1 d2 d3 d5) Source # | |
| SuppressUnusedWarnings (Tuple6Sym4 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 :: TyFun e (f ~> (a, b, c, d, e, f)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple6Sym4 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 :: TyFun e (f ~> (a, b, c, d, e, f)) -> Type) (a6989586621679304459 :: e) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple6Sym4 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 :: TyFun e (f ~> (a, b, c, d, e, f)) -> Type) (a6989586621679304459 :: e) = Tuple6Sym5 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459 :: TyFun f (a, b, c, d, e, f) -> Type | |
data Tuple6Sym5 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459 a6989586621679304460 Source #
Instances
| (SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI (Tuple6Sym5 d1 d2 d3 d5 d6 :: TyFun f (a, b, c, d4, e, f) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym5 d1 d2 d3 d5 d6) Source # | |
| SuppressUnusedWarnings (Tuple6Sym5 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459 :: TyFun f (a, b, c, d, e, f) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple6Sym5 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459 :: TyFun f (a, b, c, d, e, f) -> Type) (a6989586621679304460 :: f) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple6Sym5 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459 :: TyFun f (a, b, c, d, e, f) -> Type) (a6989586621679304460 :: f) = Tuple6Sym6 a6989586621679304455 a6989586621679304456 a6989586621679304457 a6989586621679304458 a6989586621679304459 a6989586621679304460 | |
type Tuple6Sym6 (a6989586621679304455 :: a) (a6989586621679304456 :: b) (a6989586621679304457 :: c) (a6989586621679304458 :: d) (a6989586621679304459 :: e) (a6989586621679304460 :: f) = '(a6989586621679304455, a6989586621679304456, a6989586621679304457, a6989586621679304458, a6989586621679304459, a6989586621679304460) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type) Source #
data Tuple7Sym0 a6989586621679304558 Source #
Instances
| SingI (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple7Sym0 Source # | |
| SuppressUnusedWarnings (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type) (a6989586621679304558 :: a) Source # | |
data Tuple7Sym1 a6989586621679304558 a6989586621679304559 Source #
Instances
| SingI d1 => SingI (Tuple7Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (f ~> (g ~> (a, b, c, d2, e, f, g)))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym1 d1) Source # | |
| SuppressUnusedWarnings (Tuple7Sym1 a6989586621679304558 :: TyFun b (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple7Sym1 a6989586621679304558 :: TyFun b (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))))) -> Type) (a6989586621679304559 :: b) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Tuple7Sym2 a6989586621679304558 a6989586621679304559 a6989586621679304560 Source #
Instances
| (SingI d1, SingI d2) => SingI (Tuple7Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (f ~> (g ~> (a, b, c, d3, e, f, g))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym2 d1 d2) Source # | |
| SuppressUnusedWarnings (Tuple7Sym2 a6989586621679304558 a6989586621679304559 :: TyFun c (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple7Sym2 a6989586621679304558 a6989586621679304559 :: TyFun c (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))) -> Type) (a6989586621679304560 :: c) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple7Sym2 a6989586621679304558 a6989586621679304559 :: TyFun c (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))) -> Type) (a6989586621679304560 :: c) = Tuple7Sym3 a6989586621679304558 a6989586621679304559 a6989586621679304560 :: TyFun d (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))) -> Type | |
data Tuple7Sym3 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 Source #
Instances
| (SingI d1, SingI d2, SingI d3) => SingI (Tuple7Sym3 d1 d2 d3 :: TyFun d4 (e ~> (f ~> (g ~> (a, b, c, d4, e, f, g)))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym3 d1 d2 d3) Source # | |
| SuppressUnusedWarnings (Tuple7Sym3 a6989586621679304558 a6989586621679304559 a6989586621679304560 :: TyFun d (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple7Sym3 a6989586621679304558 a6989586621679304559 a6989586621679304560 :: TyFun d (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))) -> Type) (a6989586621679304561 :: d) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple7Sym3 a6989586621679304558 a6989586621679304559 a6989586621679304560 :: TyFun d (e ~> (f ~> (g ~> (a, b, c, d, e, f, g)))) -> Type) (a6989586621679304561 :: d) = Tuple7Sym4 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 :: TyFun e (f ~> (g ~> (a, b, c, d, e, f, g))) -> Type | |
data Tuple7Sym4 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 Source #
Instances
| (SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple7Sym4 d1 d2 d3 d5 :: TyFun e (f ~> (g ~> (a, b, c, d4, e, f, g))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym4 d1 d2 d3 d5) Source # | |
| SuppressUnusedWarnings (Tuple7Sym4 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 :: TyFun e (f ~> (g ~> (a, b, c, d, e, f, g))) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple7Sym4 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 :: TyFun e (f ~> (g ~> (a, b, c, d, e, f, g))) -> Type) (a6989586621679304562 :: e) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple7Sym4 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 :: TyFun e (f ~> (g ~> (a, b, c, d, e, f, g))) -> Type) (a6989586621679304562 :: e) = Tuple7Sym5 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 :: TyFun f (g ~> (a, b, c, d, e, f, g)) -> Type | |
data Tuple7Sym5 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563 Source #
Instances
| (SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI (Tuple7Sym5 d1 d2 d3 d5 d6 :: TyFun f (g ~> (a, b, c, d4, e, f, g)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym5 d1 d2 d3 d5 d6) Source # | |
| SuppressUnusedWarnings (Tuple7Sym5 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 :: TyFun f (g ~> (a, b, c, d, e, f, g)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple7Sym5 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 :: TyFun f (g ~> (a, b, c, d, e, f, g)) -> Type) (a6989586621679304563 :: f) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple7Sym5 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 :: TyFun f (g ~> (a, b, c, d, e, f, g)) -> Type) (a6989586621679304563 :: f) = Tuple7Sym6 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563 :: TyFun g (a, b, c, d, e, f, g) -> Type | |
data Tuple7Sym6 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563 a6989586621679304564 Source #
Instances
| (SingI d1, SingI d2, SingI d3, SingI d5, SingI d6, SingI d7) => SingI (Tuple7Sym6 d1 d2 d3 d5 d6 d7 :: TyFun g (a, b, c, d4, e, f, g) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym6 d1 d2 d3 d5 d6 d7) Source # | |
| SuppressUnusedWarnings (Tuple7Sym6 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563 :: TyFun g (a, b, c, d, e, f, g) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply (Tuple7Sym6 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563 :: TyFun g (a, b, c, d, e, f, g) -> Type) (a6989586621679304564 :: g) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (Tuple7Sym6 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563 :: TyFun g (a, b, c, d, e, f, g) -> Type) (a6989586621679304564 :: g) = Tuple7Sym7 a6989586621679304558 a6989586621679304559 a6989586621679304560 a6989586621679304561 a6989586621679304562 a6989586621679304563 a6989586621679304564 | |
type Tuple7Sym7 (a6989586621679304558 :: a) (a6989586621679304559 :: b) (a6989586621679304560 :: c) (a6989586621679304561 :: d) (a6989586621679304562 :: e) (a6989586621679304563 :: f) (a6989586621679304564 :: g) = '(a6989586621679304558, a6989586621679304559, a6989586621679304560, a6989586621679304561, a6989586621679304562, a6989586621679304563, a6989586621679304564) :: (a :: Type, b :: Type, c :: Type, d :: Type, e :: Type, f :: Type, g :: Type) Source #
data CompareSym0 a6989586621679383640 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 a (a ~> Ordering) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
| type Apply (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) (a6989586621679383640 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) (a6989586621679383640 :: a) = CompareSym1 a6989586621679383640 | |
data CompareSym1 a6989586621679383640 a6989586621679383641 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 a6989586621679383640 :: TyFun a Ordering -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
| type Apply (CompareSym1 a6989586621679383640 :: TyFun a Ordering -> Type) (a6989586621679383641 :: a) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym1 a6989586621679383640 :: TyFun a Ordering -> Type) (a6989586621679383641 :: a) = CompareSym2 a6989586621679383640 a6989586621679383641 | |
type CompareSym2 (a6989586621679383640 :: a) (a6989586621679383641 :: a) = Compare a6989586621679383640 a6989586621679383641 :: Ordering Source #
data ThenCmpSym0 a6989586621679394586 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 (a6989586621679394586 :: Ordering) Source # | |
Defined in Data.Singletons.Prelude.Ord | |
data ThenCmpSym1 a6989586621679394586 a6989586621679394587 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 a6989586621679394586 :: TyFun Ordering Ordering -> Type) Source # | |
Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source # | |
| type Apply (ThenCmpSym1 a6989586621679394586 :: TyFun Ordering Ordering -> Type) (a6989586621679394587 :: Ordering) Source # | |
Defined in Data.Singletons.Prelude.Ord type Apply (ThenCmpSym1 a6989586621679394586 :: TyFun Ordering Ordering -> Type) (a6989586621679394587 :: Ordering) = ThenCmpSym2 a6989586621679394586 a6989586621679394587 | |
type ThenCmpSym2 (a6989586621679394586 :: Ordering) (a6989586621679394587 :: Ordering) = ThenCmp a6989586621679394586 a6989586621679394587 :: Ordering Source #
data FoldlSym0 a6989586621680492465 Source #
Instances
| SFoldable t => SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) Source # | |
| SuppressUnusedWarnings (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) (a6989586621680492465 :: b ~> (a ~> b)) Source # | |
data FoldlSym1 a6989586621680492465 a6989586621680492466 Source #
Instances
| (SFoldable t, SingI d) => SingI (FoldlSym1 d :: TyFun b (t a ~> b) -> Type) Source # | |
| SuppressUnusedWarnings (FoldlSym1 a6989586621680492465 :: TyFun b (t a ~> b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FoldlSym1 a6989586621680492465 :: TyFun b (t a ~> b) -> Type) (a6989586621680492466 :: b) Source # | |
data FoldlSym2 a6989586621680492465 a6989586621680492466 a6989586621680492467 Source #
Instances
| (SFoldable t, SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 :: TyFun (t a) b -> Type) Source # | |
| SuppressUnusedWarnings (FoldlSym2 a6989586621680492465 a6989586621680492466 :: TyFun (t a) b -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FoldlSym2 a6989586621680492465 a6989586621680492466 :: TyFun (t a) b -> Type) (a6989586621680492467 :: t a) Source # | |
type FoldlSym3 (a6989586621680492465 :: (~>) b ((~>) a b)) (a6989586621680492466 :: b) (a6989586621680492467 :: t a) = Foldl a6989586621680492465 a6989586621680492466 a6989586621680492467 :: b Source #
type MinBoundSym0 = MinBound :: a Source #
type MaxBoundSym0 = MaxBound :: a Source #
data ShowsPrecSym0 a6989586621680279568 Source #
Instances
| SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 Source # | |
| SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680279568 :: Nat) Source # | |
data ShowsPrecSym1 a6989586621680279568 a6989586621680279569 Source #
Instances
| (SShow a, SingI d) => SingI (ShowsPrecSym1 d :: TyFun a (Symbol ~> Symbol) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym1 d) Source # | |
| SuppressUnusedWarnings (ShowsPrecSym1 a6989586621680279568 :: TyFun a (Symbol ~> Symbol) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply (ShowsPrecSym1 a6989586621680279568 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680279569 :: a) Source # | |
Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym1 a6989586621680279568 :: TyFun a (Symbol ~> Symbol) -> Type) (a6989586621680279569 :: a) = ShowsPrecSym2 a6989586621680279568 a6989586621680279569 | |
data ShowsPrecSym2 a6989586621680279568 a6989586621680279569 a6989586621680279570 Source #
Instances
| (SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym2 d1 d2) Source # | |
| SuppressUnusedWarnings (ShowsPrecSym2 a6989586621680279568 a6989586621680279569 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply (ShowsPrecSym2 a6989586621680279568 a6989586621680279569 :: TyFun Symbol Symbol -> Type) (a6989586621680279570 :: Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym2 a6989586621680279568 a6989586621680279569 :: TyFun Symbol Symbol -> Type) (a6989586621680279570 :: Symbol) = ShowsPrecSym3 a6989586621680279568 a6989586621680279569 a6989586621680279570 | |
type ShowsPrecSym3 (a6989586621680279568 :: Nat) (a6989586621680279569 :: a) (a6989586621680279570 :: Symbol) = ShowsPrec a6989586621680279568 a6989586621680279569 a6989586621680279570 :: Symbol Source #
data ShowStringSym0 a6989586621680279523 Source #
Instances
| SingI ShowStringSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods | |
| SuppressUnusedWarnings ShowStringSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply ShowStringSym0 (a6989586621680279523 :: Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show | |
data ShowStringSym1 a6989586621680279523 a6989586621680279524 Source #
Instances
| SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowStringSym1 d) Source # | |
| SuppressUnusedWarnings (ShowStringSym1 a6989586621680279523 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply (ShowStringSym1 a6989586621680279523 :: TyFun Symbol Symbol -> Type) (a6989586621680279524 :: Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show type Apply (ShowStringSym1 a6989586621680279523 :: TyFun Symbol Symbol -> Type) (a6989586621680279524 :: Symbol) = ShowStringSym2 a6989586621680279523 a6989586621680279524 | |
type ShowStringSym2 (a6989586621680279523 :: Symbol) (a6989586621680279524 :: Symbol) = ShowString a6989586621680279523 a6989586621680279524 :: Symbol Source #
data ShowParenSym0 a6989586621680279507 Source #
Instances
| SingI ShowParenSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowParenSym0 Source # | |
| SuppressUnusedWarnings ShowParenSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply ShowParenSym0 (a6989586621680279507 :: Bool) Source # | |
Defined in Data.Singletons.Prelude.Show | |
data ShowParenSym1 a6989586621680279507 a6989586621680279508 Source #
Instances
| SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym1 d) Source # | |
| SuppressUnusedWarnings (ShowParenSym1 a6989586621680279507 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply (ShowParenSym1 a6989586621680279507 :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) (a6989586621680279508 :: Symbol ~> Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show | |
data ShowParenSym2 a6989586621680279507 a6989586621680279508 a6989586621680279509 Source #
Instances
| (SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym2 d1 d2) Source # | |
| SuppressUnusedWarnings (ShowParenSym2 a6989586621680279507 a6989586621680279508 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply (ShowParenSym2 a6989586621680279507 a6989586621680279508 :: TyFun Symbol Symbol -> Type) (a6989586621680279509 :: Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show | |
data ShowSpaceSym0 a6989586621680279495 Source #
Instances
| SingI ShowSpaceSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowSpaceSym0 Source # | |
| SuppressUnusedWarnings ShowSpaceSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply ShowSpaceSym0 (a6989586621680279495 :: Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show | |
type ShowSpaceSym1 (a6989586621680279495 :: Symbol) = ShowSpace a6989586621680279495 :: Symbol Source #
data ShowCharSym0 a6989586621680279534 Source #
Instances
| SingI ShowCharSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCharSym0 Source # | |
| SuppressUnusedWarnings ShowCharSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply ShowCharSym0 (a6989586621680279534 :: Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show | |
data ShowCharSym1 a6989586621680279534 a6989586621680279535 Source #
Instances
| SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowCharSym1 d) Source # | |
| SuppressUnusedWarnings (ShowCharSym1 a6989586621680279534 :: TyFun Symbol Symbol -> Type) Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply (ShowCharSym1 a6989586621680279534 :: TyFun Symbol Symbol -> Type) (a6989586621680279535 :: Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show type Apply (ShowCharSym1 a6989586621680279534 :: TyFun Symbol Symbol -> Type) (a6989586621680279535 :: Symbol) = ShowCharSym2 a6989586621680279534 a6989586621680279535 | |
type ShowCharSym2 (a6989586621680279534 :: Symbol) (a6989586621680279535 :: Symbol) = ShowChar a6989586621680279534 a6989586621680279535 :: Symbol Source #
data ShowCommaSpaceSym0 a6989586621680279489 Source #
Instances
| SingI ShowCommaSpaceSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods | |
| SuppressUnusedWarnings ShowCommaSpaceSym0 Source # | |
Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () Source # | |
| type Apply ShowCommaSpaceSym0 (a6989586621680279489 :: Symbol) Source # | |
Defined in Data.Singletons.Prelude.Show type Apply ShowCommaSpaceSym0 (a6989586621680279489 :: Symbol) = ShowCommaSpaceSym1 a6989586621680279489 | |
type ShowCommaSpaceSym1 (a6989586621680279489 :: Symbol) = ShowCommaSpace a6989586621680279489 :: Symbol Source #
data FmapSym0 a6989586621679559667 Source #
Instances
| SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) Source # | |
| SuppressUnusedWarnings (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679559667 :: a ~> b) Source # | |
data FmapSym1 a6989586621679559667 a6989586621679559668 Source #
Instances
| (SFunctor f, SingI d) => SingI (FmapSym1 d :: TyFun (f a) (f b) -> Type) Source # | |
| SuppressUnusedWarnings (FmapSym1 a6989586621679559667 :: TyFun (f a) (f b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FmapSym1 a6989586621679559667 :: TyFun (f a) (f b) -> Type) (a6989586621679559668 :: f a) Source # | |
type FmapSym2 (a6989586621679559667 :: (~>) a b) (a6989586621679559668 :: f a) = Fmap a6989586621679559667 a6989586621679559668 :: f b Source #
data (<$@#@$) a6989586621679559672 infixl 4 Source #
Instances
| SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) Source # | |
| SuppressUnusedWarnings ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) (a6989586621679559672 :: a) Source # | |
data a6989586621679559672 <$@#@$$ a6989586621679559673 infixl 4 Source #
Instances
| (SFunctor f, SingI d) => SingI ((<$@#@$$) d :: TyFun (f b) (f a) -> Type) Source # | |
| SuppressUnusedWarnings ((<$@#@$$) a6989586621679559672 :: TyFun (f b) (f a) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((<$@#@$$) a6989586621679559672 :: TyFun (f b) (f a) -> Type) (a6989586621679559673 :: f b) Source # | |
type (<$@#@$$$) (a6989586621679559672 :: a) (a6989586621679559673 :: f b) = (<$) a6989586621679559672 a6989586621679559673 :: f a infixl 4 Source #
data FoldMapSym0 a6989586621680492445 Source #
Instances
| (SFoldable t, SMonoid m) => SingI (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldMapSym0 Source # | |
| SuppressUnusedWarnings (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) (a6989586621680492445 :: a ~> m) Source # | |
Defined in Data.Singletons.Prelude.Foldable type Apply (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) (a6989586621680492445 :: a ~> m) = FoldMapSym1 a6989586621680492445 :: TyFun (t a) m -> Type | |
data FoldMapSym1 a6989586621680492445 a6989586621680492446 Source #
Instances
| (SFoldable t, SMonoid m, SingI d) => SingI (FoldMapSym1 d :: TyFun (t a) m -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldMapSym1 d) Source # | |
| SuppressUnusedWarnings (FoldMapSym1 a6989586621680492445 :: TyFun (t a) m -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FoldMapSym1 a6989586621680492445 :: TyFun (t a) m -> Type) (a6989586621680492446 :: t a) Source # | |
Defined in Data.Singletons.Prelude.Foldable type Apply (FoldMapSym1 a6989586621680492445 :: TyFun (t a) m -> Type) (a6989586621680492446 :: t a) = FoldMapSym2 a6989586621680492445 a6989586621680492446 | |
type FoldMapSym2 (a6989586621680492445 :: (~>) a m) (a6989586621680492446 :: t a) = FoldMap a6989586621680492445 a6989586621680492446 :: m Source #
type MemptySym0 = Mempty :: a Source #
data MappendSym0 a6989586621680347244 Source #
Instances
| SMonoid a => SingI (MappendSym0 :: TyFun a (a ~> a) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing MappendSym0 Source # | |
| SuppressUnusedWarnings (MappendSym0 :: TyFun a (a ~> a) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monoid Methods suppressUnusedWarnings :: () Source # | |
| type Apply (MappendSym0 :: TyFun a (a ~> a) -> Type) (a6989586621680347244 :: a) Source # | |
Defined in Data.Singletons.Prelude.Monoid type Apply (MappendSym0 :: TyFun a (a ~> a) -> Type) (a6989586621680347244 :: a) = MappendSym1 a6989586621680347244 | |
data MappendSym1 a6989586621680347244 a6989586621680347245 Source #
Instances
| (SMonoid a, SingI d) => SingI (MappendSym1 d :: TyFun a a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing (MappendSym1 d) Source # | |
| SuppressUnusedWarnings (MappendSym1 a6989586621680347244 :: TyFun a a -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monoid Methods suppressUnusedWarnings :: () Source # | |
| type Apply (MappendSym1 a6989586621680347244 :: TyFun a a -> Type) (a6989586621680347245 :: a) Source # | |
Defined in Data.Singletons.Prelude.Monoid type Apply (MappendSym1 a6989586621680347244 :: TyFun a a -> Type) (a6989586621680347245 :: a) = MappendSym2 a6989586621680347244 a6989586621680347245 | |
type MappendSym2 (a6989586621680347244 :: a) (a6989586621680347245 :: a) = Mappend a6989586621680347244 a6989586621680347245 :: a Source #
data FoldrSym0 a6989586621680492451 Source #
Instances
| SFoldable t => SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) Source # | |
| SuppressUnusedWarnings (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) (a6989586621680492451 :: a ~> (b ~> b)) Source # | |
data FoldrSym1 a6989586621680492451 a6989586621680492452 Source #
Instances
| (SFoldable t, SingI d) => SingI (FoldrSym1 d :: TyFun b (t a ~> b) -> Type) Source # | |
| SuppressUnusedWarnings (FoldrSym1 a6989586621680492451 :: TyFun b (t a ~> b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FoldrSym1 a6989586621680492451 :: TyFun b (t a ~> b) -> Type) (a6989586621680492452 :: b) Source # | |
data FoldrSym2 a6989586621680492451 a6989586621680492452 a6989586621680492453 Source #
Instances
| (SFoldable t, SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun (t a) b -> Type) Source # | |
| SuppressUnusedWarnings (FoldrSym2 a6989586621680492451 a6989586621680492452 :: TyFun (t a) b -> Type) Source # | |
Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (FoldrSym2 a6989586621680492451 a6989586621680492452 :: TyFun (t a) b -> Type) (a6989586621680492453 :: t a) Source # | |
type FoldrSym3 (a6989586621680492451 :: (~>) a ((~>) b b)) (a6989586621680492452 :: b) (a6989586621680492453 :: t a) = Foldr a6989586621680492451 a6989586621680492452 a6989586621680492453 :: b Source #
data TraverseSym0 a6989586621680816742 Source #
Instances
| (STraversable t, SApplicative f) => SingI (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing TraverseSym0 Source # | |
| SuppressUnusedWarnings (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Traversable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type) (a6989586621680816742 :: a ~> f b) Source # | |
Defined in Data.Singletons.Prelude.Traversable type Apply (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type) (a6989586621680816742 :: a ~> f b) = TraverseSym1 a6989586621680816742 :: TyFun (t a) (f (t b)) -> Type | |
data TraverseSym1 a6989586621680816742 a6989586621680816743 Source #
Instances
| (STraversable t, SApplicative f, SingI d) => SingI (TraverseSym1 d :: TyFun (t a) (f (t b)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (TraverseSym1 d) Source # | |
| SuppressUnusedWarnings (TraverseSym1 a6989586621680816742 :: TyFun (t a) (f (t b)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Traversable Methods suppressUnusedWarnings :: () Source # | |
| type Apply (TraverseSym1 a6989586621680816742 :: TyFun (t a) (f (t b)) -> Type) (a6989586621680816743 :: t a) Source # | |
Defined in Data.Singletons.Prelude.Traversable type Apply (TraverseSym1 a6989586621680816742 :: TyFun (t a) (f (t b)) -> Type) (a6989586621680816743 :: t a) = TraverseSym2 a6989586621680816742 a6989586621680816743 | |
type TraverseSym2 (a6989586621680816742 :: (~>) a (f b)) (a6989586621680816743 :: t a) = Traverse a6989586621680816742 a6989586621680816743 :: f (t b) Source #
data PureSym0 a6989586621679559691 Source #
Instances
| SApplicative f => SingI (PureSym0 :: TyFun a (f a) -> Type) Source # | |
| SuppressUnusedWarnings (PureSym0 :: TyFun a (f a) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply (PureSym0 :: TyFun a (f a) -> Type) (a6989586621679559691 :: a) Source # | |
data (<*>@#@$) a6989586621679559695 infixl 4 Source #
Instances
| SApplicative f => SingI ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type) Source # | |
| SuppressUnusedWarnings ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type) (a6989586621679559695 :: f (a ~> b)) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
data a6989586621679559695 <*>@#@$$ a6989586621679559696 infixl 4 Source #
Instances
| (SApplicative f, SingI d) => SingI ((<*>@#@$$) d :: TyFun (f a) (f b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((<*>@#@$$) d) Source # | |
| SuppressUnusedWarnings ((<*>@#@$$) a6989586621679559695 :: TyFun (f a) (f b) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((<*>@#@$$) a6989586621679559695 :: TyFun (f a) (f b) -> Type) (a6989586621679559696 :: f a) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<*>@#@$$) a6989586621679559695 :: TyFun (f a) (f b) -> Type) (a6989586621679559696 :: f a) = a6989586621679559695 <*>@#@$$$ a6989586621679559696 | |
type (<*>@#@$$$) (a6989586621679559695 :: f ((~>) a b)) (a6989586621679559696 :: f a) = (<*>) a6989586621679559695 a6989586621679559696 :: f b infixl 4 Source #
data LiftA2Sym0 a6989586621679559701 Source #
Instances
| SApplicative f => SingI (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftA2Sym0 Source # | |
| SuppressUnusedWarnings (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type) (a6989586621679559701 :: a ~> (b ~> c)) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal | |
data LiftA2Sym1 a6989586621679559701 a6989586621679559702 Source #
Instances
| (SApplicative f, SingI d) => SingI (LiftA2Sym1 d :: TyFun (f a) (f b ~> f c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA2Sym1 d) Source # | |
| SuppressUnusedWarnings (LiftA2Sym1 a6989586621679559701 :: TyFun (f a) (f b ~> f c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply (LiftA2Sym1 a6989586621679559701 :: TyFun (f a) (f b ~> f c) -> Type) (a6989586621679559702 :: f a) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA2Sym1 a6989586621679559701 :: TyFun (f a) (f b ~> f c) -> Type) (a6989586621679559702 :: f a) = LiftA2Sym2 a6989586621679559701 a6989586621679559702 | |
data LiftA2Sym2 a6989586621679559701 a6989586621679559702 a6989586621679559703 Source #
Instances
| (SApplicative f, SingI d1, SingI d2) => SingI (LiftA2Sym2 d1 d2 :: TyFun (f b) (f c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA2Sym2 d1 d2) Source # | |
| SuppressUnusedWarnings (LiftA2Sym2 a6989586621679559701 a6989586621679559702 :: TyFun (f b) (f c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
| type Apply (LiftA2Sym2 a6989586621679559701 a6989586621679559702 :: TyFun (f b) (f c) -> Type) (a6989586621679559703 :: f b) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA2Sym2 a6989586621679559701 a6989586621679559702 :: TyFun (f b) (f c) -> Type) (a6989586621679559703 :: f b) = LiftA2Sym3 a6989586621679559701 a6989586621679559702 a6989586621679559703 | |
type LiftA2Sym3 (a6989586621679559701 :: (~>) a ((~>) b c)) (a6989586621679559702 :: f a) (a6989586621679559703 :: f b) = LiftA2 a6989586621679559701 a6989586621679559702 a6989586621679559703 :: f c Source #
data (.@#@$) a6989586621679534187 infixr 9 Source #
Instances
| SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) Source # | |
| SuppressUnusedWarnings ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Base Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (a6989586621679534187 :: b ~> c) Source # | |
data a6989586621679534187 .@#@$$ a6989586621679534188 infixr 9 Source #
Instances
| SingI d => SingI ((.@#@$$) d :: TyFun (a ~> b) (a ~> c) -> Type) Source # | |
| SuppressUnusedWarnings ((.@#@$$) a6989586621679534187 :: TyFun (a ~> b) (a ~> c) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Base Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((.@#@$$) a6989586621679534187 :: TyFun (a ~> b) (a ~> c) -> Type) (a6989586621679534188 :: a ~> b) Source # | |
data (a6989586621679534187 .@#@$$$ a6989586621679534188) a6989586621679534189 infixr 9 Source #
Instances
| (SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type) Source # | |
| SuppressUnusedWarnings (a6989586621679534187 .@#@$$$ a6989586621679534188 :: TyFun a c -> Type) Source # | |
Defined in Data.Singletons.Prelude.Base Methods suppressUnusedWarnings :: () Source # | |
| type Apply (a6989586621679534187 .@#@$$$ a6989586621679534188 :: TyFun a c -> Type) (a6989586621679534189 :: a) Source # | |
type (.@#@$$$$) (a6989586621679534187 :: (~>) b c) (a6989586621679534188 :: (~>) a b) (a6989586621679534189 :: a) = (.) a6989586621679534187 a6989586621679534188 a6989586621679534189 :: c infixr 9 Source #
data (:@#@$) a6989586621679304138 infixr 5 Source #
Instances
| SingI ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) Source # | |
| SuppressUnusedWarnings ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) (a6989586621679304138 :: a) Source # | |
data a6989586621679304138 :@#@$$ a6989586621679304139 infixr 5 Source #
Instances
| SingI d => SingI ((:@#@$$) d :: TyFun [a] [a] -> Type) Source # | |
| SuppressUnusedWarnings ((:@#@$$) a6989586621679304138 :: TyFun [a] [a] -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source # | |
| type Apply ((:@#@$$) a6989586621679304138 :: TyFun [a] [a] -> Type) (a6989586621679304139 :: [a]) Source # | |
type (:@#@$$$) (a6989586621679304138 :: a) (a6989586621679304139 :: [a]) = '(:) a6989586621679304138 a6989586621679304139 :: [a :: Type] infixr 5 Source #
class SuppressUnusedWarnings t where Source #
This class (which users should never see) is to be instantiated in order to use an otherwise-unused data constructor, such as the "kind-inference" data constructor for defunctionalization symbols.
Methods
suppressUnusedWarnings :: () Source #