Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude

Contents

Basic singleton definitions
Singleton types
Functions working with Bool
Error reporting
Singleton equality
Singleton comparisons
Singleton Enum and Bounded
Singletons numbers
Singleton Show
Singleton Semigroup and Monoid
Singleton Functor, Applicative, Monad, and MonadFail
Singleton Foldable and Traversable
- Miscellaneous functions
List operations
Other datatypes
Other functions
Defunctionalization symbols

Description

Mimics the Haskell Prelude, but with singleton types. Includes the basic singleton definitions. Note: This is currently very incomplete!

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

module Data.Singletons
data SBool z where
- SFalse :: SBool ('False :: Bool)
- STrue :: SBool ('True :: Bool)
data SList z where
- SNil :: forall (a :: Type). SList ('[] :: [a :: Type])
- SCons :: forall (a :: Type) (n :: a) (n :: [a]). (Sing n) -> (Sing n) -> SList ('(:) n n :: [a :: Type])
data SMaybe z where
- SNothing :: forall (a :: Type). SMaybe ('Nothing :: Maybe (a :: Type))
- SJust :: forall (a :: Type) (n :: a). (Sing n) -> SMaybe ('Just n :: Maybe (a :: Type))
data SEither z where
- SLeft :: forall (a :: Type) (b :: Type) (n :: a). (Sing n) -> SEither ('Left n :: Either (a :: Type) (b :: Type))
- SRight :: forall (a :: Type) (b :: Type) (n :: b). (Sing n) -> SEither ('Right n :: Either (a :: Type) (b :: Type))
data SOrdering z where
- SLT :: SOrdering ('LT :: Ordering)
- SEQ :: SOrdering ('EQ :: Ordering)
- SGT :: SOrdering ('GT :: Ordering)
data STuple0 z where
- STuple0 :: STuple0 ('() :: ())
data STuple2 z where
- STuple2 :: forall (a :: Type) (b :: Type) (n :: a) (n :: b). (Sing n) -> (Sing n) -> STuple2 ('(n, n) :: (a :: Type, b :: Type))
data STuple3 z where
- 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))
data STuple4 z where
- 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))
data STuple5 z where
- 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))
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))
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 Not (a :: Bool) = (res :: Bool) | res -> a where ...
sNot :: Sing a -> Sing (Not a)
type family (a :: Bool) && (b :: Bool) :: Bool where ...
type family (a :: Bool) || (b :: Bool) :: Bool where ...
(%&&) :: Sing a -> Sing b -> Sing (a && b)
(%||) :: Sing a -> Sing b -> Sing (a || b)
type family Otherwise where ...
sOtherwise :: Sing (OtherwiseSym0 :: Bool)
type family Error str where ...
sError :: HasCallStack => Sing (str :: Symbol) -> a
type family ErrorWithoutStackTrace str where ...
sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a
type family Undefined where ...
sUndefined :: HasCallStack => a
module Data.Singletons.Prelude.Eq
class POrd a where
- type Compare (arg :: a) (arg :: a) :: Ordering
- type (arg :: a) < (arg :: a) :: Bool
- type (arg :: a) <= (arg :: a) :: Bool
- type (arg :: a) > (arg :: a) :: Bool
- type (arg :: a) >= (arg :: a) :: Bool
- type Max (arg :: a) (arg :: a) :: a
- type Min (arg :: a) (arg :: a) :: a
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)
class SBounded a where
- sMinBound :: Sing (MinBoundSym0 :: a)
- sMaxBound :: Sing (MaxBoundSym0 :: a)
class PBounded a where
- type MinBound :: a
- type MaxBound :: a
type MaxBoundSym0 = MaxBound :: a
type MinBoundSym0 = MinBound :: a
class SEnum a where
- sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t :: a)
- sFromEnum :: forall (t :: a). Sing t -> Sing (Apply FromEnumSym0 t :: Nat)
- sEnumFromTo :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a])
- sEnumFromThenTo :: forall (t :: a) (t :: a) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a])
class PEnum a where
- type ToEnum (arg :: Nat) :: a
- type FromEnum (arg :: a) :: Nat
- type EnumFromTo (arg :: a) (arg :: a) :: [a]
- type EnumFromThenTo (arg :: a) (arg :: a) (arg :: a) :: [a]
type EnumFromThenToSym3 (a6989586621679758488 :: a) (a6989586621679758489 :: a) (a6989586621679758490 :: a) = EnumFromThenTo a6989586621679758488 a6989586621679758489 a6989586621679758490 :: [a]
data EnumFromThenToSym2 a6989586621679758488 a6989586621679758489 a6989586621679758490
data EnumFromThenToSym1 a6989586621679758488 a6989586621679758489
data EnumFromThenToSym0 a6989586621679758488
type EnumFromToSym2 (a6989586621679758482 :: a) (a6989586621679758483 :: a) = EnumFromTo a6989586621679758482 a6989586621679758483 :: [a]
data EnumFromToSym1 a6989586621679758482 a6989586621679758483
data EnumFromToSym0 a6989586621679758482
type FromEnumSym1 (a6989586621679758478 :: a) = FromEnum a6989586621679758478 :: Nat
data FromEnumSym0 a6989586621679758478
type ToEnumSym1 (a6989586621679758475 :: Nat) = ToEnum a6989586621679758475 :: a
data ToEnumSym0 a6989586621679758475
module Data.Singletons.Prelude.Num
type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
(%^) :: Sing a -> Sing b -> Sing (a ^ b)
class PShow a where
- type ShowsPrec (arg :: Nat) (arg :: a) (arg :: Symbol) :: Symbol
- type Show_ (arg :: a) :: Symbol
- type ShowList (arg :: [a]) (arg :: Symbol) :: Symbol
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 ShowS = String -> String
type SChar = Symbol
type family Shows a a where ...
sShows :: forall a (t :: a) (t :: Symbol). SShow a => Sing t -> Sing t -> Sing (Apply (Apply ShowsSym0 t) 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 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)
class PSemigroup a where
- type (arg :: a) <> (arg :: a) :: a
class SSemigroup a where
- (%<>) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t :: a)
class PMonoid a where
- type Mempty :: a
- type Mappend (arg :: a) (arg :: a) :: a
- type Mconcat (arg :: [a]) :: a
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 PFunctor f where
- type Fmap (arg :: (~>) a b) (arg :: f a) :: f b
- type (arg :: a) <$ (arg :: f b) :: f a
class SFunctor f where
- sFmap :: forall a b (t :: (~>) a b) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t :: f b)
- (%<$) :: forall a b (t :: a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a)
type family a <$> a where ...
(%<$>) :: forall a b f (t :: (~>) a b) (t :: f a). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<$>@#@$) t) t :: f b)
class PApplicative f where
- type Pure (arg :: a) :: f a
- type (arg :: f ((~>) a b)) <*> (arg :: f a) :: f b
- type (arg :: f a) *> (arg :: f b) :: f b
- type (arg :: f a) <* (arg :: f b) :: f a
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)
- (%*>) :: 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)
class PMonad m where
- type (arg :: m a) >>= (arg :: (~>) a (m b)) :: m b
- type (arg :: m a) >> (arg :: m b) :: m b
- type Return (arg :: a) :: m a
class SApplicative m => SMonad m where
- (%>>=) :: forall a b (t :: m a) (t :: (~>) a (m b)). Sing t -> Sing t -> Sing (Apply (Apply (>>=@#@$) t) t :: m b)
- (%>>) :: forall a b (t :: m a) (t :: m b). Sing t -> Sing t -> Sing (Apply (Apply (>>@#@$) t) t :: m b)
- sReturn :: forall a (t :: a). Sing t -> Sing (Apply ReturnSym0 t :: m a)
class PMonadFail m where
- type Fail (arg :: [Char]) :: m a
class SMonad m => SMonadFail m where
- sFail :: forall a (t :: [Char]). Sing t -> Sing (Apply FailSym0 t :: m a)
type family MapM_ a a where ...
sMapM_ :: forall a m b t (t :: (~>) a (m b)) (t :: t a). (SFoldable t, SMonad m) => Sing t -> Sing t -> Sing (Apply (Apply MapM_Sym0 t) t :: m ())
type family Sequence_ a where ...
sSequence_ :: forall t m a (t :: t (m a)). (SFoldable t, SMonad m) => Sing t -> Sing (Apply Sequence_Sym0 t :: m ())
type family a =<< a where ...
(%=<<) :: forall a m b (t :: (~>) a (m b)) (t :: m a). SMonad m => Sing t -> Sing t -> Sing (Apply (Apply (=<<@#@$) t) t :: m b)
class PFoldable t where
- type FoldMap (arg :: (~>) a m) (arg :: t a) :: m
- 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 Foldr1 (arg :: (~>) a ((~>) a a)) (arg :: t a) :: a
- type Foldl1 (arg :: (~>) a ((~>) a a)) (arg :: t a) :: a
- 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
- 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)
- 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)
- 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)
- 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 PTraversable t where
- type Traverse (arg :: (~>) a (f b)) (arg :: t a) :: f (t b)
- type SequenceA (arg :: t (f a)) :: f (t a)
- type MapM (arg :: (~>) a (m b)) (arg :: t a) :: m (t b)
- type Sequence (arg :: t (m a)) :: m (t a)
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))
type family Id a where ...
sId :: forall a (t :: a). Sing t -> Sing (Apply IdSym0 t :: a)
type family Const a a where ...
sConst :: forall a b (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply ConstSym0 t) t :: 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)
type family a $ a where ...
(%$) :: forall a b (t :: (~>) a b) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply ($@#@$) t) t :: b)
type family a $! a where ...
(%$!) :: forall a b (t :: (~>) a b) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply ($!@#@$) t) t :: b)
type family Flip a a a where ...
sFlip :: forall a b c (t :: (~>) a ((~>) b c)) (t :: b) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FlipSym0 t) t) t :: c)
type family AsTypeOf a a where ...
sAsTypeOf :: forall a (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply AsTypeOfSym0 t) t :: a)
type family Seq a a where ...
sSeq :: forall a b (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply SeqSym0 t) t :: b)
type family Map a a where ...
sMap :: forall a b (t :: (~>) a b) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b])
type family a ++ a where ...
(%++) :: forall a (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (++@#@$) t) t :: [a])
type family Filter a a where ...
sFilter :: forall a (t :: (~>) a Bool) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply FilterSym0 t) t :: [a])
type family Head a where ...
sHead :: forall a (t :: [a]). Sing t -> Sing (Apply HeadSym0 t :: a)
type family Last a where ...
sLast :: forall a (t :: [a]). Sing t -> Sing (Apply LastSym0 t :: a)
type family Tail a where ...
sTail :: forall a (t :: [a]). Sing t -> Sing (Apply TailSym0 t :: [a])
type family Init a where ...
sInit :: forall a (t :: [a]). Sing t -> Sing (Apply InitSym0 t :: [a])
type family Null (arg :: t a) :: Bool
sNull :: forall a (t :: t a). SFoldable t => Sing t -> Sing (Apply NullSym0 t :: Bool)
type family Reverse a where ...
sReverse :: forall a (t :: [a]). Sing t -> Sing (Apply ReverseSym0 t :: [a])
type family And a where ...
sAnd :: forall t (t :: t Bool). SFoldable t => Sing t -> Sing (Apply AndSym0 t :: Bool)
type family Or a where ...
sOr :: forall t (t :: t Bool). SFoldable t => Sing t -> Sing (Apply OrSym0 t :: Bool)
type family Any a a where ...
sAny :: forall a t (t :: (~>) a Bool) (t :: t a). SFoldable t => Sing t -> Sing t -> Sing (Apply (Apply AnySym0 t) t :: Bool)
type family All a a where ...
sAll :: forall a t (t :: (~>) a Bool) (t :: t a). SFoldable t => Sing t -> Sing t -> Sing (Apply (Apply AllSym0 t) t :: Bool)
type family Concat a where ...
sConcat :: forall t a (t :: t [a]). SFoldable t => Sing t -> Sing (Apply ConcatSym0 t :: [a])
type family ConcatMap a a where ...
sConcatMap :: forall a b t (t :: (~>) a [b]) (t :: t a). SFoldable t => Sing t -> Sing t -> Sing (Apply (Apply ConcatMapSym0 t) t :: [b])
type family Scanl a a a where ...
sScanl :: forall b a (t :: (~>) b ((~>) a b)) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ScanlSym0 t) t) t :: [b])
type family Scanl1 a a where ...
sScanl1 :: forall a (t :: (~>) a ((~>) a a)) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Scanl1Sym0 t) t :: [a])
type family Scanr a a a where ...
sScanr :: forall a b (t :: (~>) a ((~>) b b)) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ScanrSym0 t) t) t :: [b])
type family Scanr1 a a where ...
sScanr1 :: forall a (t :: (~>) a ((~>) a a)) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply Scanr1Sym0 t) t :: [a])
type family Replicate a a where ...
sReplicate :: forall a (t :: Nat) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply ReplicateSym0 t) t :: [a])
type family Take a a where ...
sTake :: forall a (t :: Nat) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply TakeSym0 t) t :: [a])
type family Drop a a where ...
sDrop :: forall a (t :: Nat) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply DropSym0 t) t :: [a])
type family SplitAt a a where ...
sSplitAt :: forall a (t :: Nat) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply SplitAtSym0 t) t :: ([a], [a]))
type family TakeWhile a a where ...
sTakeWhile :: forall a (t :: (~>) a Bool) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply TakeWhileSym0 t) t :: [a])
type family Span a a where ...
sSpan :: forall a (t :: (~>) a Bool) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply SpanSym0 t) t :: ([a], [a]))
type family Break a a where ...
sBreak :: forall a (t :: (~>) a Bool) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply BreakSym0 t) t :: ([a], [a]))
type family NotElem a a where ...
sNotElem :: forall a t (t :: a) (t :: t a). (SFoldable t, SEq a) => Sing t -> Sing t -> Sing (Apply (Apply NotElemSym0 t) t :: Bool)
type family Lookup a a where ...
sLookup :: forall a b (t :: a) (t :: [(a, b)]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply LookupSym0 t) t :: Maybe b)
type family Zip a a where ...
sZip :: forall a b (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing (Apply (Apply ZipSym0 t) t :: [(a, b)])
type family Zip3 a a a where ...
sZip3 :: forall a b c (t :: [a]) (t :: [b]) (t :: [c]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Zip3Sym0 t) t) t :: [(a, b, c)])
type family ZipWith a a a where ...
sZipWith :: forall a b c (t :: (~>) a ((~>) b c)) (t :: [a]) (t :: [b]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ZipWithSym0 t) t) t :: [c])
type family ZipWith3 a a a a where ...
sZipWith3 :: forall a b c d (t :: (~>) a ((~>) b ((~>) c d))) (t :: [a]) (t :: [b]) (t :: [c]). Sing t -> Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (Apply ZipWith3Sym0 t) t) t) t :: [d])
type family Unzip a where ...
sUnzip :: forall a b (t :: [(a, b)]). Sing t -> Sing (Apply UnzipSym0 t :: ([a], [b]))
type family Unzip3 a where ...
sUnzip3 :: forall a b c (t :: [(a, b, c)]). Sing t -> Sing (Apply Unzip3Sym0 t :: ([a], [b], [c]))
type family Unlines a where ...
sUnlines :: forall (t :: [Symbol]). Sing t -> Sing (Apply UnlinesSym0 t :: Symbol)
type family Unwords a where ...
sUnwords :: forall (t :: [Symbol]). Sing t -> Sing (Apply UnwordsSym0 t :: Symbol)
type family Maybe_ a a a where ...
sMaybe_ :: forall b a (t :: b) (t :: (~>) a b) (t :: Maybe a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Maybe_Sym0 t) t) t :: b)
type family Either_ a a a where ...
sEither_ :: forall a c b (t :: (~>) a c) (t :: (~>) b c) (t :: Either a b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Either_Sym0 t) t) t :: c)
type family Fst a where ...
sFst :: forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t :: a)
type family Snd a where ...
sSnd :: forall a b (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t :: b)
type family Curry a a a where ...
sCurry :: forall a b c (t :: (~>) (a, b) c) (t :: a) (t :: b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply CurrySym0 t) t) t :: c)
type family Uncurry a a where ...
sUncurry :: forall a b c (t :: (~>) a ((~>) b c)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply UncurrySym0 t) t :: c)
data Symbol
either_ :: (a -> c) -> (b -> c) -> Either a b -> c
maybe_ :: b -> (a -> b) -> Maybe a -> b
bool_ :: a -> a -> Bool -> a
show_ :: Show a => a -> String
type FalseSym0 = 'False :: Bool
type TrueSym0 = 'True :: Bool
data NotSym0 a6989586621679367240
type NotSym1 (a6989586621679367240 :: Bool) = Not a6989586621679367240 :: Bool
data (&&@#@$) a6989586621679366665
data a6989586621679366665 &&@#@$$ a6989586621679366666
type (&&@#@$$$) (a6989586621679366665 :: Bool) (a6989586621679366666 :: Bool) = (&&) a6989586621679366665 a6989586621679366666 :: Bool
data (||@#@$) a6989586621679366963
data a6989586621679366963 ||@#@$$ a6989586621679366964
type (||@#@$$$) (a6989586621679366963 :: Bool) (a6989586621679366964 :: Bool) = (||) a6989586621679366963 a6989586621679366964 :: Bool
type OtherwiseSym0 = Otherwise :: Bool
type NothingSym0 = 'Nothing :: Maybe (a :: Type)
data JustSym0 a6989586621679304113
type JustSym1 (a6989586621679304113 :: a) = 'Just a6989586621679304113 :: Maybe (a :: Type)
data Maybe_Sym0 a6989586621679500654
data Maybe_Sym1 a6989586621679500654 a6989586621679500655
data Maybe_Sym2 a6989586621679500654 a6989586621679500655 a6989586621679500656
type Maybe_Sym3 (a6989586621679500654 :: b) (a6989586621679500655 :: (~>) a b) (a6989586621679500656 :: Maybe a) = Maybe_ a6989586621679500654 a6989586621679500655 a6989586621679500656 :: b
data LeftSym0 a6989586621679304182
type LeftSym1 (a6989586621679304182 :: a) = 'Left a6989586621679304182 :: Either (a :: Type) (b :: Type)
data RightSym0 a6989586621679304184
type RightSym1 (a6989586621679304184 :: b) = 'Right a6989586621679304184 :: Either (a :: Type) (b :: Type)
data Either_Sym0 a6989586621680470389
data Either_Sym1 a6989586621680470389 a6989586621680470390
data Either_Sym2 a6989586621680470389 a6989586621680470390 a6989586621680470391
type Either_Sym3 (a6989586621680470389 :: (~>) a c) (a6989586621680470390 :: (~>) b c) (a6989586621680470391 :: Either a b) = Either_ a6989586621680470389 a6989586621680470390 a6989586621680470391 :: c
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 FstSym0 a6989586621679360446
type FstSym1 (a6989586621679360446 :: (a, b)) = Fst a6989586621679360446 :: a
data SndSym0 a6989586621679360442
type SndSym1 (a6989586621679360442 :: (a, b)) = Snd a6989586621679360442 :: b
data CurrySym0 a6989586621679360434
data CurrySym1 a6989586621679360434 a6989586621679360435
data CurrySym2 a6989586621679360434 a6989586621679360435 a6989586621679360436
type CurrySym3 (a6989586621679360434 :: (~>) (a, b) c) (a6989586621679360435 :: a) (a6989586621679360436 :: b) = Curry a6989586621679360434 a6989586621679360435 a6989586621679360436 :: c
data UncurrySym0 a6989586621679360426
data UncurrySym1 a6989586621679360426 a6989586621679360427
type UncurrySym2 (a6989586621679360426 :: (~>) a ((~>) b c)) (a6989586621679360427 :: (a, b)) = Uncurry a6989586621679360426 a6989586621679360427 :: c
data ErrorSym0 a6989586621679472252
type ErrorSym1 (a6989586621679472252 :: k0) = Error a6989586621679472252 :: k
data ErrorWithoutStackTraceSym0 a6989586621679472488
type ErrorWithoutStackTraceSym1 (a6989586621679472488 :: k0) = ErrorWithoutStackTrace a6989586621679472488 :: k
type UndefinedSym0 = Undefined :: k
type LTSym0 = 'LT :: Ordering
type EQSym0 = 'EQ :: Ordering
type GTSym0 = 'GT :: Ordering
data CompareSym0 a6989586621679383640
data CompareSym1 a6989586621679383640 a6989586621679383641
type CompareSym2 (a6989586621679383640 :: a) (a6989586621679383641 :: a) = Compare a6989586621679383640 a6989586621679383641 :: Ordering
data (<@#@$) a6989586621679383645
data a6989586621679383645 <@#@$$ a6989586621679383646
type (<@#@$$$) (a6989586621679383645 :: a) (a6989586621679383646 :: a) = (<) a6989586621679383645 a6989586621679383646 :: Bool
data (<=@#@$) a6989586621679383650
data a6989586621679383650 <=@#@$$ a6989586621679383651
type (<=@#@$$$) (a6989586621679383650 :: a) (a6989586621679383651 :: a) = (<=) a6989586621679383650 a6989586621679383651 :: Bool
data (>@#@$) a6989586621679383655
data a6989586621679383655 >@#@$$ a6989586621679383656
type (>@#@$$$) (a6989586621679383655 :: a) (a6989586621679383656 :: a) = (>) a6989586621679383655 a6989586621679383656 :: Bool
data (>=@#@$) a6989586621679383660
data a6989586621679383660 >=@#@$$ a6989586621679383661
type (>=@#@$$$) (a6989586621679383660 :: a) (a6989586621679383661 :: a) = (>=) a6989586621679383660 a6989586621679383661 :: Bool
data MaxSym0 a6989586621679383665
data MaxSym1 a6989586621679383665 a6989586621679383666
type MaxSym2 (a6989586621679383665 :: a) (a6989586621679383666 :: a) = Max a6989586621679383665 a6989586621679383666 :: a
data MinSym0 a6989586621679383670
data MinSym1 a6989586621679383670 a6989586621679383671
type MinSym2 (a6989586621679383670 :: a) (a6989586621679383671 :: a) = Min a6989586621679383670 a6989586621679383671 :: a
data (^@#@$) a6989586621679472866
data a6989586621679472866 ^@#@$$ a6989586621679472867
type (^@#@$$$) (a6989586621679472866 :: Nat) (a6989586621679472867 :: Nat) = (^) a6989586621679472866 a6989586621679472867 :: Nat
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 Show_Sym0 a6989586621680279573
type Show_Sym1 (a6989586621680279573 :: a) = Show_ a6989586621680279573 :: Symbol
data ShowListSym0 a6989586621680279577
data ShowListSym1 a6989586621680279577 a6989586621680279578
type ShowListSym2 (a6989586621680279577 :: [a]) (a6989586621680279578 :: Symbol) = ShowList a6989586621680279577 a6989586621680279578 :: Symbol
data ShowsSym0 a6989586621680279560
data ShowsSym1 a6989586621680279560 a6989586621680279561
type ShowsSym2 (a6989586621680279560 :: a) (a6989586621680279561 :: Symbol) = Shows a6989586621680279560 a6989586621680279561 :: Symbol
data ShowCharSym0 a6989586621680279534
data ShowCharSym1 a6989586621680279534 a6989586621680279535
type ShowCharSym2 (a6989586621680279534 :: Symbol) (a6989586621680279535 :: Symbol) = ShowChar a6989586621680279534 a6989586621680279535 :: 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 (<>@#@$) a6989586621679830624
data a6989586621679830624 <>@#@$$ a6989586621679830625
type (<>@#@$$$) (a6989586621679830624 :: a) (a6989586621679830625 :: a) = (<>) a6989586621679830624 a6989586621679830625 :: a
type MemptySym0 = Mempty :: a
data MappendSym0 a6989586621680347244
data MappendSym1 a6989586621680347244 a6989586621680347245
type MappendSym2 (a6989586621680347244 :: a) (a6989586621680347245 :: a) = Mappend a6989586621680347244 a6989586621680347245 :: a
data MconcatSym0 a6989586621680347248
type MconcatSym1 (a6989586621680347248 :: [a]) = Mconcat a6989586621680347248 :: a
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 (<$>@#@$) a6989586621679731630
data a6989586621679731630 <$>@#@$$ a6989586621679731631
type (<$>@#@$$$) (a6989586621679731630 :: (~>) a b) (a6989586621679731631 :: f a) = (<$>) a6989586621679731630 a6989586621679731631 :: f 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 (*>@#@$) a6989586621679559707
data a6989586621679559707 *>@#@$$ a6989586621679559708
type (*>@#@$$$) (a6989586621679559707 :: f a) (a6989586621679559708 :: f b) = (*>) a6989586621679559707 a6989586621679559708 :: f b
data (<*@#@$) a6989586621679559712
data a6989586621679559712 <*@#@$$ a6989586621679559713
type (<*@#@$$$) (a6989586621679559712 :: f a) (a6989586621679559713 :: f b) = (<*) a6989586621679559712 a6989586621679559713 :: f a
data (>>=@#@$) a6989586621679559775
data a6989586621679559775 >>=@#@$$ a6989586621679559776
type (>>=@#@$$$) (a6989586621679559775 :: m a) (a6989586621679559776 :: (~>) a (m b)) = (>>=) a6989586621679559775 a6989586621679559776 :: m b
data (>>@#@$) a6989586621679559780
data a6989586621679559780 >>@#@$$ a6989586621679559781
type (>>@#@$$$) (a6989586621679559780 :: m a) (a6989586621679559781 :: m b) = (>>) a6989586621679559780 a6989586621679559781 :: m b
data ReturnSym0 a6989586621679559784
type ReturnSym1 (a6989586621679559784 :: a) = Return a6989586621679559784 :: m a
data FailSym0 a6989586621679729522
type FailSym1 (a6989586621679729522 :: [Char]) = Fail a6989586621679729522 :: m a
data MapM_Sym0 a6989586621680492379
data MapM_Sym1 a6989586621680492379 a6989586621680492380
type MapM_Sym2 (a6989586621680492379 :: (~>) a (m b)) (a6989586621680492380 :: t a) = MapM_ a6989586621680492379 a6989586621680492380 :: m ()
data Sequence_Sym0 a6989586621680492355
type Sequence_Sym1 (a6989586621680492355 :: t (m a)) = Sequence_ a6989586621680492355 :: m ()
data (=<<@#@$) a6989586621679559620
data a6989586621679559620 =<<@#@$$ a6989586621679559621
type (=<<@#@$$$) (a6989586621679559620 :: (~>) a (m b)) (a6989586621679559621 :: m a) = (=<<) a6989586621679559620 a6989586621679559621 :: m b
data ElemSym0 a6989586621680492497
data ElemSym1 a6989586621680492497 a6989586621680492498
type ElemSym2 (a6989586621680492497 :: a) (a6989586621680492498 :: t a) = Elem a6989586621680492497 a6989586621680492498 :: Bool
data FoldMapSym0 a6989586621680492445
data FoldMapSym1 a6989586621680492445 a6989586621680492446
type FoldMapSym2 (a6989586621680492445 :: (~>) a m) (a6989586621680492446 :: t a) = FoldMap a6989586621680492445 a6989586621680492446 :: m
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 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
data Foldr1Sym0 a6989586621680492478
data Foldr1Sym1 a6989586621680492478 a6989586621680492479
type Foldr1Sym2 (a6989586621680492478 :: (~>) a ((~>) a a)) (a6989586621680492479 :: t a) = Foldr1 a6989586621680492478 a6989586621680492479 :: a
data Foldl1Sym0 a6989586621680492483
data Foldl1Sym1 a6989586621680492483 a6989586621680492484
type Foldl1Sym2 (a6989586621680492483 :: (~>) a ((~>) a a)) (a6989586621680492484 :: t a) = Foldl1 a6989586621680492483 a6989586621680492484 :: a
data MaximumSym0 a6989586621680492501
type MaximumSym1 (a6989586621680492501 :: t a) = Maximum a6989586621680492501 :: a
data MinimumSym0 a6989586621680492504
type MinimumSym1 (a6989586621680492504 :: t a) = Minimum a6989586621680492504 :: a
data SumSym0 a6989586621680492507
type SumSym1 (a6989586621680492507 :: t a) = Sum a6989586621680492507 :: a
data ProductSym0 a6989586621680492510
type ProductSym1 (a6989586621680492510 :: t a) = Product a6989586621680492510 :: a
data TraverseSym0 a6989586621680816742
data TraverseSym1 a6989586621680816742 a6989586621680816743
type TraverseSym2 (a6989586621680816742 :: (~>) a (f b)) (a6989586621680816743 :: t a) = Traverse a6989586621680816742 a6989586621680816743 :: f (t b)
data SequenceASym0 a6989586621680816746
type SequenceASym1 (a6989586621680816746 :: t (f a)) = SequenceA a6989586621680816746 :: f (t a)
data MapMSym0 a6989586621680816750
data MapMSym1 a6989586621680816750 a6989586621680816751
type MapMSym2 (a6989586621680816750 :: (~>) a (m b)) (a6989586621680816751 :: t a) = MapM a6989586621680816750 a6989586621680816751 :: m (t b)
data SequenceSym0 a6989586621680816754
type SequenceSym1 (a6989586621680816754 :: t (m a)) = Sequence a6989586621680816754 :: m (t a)
data IdSym0 a6989586621679534205
type IdSym1 (a6989586621679534205 :: a) = Id a6989586621679534205 :: a
data ConstSym0 a6989586621679534200
data ConstSym1 a6989586621679534200 a6989586621679534201
type ConstSym2 (a6989586621679534200 :: a) (a6989586621679534201 :: b) = Const a6989586621679534200 a6989586621679534201 :: a
data (.@#@$) a6989586621679534187
data a6989586621679534187 .@#@$$ a6989586621679534188
data (a6989586621679534187 .@#@$$$ a6989586621679534188) a6989586621679534189
data ($@#@$) a6989586621679534156
data a6989586621679534156 $@#@$$ a6989586621679534157
type ($@#@$$$) (a6989586621679534156 :: (~>) a b) (a6989586621679534157 :: a) = ($) a6989586621679534156 a6989586621679534157 :: b
data ($!@#@$) a6989586621679534147
data a6989586621679534147 $!@#@$$ a6989586621679534148
type ($!@#@$$$) (a6989586621679534147 :: (~>) a b) (a6989586621679534148 :: a) = ($!) a6989586621679534147 a6989586621679534148 :: b
data FlipSym0 a6989586621679534175
data FlipSym1 a6989586621679534175 a6989586621679534176
data FlipSym2 a6989586621679534175 a6989586621679534176 a6989586621679534177
data AsTypeOfSym0 a6989586621679534167
data AsTypeOfSym1 a6989586621679534167 a6989586621679534168
type AsTypeOfSym2 (a6989586621679534167 :: a) (a6989586621679534168 :: a) = AsTypeOf a6989586621679534167 a6989586621679534168 :: a
data SeqSym0 a6989586621679534120
data SeqSym1 a6989586621679534120 a6989586621679534121
type SeqSym2 (a6989586621679534120 :: a) (a6989586621679534121 :: b) = Seq a6989586621679534120 a6989586621679534121 :: b
data (:@#@$) a6989586621679304138
data a6989586621679304138 :@#@$$ a6989586621679304139
type (:@#@$$$) (a6989586621679304138 :: a) (a6989586621679304139 :: [a]) = '(:) a6989586621679304138 a6989586621679304139 :: [a :: Type]
type NilSym0 = '[] :: [a :: Type]
data MapSym0 a6989586621679534219
data MapSym1 a6989586621679534219 a6989586621679534220
type MapSym2 (a6989586621679534219 :: (~>) a b) (a6989586621679534220 :: [a]) = Map a6989586621679534219 a6989586621679534220 :: [b]
data ReverseSym0 a6989586621679970000
type ReverseSym1 (a6989586621679970000 :: [a]) = Reverse a6989586621679970000 :: [a]
data a6989586621679534210 ++@#@$$ a6989586621679534211
data (++@#@$) a6989586621679534210
data FilterSym0 a6989586621679969267
data FilterSym1 a6989586621679969267 a6989586621679969268
type FilterSym2 (a6989586621679969267 :: (~>) a Bool) (a6989586621679969268 :: [a]) = Filter a6989586621679969267 a6989586621679969268 :: [a]
data HeadSym0 a6989586621679970037
type HeadSym1 (a6989586621679970037 :: [a]) = Head a6989586621679970037 :: a
data LastSym0 a6989586621679970031
type LastSym1 (a6989586621679970031 :: [a]) = Last a6989586621679970031 :: a
data TailSym0 a6989586621679970027
type TailSym1 (a6989586621679970027 :: [a]) = Tail a6989586621679970027 :: [a]
data InitSym0 a6989586621679970015
type InitSym1 (a6989586621679970015 :: [a]) = Init a6989586621679970015 :: [a]
data NullSym0 a6989586621680492490
type NullSym1 (a6989586621680492490 :: t a) = Null a6989586621680492490 :: Bool
data ConcatSym0 a6989586621680492332
type ConcatSym1 (a6989586621680492332 :: t [a]) = Concat a6989586621680492332 :: [a]
data ConcatMapSym0 a6989586621680492321
data ConcatMapSym1 a6989586621680492321 a6989586621680492322
type ConcatMapSym2 (a6989586621680492321 :: (~>) a [b]) (a6989586621680492322 :: t a) = ConcatMap a6989586621680492321 a6989586621680492322 :: [b]
data AndSym0 a6989586621680492316
type AndSym1 (a6989586621680492316 :: t Bool) = And a6989586621680492316 :: Bool
data OrSym0 a6989586621680492310
type OrSym1 (a6989586621680492310 :: t Bool) = Or a6989586621680492310 :: Bool
data AnySym0 a6989586621680492302
data AnySym1 a6989586621680492302 a6989586621680492303
type AnySym2 (a6989586621680492302 :: (~>) a Bool) (a6989586621680492303 :: t a) = Any a6989586621680492302 a6989586621680492303 :: Bool
data AllSym0 a6989586621680492293
data AllSym1 a6989586621680492293 a6989586621680492294
type AllSym2 (a6989586621680492293 :: (~>) a Bool) (a6989586621680492294 :: t a) = All a6989586621680492293 a6989586621680492294 :: Bool
data ScanlSym0 a6989586621679969805
data ScanlSym1 a6989586621679969805 a6989586621679969806
data ScanlSym2 a6989586621679969805 a6989586621679969806 a6989586621679969807
type ScanlSym3 (a6989586621679969805 :: (~>) b ((~>) a b)) (a6989586621679969806 :: b) (a6989586621679969807 :: [a]) = Scanl a6989586621679969805 a6989586621679969806 a6989586621679969807 :: [b]
data Scanl1Sym0 a6989586621679969796
data Scanl1Sym1 a6989586621679969796 a6989586621679969797
type Scanl1Sym2 (a6989586621679969796 :: (~>) a ((~>) a a)) (a6989586621679969797 :: [a]) = Scanl1 a6989586621679969796 a6989586621679969797 :: [a]
data ScanrSym0 a6989586621679969778
data ScanrSym1 a6989586621679969778 a6989586621679969779
data ScanrSym2 a6989586621679969778 a6989586621679969779 a6989586621679969780
type ScanrSym3 (a6989586621679969778 :: (~>) a ((~>) b b)) (a6989586621679969779 :: b) (a6989586621679969780 :: [a]) = Scanr a6989586621679969778 a6989586621679969779 a6989586621679969780 :: [b]
data Scanr1Sym0 a6989586621679969758
data Scanr1Sym1 a6989586621679969758 a6989586621679969759
type Scanr1Sym2 (a6989586621679969758 :: (~>) a ((~>) a a)) (a6989586621679969759 :: [a]) = Scanr1 a6989586621679969758 a6989586621679969759 :: [a]
data ReplicateSym0 a6989586621679968895
data ReplicateSym1 a6989586621679968895 a6989586621679968896
type ReplicateSym2 (a6989586621679968895 :: Nat) (a6989586621679968896 :: a) = Replicate a6989586621679968895 a6989586621679968896 :: [a]
data TakeSym0 a6989586621679969050
data TakeSym1 a6989586621679969050 a6989586621679969051
type TakeSym2 (a6989586621679969050 :: Nat) (a6989586621679969051 :: [a]) = Take a6989586621679969050 a6989586621679969051 :: [a]
data DropSym0 a6989586621679969037
data DropSym1 a6989586621679969037 a6989586621679969038
type DropSym2 (a6989586621679969037 :: Nat) (a6989586621679969038 :: [a]) = Drop a6989586621679969037 a6989586621679969038 :: [a]
data SplitAtSym0 a6989586621679969030
data SplitAtSym1 a6989586621679969030 a6989586621679969031
type SplitAtSym2 (a6989586621679969030 :: Nat) (a6989586621679969031 :: [a]) = SplitAt a6989586621679969030 a6989586621679969031 :: ([a], [a])
data TakeWhileSym0 a6989586621679969167
data TakeWhileSym1 a6989586621679969167 a6989586621679969168
type TakeWhileSym2 (a6989586621679969167 :: (~>) a Bool) (a6989586621679969168 :: [a]) = TakeWhile a6989586621679969167 a6989586621679969168 :: [a]
data DropWhileSym0 a6989586621679969152
data DropWhileSym1 a6989586621679969152 a6989586621679969153
type DropWhileSym2 (a6989586621679969152 :: (~>) a Bool) (a6989586621679969153 :: [a]) = DropWhile a6989586621679969152 a6989586621679969153 :: [a]
data DropWhileEndSym0 a6989586621679969135
data DropWhileEndSym1 a6989586621679969135 a6989586621679969136
type DropWhileEndSym2 (a6989586621679969135 :: (~>) a Bool) (a6989586621679969136 :: [a]) = DropWhileEnd a6989586621679969135 a6989586621679969136 :: [a]
data SpanSym0 a6989586621679969098
data SpanSym1 a6989586621679969098 a6989586621679969099
type SpanSym2 (a6989586621679969098 :: (~>) a Bool) (a6989586621679969099 :: [a]) = Span a6989586621679969098 a6989586621679969099 :: ([a], [a])
data BreakSym0 a6989586621679969063
data BreakSym1 a6989586621679969063 a6989586621679969064
type BreakSym2 (a6989586621679969063 :: (~>) a Bool) (a6989586621679969064 :: [a]) = Break a6989586621679969063 a6989586621679969064 :: ([a], [a])
data NotElemSym0 a6989586621680492244
data NotElemSym1 a6989586621680492244 a6989586621680492245
type NotElemSym2 (a6989586621680492244 :: a) (a6989586621680492245 :: t a) = NotElem a6989586621680492244 a6989586621680492245 :: Bool
data ZipSym0 a6989586621679969585
data ZipSym1 a6989586621679969585 a6989586621679969586
type ZipSym2 (a6989586621679969585 :: [a]) (a6989586621679969586 :: [b]) = Zip a6989586621679969585 a6989586621679969586 :: [(a, b)]
data Zip3Sym0 a6989586621679969573
data Zip3Sym1 a6989586621679969573 a6989586621679969574
data Zip3Sym2 a6989586621679969573 a6989586621679969574 a6989586621679969575
type Zip3Sym3 (a6989586621679969573 :: [a]) (a6989586621679969574 :: [b]) (a6989586621679969575 :: [c]) = Zip3 a6989586621679969573 a6989586621679969574 a6989586621679969575 :: [(a, b, c)]
data ZipWithSym0 a6989586621679969561
data ZipWithSym1 a6989586621679969561 a6989586621679969562
data ZipWithSym2 a6989586621679969561 a6989586621679969562 a6989586621679969563
type ZipWithSym3 (a6989586621679969561 :: (~>) a ((~>) b c)) (a6989586621679969562 :: [a]) (a6989586621679969563 :: [b]) = ZipWith a6989586621679969561 a6989586621679969562 a6989586621679969563 :: [c]
data ZipWith3Sym0 a6989586621679969546
data ZipWith3Sym1 a6989586621679969546 a6989586621679969547
data ZipWith3Sym2 a6989586621679969546 a6989586621679969547 a6989586621679969548
data ZipWith3Sym3 a6989586621679969546 a6989586621679969547 a6989586621679969548 a6989586621679969549
data UnzipSym0 a6989586621679969527
type UnzipSym1 (a6989586621679969527 :: [(a, b)]) = Unzip a6989586621679969527 :: ([a], [b])
data UnlinesSym0 a6989586621679969412
type UnlinesSym1 (a6989586621679969412 :: [Symbol]) = Unlines a6989586621679969412 :: Symbol
data UnwordsSym0 a6989586621679969402
type UnwordsSym1 (a6989586621679969402 :: [Symbol]) = Unwords a6989586621679969402 :: Symbol

Basic singleton definitions

module Data.Singletons

Singleton types

data SBool z where Source #

Constructors

SFalse :: SBool ('False :: Bool)
STrue :: SBool ('True :: Bool)

Instances

Instances details

TestCoercion SBool Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a :: k) (b :: k). SBool a -> SBool b -> Maybe (Coercion a b) #
TestEquality SBool Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a :: k) (b :: k). SBool a -> SBool b -> Maybe (a :~: b) #
Show (SBool z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SBool z -> ShowS # show :: SBool z -> String # showList :: [SBool z] -> ShowS #

data SList z where Source #

Constructors

SNil :: forall (a :: Type). SList ('[] :: [a :: Type])
SCons :: forall (a :: Type) (n :: a) (n :: [a]). (Sing n) -> (Sing n) -> SList ('(:) n n :: [a :: Type]) infixr 5

Instances

Instances details

(SDecide a, SDecide [a]) => TestCoercion (SList :: [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b :: k). SList a0 -> SList b -> Maybe (Coercion a0 b) #
(SDecide a, SDecide [a]) => TestEquality (SList :: [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b :: k). SList a0 -> SList b -> Maybe (a0 :~: b) #
(ShowSing a, ShowSing [a]) => Show (SList z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SList z -> ShowS # show :: SList z -> String # showList :: [SList z] -> ShowS #

data SMaybe z where Source #

Constructors

SNothing :: forall (a :: Type). SMaybe ('Nothing :: Maybe (a :: Type))
SJust :: forall (a :: Type) (n :: a). (Sing n) -> SMaybe ('Just n :: Maybe (a :: Type))

Instances

Instances details

SDecide a => TestCoercion (SMaybe :: Maybe a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b :: k). SMaybe a0 -> SMaybe b -> Maybe (Coercion a0 b) #
SDecide a => TestEquality (SMaybe :: Maybe a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b :: k). SMaybe a0 -> SMaybe b -> Maybe (a0 :~: b) #
ShowSing a => Show (SMaybe z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SMaybe z -> ShowS # show :: SMaybe z -> String # showList :: [SMaybe z] -> ShowS #

data SEither z where Source #

Constructors

SLeft :: forall (a :: Type) (b :: Type) (n :: a). (Sing n) -> SEither ('Left n :: Either (a :: Type) (b :: Type))
SRight :: forall (a :: Type) (b :: Type) (n :: b). (Sing n) -> SEither ('Right n :: Either (a :: Type) (b :: Type))

Instances

Instances details

(SDecide a, SDecide b) => TestCoercion (SEither :: Either a b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b0 :: k). SEither a0 -> SEither b0 -> Maybe (Coercion a0 b0) #
(SDecide a, SDecide b) => TestEquality (SEither :: Either a b -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). SEither a0 -> SEither b0 -> Maybe (a0 :~: b0) #
(ShowSing a, ShowSing b) => Show (SEither z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SEither z -> ShowS # show :: SEither z -> String # showList :: [SEither z] -> ShowS #

data SOrdering z where Source #

Constructors

SLT :: SOrdering ('LT :: Ordering)
SEQ :: SOrdering ('EQ :: Ordering)
SGT :: SOrdering ('GT :: Ordering)

Instances

Instances details

TestCoercion SOrdering Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (Coercion a b) #
TestEquality SOrdering Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (a :~: b) #
Show (SOrdering z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SOrdering z -> ShowS # show :: SOrdering z -> String # showList :: [SOrdering z] -> ShowS #

data STuple0 z where Source #

Constructors

STuple0 :: STuple0 ('() :: ())

Instances

Instances details

TestCoercion STuple0 Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a :: k) (b :: k). STuple0 a -> STuple0 b -> Maybe (Coercion a b) #
TestEquality STuple0 Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a :: k) (b :: k). STuple0 a -> STuple0 b -> Maybe (a :~: b) #
Show (STuple0 z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> STuple0 z -> ShowS # show :: STuple0 z -> String # showList :: [STuple0 z] -> ShowS #

data STuple2 z where Source #

Constructors

STuple2 :: forall (a :: Type) (b :: Type) (n :: a) (n :: b). (Sing n) -> (Sing n) -> STuple2 ('(n, n) :: (a :: Type, b :: Type))

Instances

Instances details

(SDecide a, SDecide b) => TestCoercion (STuple2 :: (a, b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b0 :: k). STuple2 a0 -> STuple2 b0 -> Maybe (Coercion a0 b0) #
(SDecide a, SDecide b) => TestEquality (STuple2 :: (a, b) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). STuple2 a0 -> STuple2 b0 -> Maybe (a0 :~: b0) #
(ShowSing a, ShowSing b) => Show (STuple2 z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> STuple2 z -> ShowS # show :: STuple2 z -> String # showList :: [STuple2 z] -> ShowS #

data STuple3 z where Source #

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

Instances details

(SDecide a, SDecide b, SDecide c) => TestCoercion (STuple3 :: (a, b, c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b0 :: k). STuple3 a0 -> STuple3 b0 -> Maybe (Coercion a0 b0) #
(SDecide a, SDecide b, SDecide c) => TestEquality (STuple3 :: (a, b, c) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). STuple3 a0 -> STuple3 b0 -> Maybe (a0 :~: b0) #
(ShowSing a, ShowSing b, ShowSing c) => Show (STuple3 z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> STuple3 z -> ShowS # show :: STuple3 z -> String # showList :: [STuple3 z] -> ShowS #

data STuple4 z where 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

Instances details

(SDecide a, SDecide b, SDecide c, SDecide d) => TestCoercion (STuple4 :: (a, b, c, d) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b0 :: k). STuple4 a0 -> STuple4 b0 -> Maybe (Coercion a0 b0) #
(SDecide a, SDecide b, SDecide c, SDecide d) => TestEquality (STuple4 :: (a, b, c, d) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). STuple4 a0 -> STuple4 b0 -> Maybe (a0 :~: b0) #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (STuple4 z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> STuple4 z -> ShowS # show :: STuple4 z -> String # showList :: [STuple4 z] -> ShowS #

data STuple5 z where 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

Instances details

(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e) => TestCoercion (STuple5 :: (a, b, c, d, e) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b0 :: k). STuple5 a0 -> STuple5 b0 -> Maybe (Coercion a0 b0) #
(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e) => TestEquality (STuple5 :: (a, b, c, d, e) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). STuple5 a0 -> STuple5 b0 -> Maybe (a0 :~: b0) #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (STuple5 z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> STuple5 z -> ShowS # show :: STuple5 z -> String # showList :: [STuple5 z] -> ShowS #

data STuple6 z where 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

Instances details

(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f) => TestCoercion (STuple6 :: (a, b, c, d, e, f) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b0 :: k). STuple6 a0 -> STuple6 b0 -> Maybe (Coercion a0 b0) #
(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f) => TestEquality (STuple6 :: (a, b, c, d, e, f) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). STuple6 a0 -> STuple6 b0 -> Maybe (a0 :~: b0) #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (STuple6 z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> STuple6 z -> ShowS # show :: STuple6 z -> String # showList :: [STuple6 z] -> ShowS #

data STuple7 z where 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

Instances details

(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 #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b0 :: k). STuple7 a0 -> STuple7 b0 -> Maybe (Coercion a0 b0) #
(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 #
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b0 :: k). STuple7 a0 -> STuple7 b0 -> Maybe (a0 :~: b0) #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (STuple7 z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> STuple7 z -> ShowS # show :: STuple7 z -> String # showList :: [STuple7 z] -> ShowS #

Functions working with `Bool`

type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #

Type-level If. If True a b ==> a; If False a b ==> b

Equations

If 'True (tru :: k) (fls :: k) = tru
If 'False (tru :: k) (fls :: k) = fls

sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c) Source #

Conditional over singletons

type family Not (a :: Bool) = (res :: Bool) | res -> a where ... #

Type-level "not". An injective type family since 4.10.0.0.

Since: base-4.7.0.0

Equations

Not 'False = 'True
Not 'True = 'False

sNot :: Sing a -> Sing (Not a) Source #

Negation of a singleton

type family (a :: Bool) && (b :: Bool) :: Bool where ... infixr 3 #

Type-level "and"

Equations

'False && a = 'False
'True && a = a
a && 'False = 'False
a && 'True = a
a && a = a

type family (a :: Bool) || (b :: Bool) :: Bool where ... infixr 2 #

Type-level "or"

Equations

'False \|\| a = a
'True \|\| a = 'True
a \|\| 'False = a
a \|\| 'True = 'True
a \|\| a = a

(%&&) :: Sing a -> Sing b -> Sing (a && b) infixr 3 Source #

Conjunction of singletons

(%||) :: Sing a -> Sing b -> Sing (a || b) infixr 2 Source #

Disjunction of singletons

type family Otherwise where ... Source #

Equations

Otherwise = TrueSym0

sOtherwise :: Sing (OtherwiseSym0 :: Bool) Source #

Error reporting

type family Error str where ... Source #

The promotion of error. This version is more poly-kinded for easier use.

sError :: HasCallStack => Sing (str :: Symbol) -> a Source #

The singleton for error

type family ErrorWithoutStackTrace str where ... Source #

The promotion of errorWithoutStackTrace. This version is more poly-kinded for easier use.

sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a Source #

The singleton for errorWithoutStackTrace.

type family Undefined where ... Source #

The promotion of undefined.

sUndefined :: HasCallStack => a Source #

The singleton for undefined.

Singleton equality

module Data.Singletons.Prelude.Eq

Singleton comparisons

class POrd a Source #

Associated Types

type Compare (arg :: a) (arg :: a) :: Ordering Source #

type Compare a a = Apply (Apply Compare_6989586621679383674Sym0 a) a

type (arg :: a) < (arg :: a) :: Bool infix 4 Source #

type a < a = Apply (Apply TFHelper_6989586621679383695Sym0 a) a

type (arg :: a) <= (arg :: a) :: Bool infix 4 Source #

type a <= a = Apply (Apply TFHelper_6989586621679383711Sym0 a) a

type (arg :: a) > (arg :: a) :: Bool infix 4 Source #

type a > a = Apply (Apply TFHelper_6989586621679383727Sym0 a) a

type (arg :: a) >= (arg :: a) :: Bool infix 4 Source #

type a >= a = Apply (Apply TFHelper_6989586621679383743Sym0 a) a

type Max (arg :: a) (arg :: a) :: a Source #

type Max a a = Apply (Apply Max_6989586621679383759Sym0 a) a

type Min (arg :: a) (arg :: a) :: a Source #

type Min a a = Apply (Apply Min_6989586621679383775Sym0 a) a

Instances

Instances details

POrd Bool Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd () Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Void Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd All Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Any Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd [a] Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Option a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Arg a b) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Proxy s) Source #
Instance details Defined in Data.Singletons.Prelude.Proxy Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c, d) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c, d, e) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c, d, e, f) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a 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 #

default sMin :: forall (t :: a) (t :: a). (Apply (Apply MinSym0 t) t :: a) ~ Apply (Apply Min_6989586621679383775Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) Source #

Instances

Instances details

SOrd Bool Source #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #
Instance details 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 #

Singleton Enum and Bounded

As a matter of convenience, the singletons Prelude does not export promoted/singletonized succ and pred, due to likely conflicts with unary numbers. Please import Enum directly if you want these.

class SBounded a where Source #

Methods

sMinBound :: Sing (MinBoundSym0 :: a) Source #

sMaxBound :: Sing (MaxBoundSym0 :: a) Source #

Instances

Instances details

SBounded Bool Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded () Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded Bool => SBounded All Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded Bool => SBounded Any Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded m => SBounded (WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
(SBounded a, SBounded b) => SBounded (a, b) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded (Proxy s) Source #
Instance details Defined in Data.Singletons.Prelude.Proxy Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
(SBounded a, SBounded b, SBounded c) => SBounded (a, b, c) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
SBounded a => SBounded (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
(SBounded a, SBounded b, SBounded c, SBounded d) => SBounded (a, b, c, d) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e) => SBounded (a, b, c, d, e) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f) => SBounded (a, b, c, d, e, f) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #
(SBounded a, SBounded b, SBounded c, SBounded d, SBounded e, SBounded f, SBounded g) => SBounded (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sMinBound :: Sing MinBoundSym0 Source # sMaxBound :: Sing MaxBoundSym0 Source #

class PBounded a Source #

Associated Types

type MinBound :: a Source #

type MaxBound :: a Source #

Instances

Instances details

PBounded Bool Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded () Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded All Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded Any Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (a, b) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Proxy s) Source #
Instance details Defined in Data.Singletons.Prelude.Proxy Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (a, b, c) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (a, b, c, d) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (a, b, c, d, e) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (a, b, c, d, e, f) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #
PBounded (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type MinBound :: a Source # type MaxBound :: a Source #

type MaxBoundSym0 = MaxBound :: a Source #

type MinBoundSym0 = MinBound :: a Source #

class SEnum a where Source #

Minimal complete definition

sToEnum, sFromEnum

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 #

sEnumFromTo :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) Source #

default sEnumFromTo :: forall (t :: a) (t :: a). (Apply (Apply EnumFromToSym0 t) t :: [a]) ~ Apply (Apply EnumFromTo_6989586621679758515Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) Source #

sEnumFromThenTo :: forall (t :: a) (t :: a) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) Source #

default sEnumFromThenTo :: forall (t :: a) (t :: a) (t :: a). (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) ~ Apply (Apply (Apply EnumFromThenTo_6989586621679758527Sym0 t) t) t => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) Source #

Instances

Instances details

SEnum Bool Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: forall (t :: Bool). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Bool). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Bool). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Bool) (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: forall (t :: Ordering). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Ordering). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Ordering). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Ordering) (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: forall (t :: Nat). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Nat). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Nat) (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum () Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: forall (t :: ()). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: ()). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: ()). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: ()) (t :: ()) (t :: ()). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum a => SEnum (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: forall (t :: Min a). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Min a). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Min a). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Min a) (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum a => SEnum (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: forall (t :: Max a). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Max a). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Max a). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Max a) (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum a => SEnum (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: forall (t :: First a). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: First a). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: First a). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: First a) (t :: First a) (t :: First a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum a => SEnum (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: forall (t :: Last a). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Last a). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Last a). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Last a) (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum a => SEnum (WrappedMonoid a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sSucc :: forall (t :: WrappedMonoid a). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: WrappedMonoid a). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: WrappedMonoid a). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: WrappedMonoid a) (t :: WrappedMonoid a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: WrappedMonoid a) (t :: WrappedMonoid a) (t :: WrappedMonoid a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum a => SEnum (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Identity Methods sSucc :: forall (t :: Identity a). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Identity a). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Identity a). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Identity a) (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum (Proxy s) Source #
Instance details Defined in Data.Singletons.Prelude.Proxy Methods sSucc :: forall (t :: Proxy s). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Proxy s). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Proxy s). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Proxy s) (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #
SEnum a => SEnum (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Methods sSucc :: forall (t :: Const a b). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Const a b). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Const a b). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source # sEnumFromThenTo :: forall (t :: Const a b) (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #

class PEnum a Source #

Associated Types

type ToEnum (arg :: Nat) :: a Source #

type FromEnum (arg :: a) :: Nat Source #

type EnumFromTo (arg :: a) (arg :: a) :: [a] Source #

type EnumFromTo a a = Apply (Apply EnumFromTo_6989586621679758515Sym0 a) a

type EnumFromThenTo (arg :: a) (arg :: a) (arg :: a) :: [a] Source #

type EnumFromThenTo a a a = Apply (Apply (Apply EnumFromThenTo_6989586621679758527Sym0 a) a) a

Instances

Instances details

PEnum Bool Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum Nat Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum () Source #
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum (WrappedMonoid a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Identity Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum (Proxy s) Source #
Instance details Defined in Data.Singletons.Prelude.Proxy Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
PEnum (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #

type EnumFromThenToSym3 (a6989586621679758488 :: a) (a6989586621679758489 :: a) (a6989586621679758490 :: a) = EnumFromThenTo a6989586621679758488 a6989586621679758489 a6989586621679758490 :: [a] Source #

data EnumFromThenToSym2 a6989586621679758488 a6989586621679758489 a6989586621679758490 Source #

Instances

Instances details

(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromThenToSym2 d1 d2) Source #
SuppressUnusedWarnings (EnumFromThenToSym2 a6989586621679758488 a6989586621679758489 :: TyFun a [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
type Apply (EnumFromThenToSym2 a6989586621679758488 a6989586621679758489 :: TyFun a [a] -> Type) (a6989586621679758490 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromThenToSym2 a6989586621679758488 a6989586621679758489 :: TyFun a [a] -> Type) (a6989586621679758490 :: a) = EnumFromThenToSym3 a6989586621679758488 a6989586621679758489 a6989586621679758490

data EnumFromThenToSym1 a6989586621679758488 a6989586621679758489 Source #

Instances

Instances details

(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromThenToSym1 d) Source #
SuppressUnusedWarnings (EnumFromThenToSym1 a6989586621679758488 :: TyFun a (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
type Apply (EnumFromThenToSym1 a6989586621679758488 :: TyFun a (a ~> [a]) -> Type) (a6989586621679758489 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromThenToSym1 a6989586621679758488 :: TyFun a (a ~> [a]) -> Type) (a6989586621679758489 :: a) = EnumFromThenToSym2 a6989586621679758488 a6989586621679758489

data EnumFromThenToSym0 a6989586621679758488 Source #

Instances

Instances details

SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EnumFromThenToSym0 Source #
SuppressUnusedWarnings (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
type Apply (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) (a6989586621679758488 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) (a6989586621679758488 :: a) = EnumFromThenToSym1 a6989586621679758488

type EnumFromToSym2 (a6989586621679758482 :: a) (a6989586621679758483 :: a) = EnumFromTo a6989586621679758482 a6989586621679758483 :: [a] Source #

data EnumFromToSym1 a6989586621679758482 a6989586621679758483 Source #

Instances

Instances details

(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromToSym1 d) Source #
SuppressUnusedWarnings (EnumFromToSym1 a6989586621679758482 :: TyFun a [a] -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
type Apply (EnumFromToSym1 a6989586621679758482 :: TyFun a [a] -> Type) (a6989586621679758483 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromToSym1 a6989586621679758482 :: TyFun a [a] -> Type) (a6989586621679758483 :: a) = EnumFromToSym2 a6989586621679758482 a6989586621679758483

data EnumFromToSym0 a6989586621679758482 Source #

Instances

Instances details

SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EnumFromToSym0 Source #
SuppressUnusedWarnings (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
type Apply (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) (a6989586621679758482 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) (a6989586621679758482 :: a) = EnumFromToSym1 a6989586621679758482

type FromEnumSym1 (a6989586621679758478 :: a) = FromEnum a6989586621679758478 :: Nat Source #

data FromEnumSym0 a6989586621679758478 Source #

Instances

Instances details

SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing FromEnumSym0 Source #
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a Nat -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621679758478 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621679758478 :: a) = FromEnumSym1 a6989586621679758478

type ToEnumSym1 (a6989586621679758475 :: Nat) = ToEnum a6989586621679758475 :: a Source #

data ToEnumSym0 a6989586621679758475 Source #

Instances

Instances details

SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing ToEnumSym0 Source #
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () Source #
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621679758475 :: Nat) Source #
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621679758475 :: Nat) = ToEnumSym1 a6989586621679758475 :: k2

Singletons numbers

module Data.Singletons.Prelude.Num

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #

Exponentiation of type-level naturals.

Since: base-4.7.0.0

(%^) :: Sing a -> Sing b -> Sing (a ^ b) infixr 8 Source #

The singleton analogue of (^) for Nats.

Singleton `Show`

class PShow a Source #

Associated Types

type ShowsPrec (arg :: Nat) (arg :: a) (arg :: Symbol) :: Symbol Source #

type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_6989586621680279582Sym0 a) a) a

type Show_ (arg :: a) :: Symbol Source #

type Show_ a = Apply Show__6989586621680279594Sym0 a

type ShowList (arg :: [a]) (arg :: Symbol) :: Symbol Source #

type ShowList a a = Apply (Apply ShowList_6989586621680279602Sym0 a) a

Instances

Instances details

PShow Bool Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow Nat Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow () Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow Void Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow All Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow Any Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow [a] Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Option a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Identity Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (a, b) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Arg a b) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Proxy s) Source #
Instance details Defined in Data.Singletons.Prelude.Proxy Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (a, b, c) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (a, b, c, d) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (a, b, c, d, e) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (a, b, c, d, e, f) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
PShow (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #

class SShow a where 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 #

default sShowList :: forall (t :: [a]) (t :: Symbol). (Apply (Apply ShowListSym0 t) t :: Symbol) ~ Apply (Apply ShowList_6989586621680279602Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t :: Symbol) Source #

Instances

Instances details

SShow Bool Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Bool) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Bool). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Bool]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Ordering) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Ordering). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Ordering]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow Nat Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Nat) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Nat). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Nat]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow Symbol Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Symbol). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Symbol]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow () Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: ()) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: ()). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [()]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow Void Source #
Instance details 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 #
SShow Bool => SShow All Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sShowsPrec :: forall (t :: Nat) (t :: All) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: All). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [All]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow Bool => SShow Any Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sShowsPrec :: forall (t :: Nat) (t :: Any) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Any). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Any]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow a => SShow [a] Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: [a]) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: [a]). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [[a]]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow a => SShow (Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t :: Nat) (t :: Maybe a) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Maybe a). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Maybe a]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow a => SShow (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sShowsPrec :: forall (t :: Nat) (t :: Min a) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Min a). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Min a]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow a => SShow (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sShowsPrec :: forall (t :: Nat) (t :: Max a) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Max a). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Max a]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
SShow a => SShow (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sShowsPrec :: forall (t :: Nat) (t :: First a) (t :: Symbol). Sing t -> Sing t ->

'False \|\| a = a
'True \|\| a = 'True
a \|\| 'False = a
a \|\| 'True = 'True
a \|\| a = a

Basic singleton definitions

Singleton types

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Functions working with Bool

Error reporting

Singleton equality

Singleton comparisons

Instances

Instances

Singleton Enum and Bounded

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Singletons numbers

Singleton Show

Instances

Instances

Functions working with `Bool`

Singleton `Show`