morley-1.7.0: Developer tools for the Michelson Language
Safe HaskellNone
LanguageHaskell2010

Michelson.Typed.Scope

Description

Module, containing restrictions imposed by instruction or value scope.

Michelson have multiple restrictions on values, examples: * operation type cannot appear in parameter. * big_map type cannot appear in PUSH-able constants. * contract type cannot appear in type we UNPACK to.

Thus we declare multiple "scopes" - constraints applied in corresponding situations, for instance * ParameterScope; * StorageScope; * ConstantScope.

Also we separate multiple "classes" of scope-related constraints.

  • ParameterScope and similar ones are used within Michelson engine, they are understandable by GHC but produce not very clarifying errors.
  • ProperParameterBetterErrors and similar ones are middle-layer constraints, they produce human-readable errors but GHC cannot make conclusions from them. They are supposed to be used only by eDSLs to define their own high-level constraints.
  • Lorentz and other eDSLs may declare their own constraints, in most cases you should use them. For example see Constraints module.
Synopsis

Scopes

type ConstantScope t = (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t) Source #

Alias for constraints which Michelson applies to pushed constants.

type StorageScope t = (KnownT t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) Source #

Alias for constraints which Michelson applies to contract storage.

type PackedValScope t = (SingI t, HasNoOp t, HasNoBigMap t) Source #

Alias for constraints which Michelson applies to packed values.

type ParameterScope t = (KnownT t, HasNoOp t, HasNoNestedBigMaps t) Source #

Alias for constraints which Michelson applies to parameter.

type PrintedValScope t = (SingI t, HasNoOp t) Source #

Alias for constraints which are required for printing.

type UnpackedValScope t = (PackedValScope t, ConstantScope t) Source #

Alias for constraints which Michelson applies to unpacked values.

It is different from PackedValScope, e.g. contract type cannot appear in a value we unpack to.

newtype a :- b infixr 9 #

This is the type of entailment.

a :- b is read as a "entails" b.

With this we can actually build a category for Constraint resolution.

e.g.

Because Eq a is a superclass of Ord a, we can show that Ord a entails Eq a.

Because instance Ord a => Ord [a] exists, we can show that Ord a entails Ord [a] as well.

This relationship is captured in the :- entailment type here.

Since p :- p and entailment composes, :- forms the arrows of a Category of constraints. However, Category only became sufficiently general to support this instance in GHC 7.8, so prior to 7.8 this instance is unavailable.

But due to the coherence of instance resolution in Haskell, this Category has some very interesting properties. Notably, in the absence of IncoherentInstances, this category is "thin", which is to say that between any two objects (constraints) there is at most one distinguishable arrow.

This means that for instance, even though there are two ways to derive Ord a :- Eq [a], the answers from these two paths _must_ by construction be equal. This is a property that Haskell offers that is pretty much unique in the space of languages with things they call "type classes".

What are the two ways?

Well, we can go from Ord a :- Eq a via the superclass relationship, and then from Eq a :- Eq [a] via the instance, or we can go from Ord a :- Ord [a] via the instance then from Ord [a] :- Eq [a] through the superclass relationship and this diagram by definition must "commute".

Diagrammatically,

                   Ord a
               ins /     \ cls
                  v       v
            Ord [a]     Eq a
               cls \     / ins
                    v   v
                   Eq [a]

This safety net ensures that pretty much anything you can write with this library is sensible and can't break any assumptions on the behalf of library authors.

Constructors

Sub (a => Dict b) 

Instances

Instances details
Category (:-)

Possible since GHC 7.8, when Category was made polykinded.

Instance details

Defined in Data.Constraint

Methods

id :: forall (a :: k). a :- a #

(.) :: forall (b :: k) (c :: k) (a :: k). (b :- c) -> (a :- b) -> a :- c #

() :=> (Eq (a :- b)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Eq (a :- b) #

() :=> (Ord (a :- b)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Ord (a :- b) #

() :=> (Show (a :- b)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Show (a :- b) #

a => HasDict b (a :- b) 
Instance details

Defined in Data.Constraint

Methods

evidence :: (a :- b) -> Dict b #

Eq (a :- b)

Assumes IncoherentInstances doesn't exist.

Instance details

Defined in Data.Constraint

Methods

(==) :: (a :- b) -> (a :- b) -> Bool #

(/=) :: (a :- b) -> (a :- b) -> Bool #

(Typeable p, Typeable q, p, q) => Data (p :- q) 
Instance details

Defined in Data.Constraint

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> (p :- q) -> c (p :- q) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (p :- q) #

toConstr :: (p :- q) -> Constr #

dataTypeOf :: (p :- q) -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (p :- q)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (p :- q)) #

gmapT :: (forall b. Data b => b -> b) -> (p :- q) -> p :- q #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r #

gmapQ :: (forall d. Data d => d -> u) -> (p :- q) -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> (p :- q) -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) #

Ord (a :- b)

Assumes IncoherentInstances doesn't exist.

Instance details

Defined in Data.Constraint

Methods

compare :: (a :- b) -> (a :- b) -> Ordering #

(<) :: (a :- b) -> (a :- b) -> Bool #

(<=) :: (a :- b) -> (a :- b) -> Bool #

(>) :: (a :- b) -> (a :- b) -> Bool #

(>=) :: (a :- b) -> (a :- b) -> Bool #

max :: (a :- b) -> (a :- b) -> a :- b #

min :: (a :- b) -> (a :- b) -> a :- b #

Show (a :- b) 
Instance details

Defined in Data.Constraint

Methods

showsPrec :: Int -> (a :- b) -> ShowS #

show :: (a :- b) -> String #

showList :: [a :- b] -> ShowS #

a => NFData (a :- b) 
Instance details

Defined in Data.Constraint

Methods

rnf :: (a :- b) -> () #

data BadTypeForScope Source #

Instances

Instances details
Eq BadTypeForScope Source # 
Instance details

Defined in Michelson.Typed.Scope

Show BadTypeForScope Source # 
Instance details

Defined in Michelson.Typed.Scope

Generic BadTypeForScope Source # 
Instance details

Defined in Michelson.Typed.Scope

Associated Types

type Rep BadTypeForScope :: Type -> Type #

NFData BadTypeForScope Source # 
Instance details

Defined in Michelson.Typed.Scope

Methods

rnf :: BadTypeForScope -> () #

Buildable BadTypeForScope Source # 
Instance details

Defined in Michelson.Typed.Scope

type Rep BadTypeForScope Source # 
Instance details

Defined in Michelson.Typed.Scope

type Rep BadTypeForScope = D1 ('MetaData "BadTypeForScope" "Michelson.Typed.Scope" "morley-1.7.0-inplace" 'False) ((C1 ('MetaCons "BtNotComparable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BtIsOperation" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BtHasBigMap" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BtHasNestedBigMap" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BtHasContract" 'PrefixI 'False) (U1 :: Type -> Type))))

class CheckScope (c :: Constraint) where Source #

Should be present for common scopes.

Methods

checkScope :: Either BadTypeForScope (Dict c) Source #

Check that constraint hold for a given type.

Instances

Instances details
KnownT t => CheckScope (UnpackedValScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (PackedValScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (ConstantScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (StorageScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (ParameterScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

SingI t => CheckScope (HasNoNestedBigMaps t) Source # 
Instance details

Defined in Michelson.Typed.Scope

SingI t => CheckScope (HasNoBigMap t) Source # 
Instance details

Defined in Michelson.Typed.Scope

SingI t => CheckScope (HasNoContract t) Source # 
Instance details

Defined in Michelson.Typed.Scope

SingI t => CheckScope (HasNoOp t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (ComparabilityScope t) Source # 
Instance details

Defined in Michelson.Typed.Value

SingI t => CheckScope (Comparable t) Source # 
Instance details

Defined in Michelson.Typed.Value

Implementation internals

class ContainsBigMap t ~ 'False => HasNoBigMap t Source #

Constraint which ensures that bigmap does not appear in a given type.

class ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t Source #

Constraint which ensures that there are no nested bigmaps.

class ContainsOp t ~ 'False => HasNoOp t Source #

Constraint which ensures that operation type does not appear in a given type.

Not just a type alias in order to be able to partially apply it (e.g. in Each).

Instances

Instances details
ContainsOp t ~ 'False => HasNoOp t Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (UnpackedValScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (PackedValScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (ConstantScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (StorageScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (ParameterScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

SingI t => CheckScope (HasNoOp t) Source # 
Instance details

Defined in Michelson.Typed.Scope

class ContainsContract t ~ 'False => HasNoContract t Source #

Constraint which ensures that contract type does not appear in a given type.

Instances

Instances details
ContainsContract t ~ 'False => HasNoContract t Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (UnpackedValScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (ConstantScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (StorageScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

SingI t => CheckScope (HasNoContract t) Source # 
Instance details

Defined in Michelson.Typed.Scope

type family ContainsNestedBigMaps (t :: T) :: Bool where ... Source #

Whether this type contains a type with nested TBigMaps .

Nested big_maps (i.e. big_map which contains another big_map inside of it's value type). Are prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more strict because they doesn't work with big_map at all.

type ForbidOp t = FailOnOperationFound (ContainsOp t) Source #

This is like HasNoOp, it raises a more human-readable error when t type is concrete, but GHC cannot make any conclusions from such constraint as it can for HasNoOp. Though, hopefully, it will someday: #11503.

Use this constraint in our eDSL.

type ForbidContract t = FailOnContractFound (ContainsContract t) Source #

type family FailOnBigMapFound (enabled :: Bool) :: Constraint where ... Source #

Report a human-readable error about TBigMap at a wrong place.

Equations

FailOnBigMapFound 'True = TypeError ('Text "BigMaps are not allowed in this scope") 
FailOnBigMapFound 'False = () 

type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where ... Source #

Report a human-readable error that TBigMap contains another TBigMap

Equations

FailOnNestedBigMapsFound 'True = TypeError ('Text "Nested BigMaps are not allowed") 
FailOnNestedBigMapsFound 'False = () 

type family FailOnOperationFound (enabled :: Bool) :: Constraint where ... Source #

Report a human-readable error about TOperation at a wrong place.

Equations

FailOnOperationFound 'True = TypeError ('Text "Operations are not allowed in this scope") 
FailOnOperationFound 'False = () 

data OpPresence (t :: T) Source #

Whether the type contains TOperation, with proof.

Constructors

ContainsOp t ~ 'True => OpPresent 
ContainsOp t ~ 'False => OpAbsent 

data ContractPresence (t :: T) Source #

Constructors

ContainsContract t ~ 'True => ContractPresent 
ContainsContract t ~ 'False => ContractAbsent 

checkOpPresence :: Sing (ty :: T) -> OpPresence ty Source #

Check at runtime whether the given type contains TOperation.

checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty Source #

Check at runtime whether the given type contains TContract.

checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty Source #

Check at runtime whether the given type contains TBigMap.

checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty Source #

Check at runtime whether the given type contains TBigMap.

opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t) Source #

Check at runtime that the given type does not contain TOperation.

contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t) Source #

Check at runtime that the given type does not contain TContract.

bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t) Source #

Check at runtime that the given type does not containt TBigMap

nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t) Source #

Check at runtime that the given type does not contain nested TBigMap

forbiddenOp :: forall t a. (SingI t, ForbidOp t) => (HasNoOp t => a) -> a Source #

Reify HasNoOp contraint from ForbidOp.

Left for backward compatibility.

forbiddenContractType :: forall t a. (SingI t, ForbidContract t) => (HasNoContract t => a) -> a Source #

Reify HasNoContract contraint from ForbidContract.

forbiddenBigMap :: forall t a. (SingI t, ForbidBigMap t) => (HasNoBigMap t => a) -> a Source #

Re-exports

withDict :: HasDict c e => e -> (c => r) -> r #

From a Dict, takes a value in an environment where the instance witnessed by the Dict is in scope, and evaluates it.

Essentially a deconstruction of a Dict into its continuation-style form.

Can also be used to deconstruct an entailment, a :- b, using a context a.

withDict :: Dict c -> (c => r) -> r
withDict :: a => (a :- c) -> (c => r) -> r

class SingI (a :: k) where #

A SingI constraint is essentially an implicitly-passed singleton. If you need to satisfy this constraint with an explicit singleton, please see withSingI or the Sing pattern synonym.

Methods

sing :: Sing a #

Produce the singleton explicitly. You will likely need the ScopedTypeVariables extension to use this method the way you want.

Instances

Instances details
SingI 'Z Source # 
Instance details

Defined in Util.Peano

Methods

sing :: Sing 'Z #

SingI 'TKey Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TKey #

SingI 'TUnit Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TUnit #

SingI 'TSignature Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TSignature #

SingI 'TChainId Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TChainId #

SingI 'TOperation Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TOperation #

SingI 'TInt Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TInt #

SingI 'TNat Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TNat #

SingI 'TString Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TString #

SingI 'TBytes Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TBytes #

SingI 'TMutez Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TMutez #

SingI 'TBool Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TBool #

SingI 'TKeyHash Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TKeyHash #

SingI 'TTimestamp Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TTimestamp #

SingI 'TAddress Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TAddress #

(SingI n, KnownPeano n) => SingI ('S n :: Nat) Source # 
Instance details

Defined in Util.Peano

Methods

sing :: Sing ('S n) #

KnownT a => SingI ('TOption a :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TOption a) #

KnownT a => SingI ('TList a :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TList a) #

KnownT a => SingI ('TSet a :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TSet a) #

KnownT a => SingI ('TContract a :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TContract a) #

(KnownT a, KnownT b) => SingI ('TPair a b :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TPair a b) #

(KnownT a, KnownT b) => SingI ('TOr a b :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TOr a b) #

(KnownT a, KnownT b) => SingI ('TLambda a b :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TLambda a b) #

(KnownT a, KnownT b) => SingI ('TMap a b :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TMap a b) #

(KnownT a, KnownT b) => SingI ('TBigMap a b :: T) Source # 
Instance details

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TBigMap a b) #

KnownT t => CheckScope (UnpackedValScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (PackedValScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

KnownT t => CheckScope (ConstantScope t) Source # 
Instance details

Defined in Michelson.Typed.Scope

SingI NotSym0 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing NotSym0 #

SingI (||@#@$) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (||@#@$) #

SingI (&&@#@$) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (&&@#@$) #

SingI Log2Sym0 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing Log2Sym0 #

SingI (<=?@#@$) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing (<=?@#@$) #

SingI ModSym0 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing ModSym0 #

SingI DivSym0 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing DivSym0 #

SingI (^@#@$) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing (^@#@$) #

SingI AllSym0 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing AllSym0 #

SingI AnySym0 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing AnySym0 #

SingI ShowParenSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI OrSym0 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing OrSym0 #

SingI AndSym0 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AndSym0 #

SingI UnwordsSym0 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI UnlinesSym0 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI Show_tupleSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_tupleSym0 #

SingI ThenCmpSym0 
Instance details

Defined in Data.Singletons.Prelude.Ord

SingI EftNatSym0 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EftNatSym0 #

SingI EfdtNatSym0 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatSym0 #

SingI EfdtNatDnSym0 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatDnSym0 #

SingI EfdtNatUpSym0 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatUpSym0 #

SingI ShowCommaSpaceSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI ShowSpaceSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI ShowStringSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI ShowCharSym0 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI x => SingI ((||@#@$$) x :: TyFun Bool Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing ((||@#@$$) x) #

SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing ((&&@#@$$) x) #

SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ((<=?@#@$$) x) #

SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type) 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x) #

SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type) 
Instance details

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x) #

SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ((^@#@$$) x) #

SAlternative f => SingI (GuardSym0 :: TyFun Bool (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing GuardSym0 #

SApplicative f => SingI (WhenSym0 :: TyFun Bool (f () ~> f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing WhenSym0 #

SingI (ListtransposeSym0 :: TyFun [[a]] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListtransposeSym0 #

SingI (TransposeSym0 :: TyFun [[a]] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (ConcatSym0 :: TyFun [[a]] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ConcatSym0 #

SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

SingI (ListtailsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListtailsSym0 #

SNum a => SingI (ListsumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListsumSym0 #

SOrd a => SingI (ListsortSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListsortSym0 #

SingI (ListreverseSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListreverseSym0 #

SNum a => SingI (ListproductSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListproductSym0 #

SingI (ListnullSym0 :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListnullSym0 #

SOrd a => SingI (ListminimumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListminimumSym0 #

SOrd a => SingI (ListmaximumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListmaximumSym0 #

SingI (ListlengthSym0 :: TyFun [a] Nat -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListlengthSym0 #

SingI (ListlastSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListlastSym0 #

SEq a => SingI (ListisPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListisPrefixOfSym0 #

SingI (ListinitsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListinitsSym0 #

SingI (ListinitSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListinitSym0 #

SingI (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListindexSym0 #

SEq a => SingI ((\\@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (\\@#@$) #

SEq a => SingI (UnionSym0 :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnionSym0 #

SingI (TailsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TailsSym0 #

SingI (TailSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TailSym0 #

SNum a => SingI (SumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SumSym0 #

SingI (SubsequencesSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SOrd a => SingI (SortSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SortSym0 #

SingI (ReverseSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SNum a => SingI (ProductSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ProductSym0 #

SingI (PermutationsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (NullSym0 :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NullSym0 #

SEq a => SingI (NubSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NubSym0 #

SingI (NonEmptySubsequencesSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NonEmptySubsequencesSym0 #

SOrd a => SingI (MinimumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MinimumSym0 #

SOrd a => SingI (MaximumSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MaximumSym0 #

SingI (LengthSym0 :: TyFun [a] Nat -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LengthSym0 #

SingI (LastSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LastSym0 #

SEq a => SingI (IsSuffixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SEq a => SingI (IsPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SEq a => SingI (IsInfixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SEq a => SingI (IntersectSym0 :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (IntercalateSym0 :: TyFun [a] ([[a]] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (InitsSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InitsSym0 #

SingI (InitSym0 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InitSym0 #

SingI (HeadSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing HeadSym0 #

SEq a => SingI (GroupSym0 :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GroupSym0 #

SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (!!@#@$) #

SingI ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (++@#@$) #

SMonoid a => SingI (MconcatSym0 :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing IsJustSym0 #

SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

SingI (OptionSym0 :: TyFun (Maybe a) (Option a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing OptionSym0 #

SingI (LastSym0 :: TyFun (Maybe a) (Last a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing LastSym0 #

SingI (FirstSym0 :: TyFun (Maybe a) (First a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing FirstSym0 #

SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ThenCmpSym1 d) #

SingI d => SingI (EftNatSym1 d :: TyFun Nat [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EftNatSym1 d) #

SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing ToEnumSym0 #

SingI (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListtakeSym0 #

SingI (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListsplitAtSym0 #

SingI (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListdropSym0 #

SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeSym0 #

SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropSym0 #

SingI d => SingI (EfdtNatSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatSym1 d) #

SingI d => SingI (EfdtNatDnSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatDnSym1 d) #

SingI d => SingI (EfdtNatUpSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatUpSym1 d) #

SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowStringSym1 d) #

SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowCharSym1 d) #

SingI d => SingI (Show_tupleSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (Show_tupleSym1 d) #

SIsString a => SingI (FromStringSym0 :: TyFun Symbol a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.IsString

SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsSym0 #

SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_Sym0 #

SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

SNum a => SingI (SignumSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SignumSym0 #

SNum a => SingI (NegateSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing NegateSym0 #

SNum a => SingI (AbsSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing AbsSym0 #

SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (-@#@$) #

SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (+@#@$) #

SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (*@#@$) #

SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

SingI (ListintersperseSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListintersperseSym0 #

SOrd a => SingI (ListinsertSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListinsertSym0 #

SEq a => SingI (ListelemSym0 :: TyFun a ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListelemSym0 #

SingI (PrependToAllSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PrependToAllSym0 #

SEq a => SingI (NotElemSym0 :: TyFun a ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NotElemSym0 #

SingI (IntersperseSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SOrd a => SingI (InsertSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InsertSym0 #

SEq a => SingI (ElemSym0 :: TyFun a ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemSym0 #

SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SEq a => SingI (DeleteSym0 :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteSym0 #

SFoldable t => SingI (OrSym0 :: TyFun (t Bool) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing OrSym0 #

SFoldable t => SingI (AndSym0 :: TyFun (t Bool) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AndSym0 #

SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

sing :: Sing (==@#@$) #

SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

sing :: Sing (/=@#@$) #

SEnum a => SingI (SuccSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing SuccSym0 #

SEnum a => SingI (PredSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing PredSym0 #

SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing Bool_Sym0 #

SingI (IdSym0 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing IdSym0 #

SingI (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

SingI (JustSym0 :: TyFun a (Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing JustSym0 #

SingI (IdentitySym0 :: TyFun a (Identity a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

SingI ((:|@#@$) :: TyFun a ([a] ~> NonEmpty a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (:|@#@$) #

SingI ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (:@#@$) #

SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MinSym0 #

SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MaxSym0 #

SingI (DownSym0 :: TyFun a (Down a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing DownSym0 #

SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>@#@$) #

SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>=@#@$) #

SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<@#@$) #

SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<=@#@$) #

SingI (WrapMonoidSym0 :: TyFun m (WrappedMonoid m) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SingI (SumSym0 :: TyFun a (Sum a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing SumSym0 #

SingI (ProductSym0 :: TyFun a (Product a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SingI (MinSym0 :: TyFun a (Min a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing MinSym0 #

SingI (MaxSym0 :: TyFun a (Max a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing MaxSym0 #

SingI (LastSym0 :: TyFun a (Last a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing LastSym0 #

SingI (FirstSym0 :: TyFun a (First a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing FirstSym0 #

SingI (DualSym0 :: TyFun a (Dual a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing DualSym0 #

SSemigroup a => SingI ((<>@#@$) :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing (<>@#@$) #

SMonoid a => SingI (MappendSym0 :: TyFun a (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

SSemigroup a => SingI (SconcatSym0 :: TyFun (NonEmpty a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym1 d) #

SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

SingI (ListtakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListtakeWhileSym0 #

SingI (ListspanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListspanSym0 #

SingI (ListsortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListsortBySym0 #

SingI (Listscanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing Listscanr1Sym0 #

SingI (ListpartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListpartitionSym0 #

SingI (ListnubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListnubBySym0 #

SingI (Listfoldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing Listfoldr1Sym0 #

SingI (Listfoldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing Listfoldl1Sym0 #

SingI (ListfilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListfilterSym0 #

SingI (ListdropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListdropWhileSym0 #

SingI (UnionBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (TakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (SpanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SpanSym0 #

SingI (SortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SortBySym0 #

SingI (SelectSym0 :: TyFun (a ~> Bool) (a ~> (([a], [a]) ~> ([a], [a]))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SelectSym0 #

SingI (Scanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Scanr1Sym0 #

SingI (Scanl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Scanl1Sym0 #

SingI (PartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (NubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NubBySym0 #

SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MinimumBySym0 #

SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MaximumBySym0 #

SingI (IntersectBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (InsertBySym0 :: TyFun (a ~> (a ~> Ordering)) (a ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (GroupBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [[a]]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldr1Sym0 #

SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl1Sym0 #

SingI (Foldl1'Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (FindSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindSym0 #

SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (FilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FilterSym0 #

SingI (Elem_bySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> Bool)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Elem_bySym0 #

SingI (DropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (DropWhileEndSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (DeleteFirstsBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (DeleteBySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (BreakSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing BreakSym0 #

SingI (AnySym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AnySym0 #

SingI (AllSym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AllSym0 #

SingI (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing UntilSym0 #

SingI d => SingI (IntercalateSym1 d :: TyFun [[a]] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntercalateSym1 d) #

SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing RightsSym0 #

SingI (PartitionEithersSym0 :: TyFun [Either a b] ([a], [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing PartitionEithersSym0 #

SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing LeftsSym0 #

SingI (ListunzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListunzipSym0 #

SingI (UnzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnzipSym0 #

SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym1 d) #

SingI (ListzipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListzipSym0 #

SingI d => SingI (ListtakeWhileSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListtakeWhileSym1 d) #

SingI d => SingI (ListtakeSym1 d a :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListtakeSym1 d a) #

SingI d => SingI (ListsplitAtSym1 d a :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListsplitAtSym1 d a) #

SingI d => SingI (ListspanSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListspanSym1 d) #

SingI d => SingI (ListsortBySym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListsortBySym1 d) #

SingI d => SingI (Listscanr1Sym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listscanr1Sym1 d) #

SingI d => SingI (ListpartitionSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListpartitionSym1 d) #

SingI d => SingI (ListnubBySym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListnubBySym1 d) #

(SEq a, SingI d) => SingI (ListisPrefixOfSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListisPrefixOfSym1 d) #

SingI d => SingI (ListintersperseSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListintersperseSym1 d) #

(SOrd a, SingI d) => SingI (ListinsertSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListinsertSym1 d) #

SingI d => SingI (Listfoldr1Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listfoldr1Sym1 d) #

SingI d => SingI (Listfoldl1Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl1Sym1 d) #

SingI d => SingI (ListfilterSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfilterSym1 d) #

(SEq a, SingI d) => SingI (ListelemSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListelemSym1 d) #

SingI d => SingI (ListdropWhileSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListdropWhileSym1 d) #

SingI d => SingI (ListdropSym1 d a :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListdropSym1 d a) #

(SEq a, SingI d) => SingI ((\\@#@$$) d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ((\\@#@$$) d) #

SingI (ZipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipSym0 #

(SEq a, SingI d) => SingI (UnionSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionSym1 d) #

SingI d => SingI (UnionBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionBySym1 d) #

SingI d => SingI (TakeWhileSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (TakeWhileSym1 d) #

SingI d => SingI (TakeSym1 d a :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (TakeSym1 d a) #

SingI d => SingI (SplitAtSym1 d a :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SplitAtSym1 d a) #

SingI d => SingI (SpanSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SpanSym1 d) #

SingI d => SingI (SortBySym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SortBySym1 d) #

SingI d => SingI (Scanr1Sym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Scanr1Sym1 d) #

SingI d => SingI (Scanl1Sym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Scanl1Sym1 d) #

SingI d => SingI (PrependToAllSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (PrependToAllSym1 d) #

SingI d => SingI (PartitionSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (PartitionSym1 d) #

SingI d => SingI (NubBySym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (NubBySym1 d) #

(SEq a, SingI d) => SingI (NotElemSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (NotElemSym1 d) #

SingI d => SingI (MinimumBySym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MinimumBySym1 d) #

SingI d => SingI (MaximumBySym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MaximumBySym1 d) #

(SEq a, SingI d) => SingI (IsSuffixOfSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsSuffixOfSym1 d) #

(SEq a, SingI d) => SingI (IsPrefixOfSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsPrefixOfSym1 d) #

(SEq a, SingI d) => SingI (IsInfixOfSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsInfixOfSym1 d) #

SingI d => SingI (IntersperseSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersperseSym1 d) #

(SEq a, SingI d) => SingI (IntersectSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectSym1 d) #

SingI d => SingI (IntersectBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectBySym1 d) #

(SOrd a, SingI d) => SingI (InsertSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertSym1 d) #

SingI d => SingI (GroupBySym1 d :: TyFun [a] [[a]] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (GroupBySym1 d) #

SNum i => SingI (GenericLengthSym0 :: TyFun [a] i -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI d => SingI (Foldr1Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldr1Sym1 d) #

SingI d => SingI (Foldl1Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl1Sym1 d) #

SingI d => SingI (Foldl1'Sym1 d :: TyFun [a] a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl1'Sym1 d) #

SingI d => SingI (FindSym1 d :: TyFun [a] (Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindSym1 d) #

SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndicesSym1 d) #

SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndexSym1 d) #

SingI d => SingI (FilterSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FilterSym1 d) #

(SEq a, SingI d) => SingI (ElemSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemSym1 d) #

(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndicesSym1 d) #

(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndexSym1 d) #

SingI d => SingI (DropWhileSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropWhileSym1 d) #

SingI d => SingI (DropWhileEndSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropWhileEndSym1 d) #

SingI d => SingI (DropSym1 d a :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropSym1 d a) #

(SEq a, SingI d) => SingI (DeleteSym1 d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteSym1 d) #

SingI d => SingI (DeleteFirstsBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI d => SingI (BreakSym1 d :: TyFun [a] ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (BreakSym1 d) #

SingI d => SingI (AnySym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (AnySym1 d) #

SingI d => SingI (AllSym1 d :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (AllSym1 d) #

SingI d => SingI ((++@#@$$) d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ((++@#@$$) d) #

SingI d => SingI ((:|@#@$$) d :: TyFun [a] (NonEmpty a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing ((:|@#@$$) d) #

SingI d => SingI ((:@#@$$) d :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing ((:@#@$$) d) #

SingI d => SingI (FromMaybeSym1 d :: TyFun (Maybe a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (FromMaybeSym1 d) #

SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing IsLeftSym0 #

(SingI d1, SingI d2) => SingI (EfdtNatSym2 d1 d2 :: TyFun Nat [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (EfdtNatDnSym2 d1 d2 :: TyFun Nat [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatDnSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (EfdtNatUpSym2 d1 d2 :: TyFun Nat [Nat] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatUpSym2 d1 d2) #

SingI d => SingI (ListindexSym1 d :: TyFun Nat a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListindexSym1 d) #

SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ((!!@#@$$) d) #

(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym2 d1 d2) #

(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsSym1 d) #

(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListSym1 d) #

SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

SingI (ErrorSym0 :: TyFun Symbol a -> Type) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorSym0 #

SingI (SwapSym0 :: TyFun (a, b) (b, a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing SwapSym0 #

SingI (SndSym0 :: TyFun (a, b) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing SndSym0 #

SingI (FstSym0 :: TyFun (a, b) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing FstSym0 #

(SShow a, SingI d) => SingI (ShowsPrecSym1 d a :: TyFun a (Symbol ~> Symbol) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym1 d a) #

(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (SubtractSym1 d) #

(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((-@#@$$) d) #

(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((+@#@$$) d) #

(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing ((*@#@$$) d) #

SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing Maybe_Sym0 #

SingI d => SingI (SelectSym1 d :: TyFun a (([a], [a]) ~> ([a], [a])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SelectSym1 d) #

SingI d => SingI (ReplicateSym1 d a :: TyFun a [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ReplicateSym1 d a) #

SEq a => SingI (LookupSym0 :: TyFun a ([(a, b)] ~> Maybe b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LookupSym0 #

SingI d => SingI (InsertBySym1 d :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertBySym1 d) #

SingI d => SingI (Elem_bySym1 d :: TyFun a ([a] ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Elem_bySym1 d) #

SingI d => SingI (DeleteBySym1 d :: TyFun a ([a] ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteBySym1 d) #

(SApplicative f, SingI d) => SingI (WhenSym1 d f :: TyFun (f ()) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (WhenSym1 d f) #

SMonad m => SingI (ReturnSym0 :: TyFun a (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ReturnSym0 #

SApplicative f => SingI (PureSym0 :: TyFun a (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing PureSym0 #

SMonad m => SingI (JoinSym0 :: TyFun (m (m a)) (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing JoinSym0 #

SFoldable t => SingI (ToListSym0 :: TyFun (t a) [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ToListSym0 #

(SFoldable t, SNum a) => SingI (SumSym0 :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing SumSym0 #

(SFoldable t, SNum a) => SingI (ProductSym0 :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

(SFoldable t, SEq a) => SingI (NotElemSym0 :: TyFun a (t a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

(SFoldable t, SOrd a) => SingI (MinimumSym0 :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

(SFoldable t, SOrd a) => SingI (MaximumSym0 :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

(SFoldable t, SMonoid m) => SingI (FoldSym0 :: TyFun (t m) m -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldSym0 #

(SFoldable t, SEq a) => SingI (ElemSym0 :: TyFun a (t a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ElemSym0 #

SFoldable t => SingI (ConcatSym0 :: TyFun (t [a]) [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ConcatSym0 #

(SEq a, SingI x) => SingI ((==@#@$$) x :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

sing :: Sing ((==@#@$$) x) #

(SEq a, SingI x) => SingI ((/=@#@$$) x :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Eq

Methods

sing :: Sing ((/=@#@$$) x) #

(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromToSym1 d) #

(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (Bool_Sym1 d) #

SingI (SeqSym0 :: TyFun a (b ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing SeqSym0 #

SingI (ConstSym0 :: TyFun a (b ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ConstSym0 #

SingI d => SingI (AsTypeOfSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (AsTypeOfSym1 d) #

SingI (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple2Sym0 #

SingI (RightSym0 :: TyFun b (Either a b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing RightSym0 #

SingI (LeftSym0 :: TyFun a (Either a b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing LeftSym0 #

(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MinSym1 d) #

(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MaxSym1 d) #

(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (CompareSym1 d) #

(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((>@#@$$) d) #

(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((>=@#@$$) d) #

(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((<@#@$$) d) #

(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((<=@#@$$) d) #

(SSemigroup a, SingI d) => SingI ((<>@#@$$) d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing ((<>@#@$$) d) #

(SMonoid a, SingI d) => SingI (MappendSym1 d :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing (MappendSym1 d) #

SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing VoidSym0 #

SingI (Option_Sym0 :: TyFun b ((a ~> b) ~> (Option a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing Option_Sym0 #

SingI (ArgSym0 :: TyFun a (b ~> Arg a b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing ArgSym0 #

SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

SingI (ListscanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListscanrSym0 #

SingI (ListscanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListscanlSym0 #

SingI (ListmapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListmapSym0 #

SingI (ListfoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListfoldrSym0 #

SingI (ListfoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListfoldlSym0 #

SingI (Listfoldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing Listfoldl'Sym0 #

SingI (UnfoldrSym0 :: TyFun (b ~> Maybe (a, b)) (b ~> [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (ScanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ScanrSym0 #

SingI (ScanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ScanlSym0 #

SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl'Sym0 #

SingI (ConcatMapSym0 :: TyFun (a ~> [b]) ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ConcatMapSym0 #

SFoldable t => SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

SFoldable t => SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

SFoldable t => SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldr1Sym0 #

SFoldable t => SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldl1Sym0 #

SFoldable t => SingI (FindSym0 :: TyFun (a ~> Bool) (t a ~> Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FindSym0 #

SFoldable t => SingI (AnySym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AnySym0 #

SFoldable t => SingI (AllSym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AllSym0 #

SingI d => SingI (UntilSym1 d :: TyFun (a ~> a) (a ~> a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (UntilSym1 d) #

SingI (MapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing MapSym0 #

SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing FoldrSym0 #

SingI (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ($@#@$) #

SingI (($!@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ($!@#@$) #

SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing FoldlSym0 #

SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

SingI (ConstSym0 :: TyFun a6989586621679091300 (Const a6989586621679091300 b6989586621679091301) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Const

Methods

sing :: Sing ConstSym0 #

SingI a => SingI ('WrapSing s :: WrappedSing a) 
Instance details

Defined in Data.Singletons.Internal

Methods

sing :: Sing ('WrapSing s) #

(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (Bool_Sym2 d1 d2) #

(SEq a, SingI d) => SingI (LookupSym1 d b :: TyFun [(a, b)] (Maybe b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (LookupSym1 d b) #

SingI (Unzip3Sym0 :: TyFun [(a, b, c)] ([a], [b], [c]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip3Sym0 #

SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (MapMaybeSym1 d) #

SingI d => SingI (ListzipSym1 d b :: TyFun [b] [(a, b)] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListzipSym1 d b) #

SingI d => SingI (ListmapSym1 d :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListmapSym1 d) #

SingI d => SingI (ZipSym1 d b :: TyFun [b] [(a, b)] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipSym1 d b) #

SingI (Zip3Sym0 :: TyFun [a] ([b] ~> ([c] ~> [(a, b, c)])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Zip3Sym0 #

(SingI d1, SingI d2) => SingI (UnionBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionBySym2 d1 d2) #

(SingI d1, SingI d2) => SingI (IntersectBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectBySym2 d1 d2) #

(SingI d1, SingI d2) => SingI (InsertBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertBySym2 d1 d2) #

(SingI d1, SingI d2) => SingI (Elem_bySym2 d1 d2 :: TyFun [a] Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Elem_bySym2 d1 d2) #

(SingI d1, SingI d2) => SingI (DeleteFirstsBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteFirstsBySym2 d1 d2) #

(SingI d1, SingI d2) => SingI (DeleteBySym2 d1 d2 :: TyFun [a] [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteBySym2 d1 d2) #

SingI d => SingI (ConcatMapSym1 d :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ConcatMapSym1 d) #

SingI d => SingI (MapSym1 d :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (MapSym1 d) #

(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym2 d1 d2) #

(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (SelectSym2 d1 d2 :: TyFun ([a], [a]) ([a], [a]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SelectSym2 d1 d2) #

(STraversable t, SMonad m) => SingI (SequenceSym0 :: TyFun (t (m a)) (m (t a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

(STraversable t, SApplicative f) => SingI (SequenceASym0 :: TyFun (t (f a)) (f (t a)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

SingI d => SingI (ListscanrSym1 d :: TyFun b ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListscanrSym1 d) #

SingI d => SingI (ListscanlSym1 d :: TyFun b ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListscanlSym1 d) #

SingI d => SingI (ListfoldrSym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfoldrSym1 d) #

SingI d => SingI (ListfoldlSym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfoldlSym1 d) #

SingI d => SingI (Listfoldl'Sym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl'Sym1 d) #

SingI d => SingI (UnfoldrSym1 d :: TyFun b [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnfoldrSym1 d) #

SingI d => SingI (ScanrSym1 d :: TyFun b ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanrSym1 d) #

SingI d => SingI (ScanlSym1 d :: TyFun b ([a] ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanlSym1 d) #

SingI d => SingI (Foldl'Sym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl'Sym1 d) #

SMonadPlus m => SingI (MplusSym0 :: TyFun (m a) (m a ~> m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing MplusSym0 #

SMonad m => SingI (ApSym0 :: TyFun (m (a ~> b)) (m a ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ApSym0 #

SMonad m => SingI ((>>=@#@$) :: TyFun (m a) ((a ~> m b) ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (>>=@#@$) #

SAlternative f => SingI ((<|>@#@$) :: TyFun (f a) (f a ~> f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<|>@#@$) #

SApplicative f => SingI ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<*>@#@$) #

SApplicative f => SingI ((<**>@#@$) :: TyFun (f a) (f (a ~> b) ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<**>@#@$) #

SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<$@#@$) #

(SFoldable t, SMonad m) => SingI (Sequence_Sym0 :: TyFun (t (m a)) (m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

(SFoldable t, SApplicative f) => SingI (SequenceA_Sym0 :: TyFun (t (f a)) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

SFoldable t => SingI (NullSym0 :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing NullSym0 #

(SFoldable t, SEq a, SingI d) => SingI (NotElemSym1 d t :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (NotElemSym1 d t) #

(SFoldable t, SingI d) => SingI (MinimumBySym1 d t :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (MinimumBySym1 d t) #

(SFoldable t, SingI d) => SingI (MaximumBySym1 d t :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (MaximumBySym1 d t) #

SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing LengthSym0 #

(SFoldable t, SingI d) => SingI (Foldr1Sym1 d t :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldr1Sym1 d t) #

(SFoldable t, SingI d) => SingI (Foldl1Sym1 d t :: TyFun (t a) a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldl1Sym1 d t) #

(SFoldable t, SingI d) => SingI (FindSym1 d t :: TyFun (t a) (Maybe a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FindSym1 d t) #

(SFoldable t, SEq a, SingI d) => SingI (ElemSym1 d t :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (ElemSym1 d t) #

(SFoldable t, SingI d) => SingI (AnySym1 d t :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (AnySym1 d t) #

(SFoldable t, SingI d) => SingI (AllSym1 d t :: TyFun (t a) Bool -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (AllSym1 d t) #

(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromThenToSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (UntilSym2 d1 d2 :: TyFun a a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (UntilSym2 d1 d2) #

SingI d => SingI (SeqSym1 d b :: TyFun b b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (SeqSym1 d b) #

SingI d => SingI (FoldrSym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FoldrSym1 d) #

SingI d => SingI (ConstSym1 d b :: TyFun b a -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (ConstSym1 d b) #

SingI d => SingI (($@#@$$) d :: TyFun a b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (($@#@$$) d) #

SingI d => SingI (($!@#@$$) d :: TyFun a b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (($!@#@$$) d) #

SingI (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple3Sym0 #

SingI d => SingI (Tuple2Sym1 d b :: TyFun b (a, b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple2Sym1 d b) #

SingI d => SingI (FoldlSym1 d :: TyFun b ([a] ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (FoldlSym1 d) #

(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ComparingSym1 d) #

SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (<&>@#@$) #

SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing ($>@#@$) #

SingI d => SingI (ArgSym1 d b :: TyFun b (Arg a b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing (ArgSym1 d b) #

SingI (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing CurrySym0 #

SingI (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

(STraversable t, SMonoid m) => SingI (FoldMapDefaultSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

STraversable t => SingI (FmapDefaultSym0 :: TyFun (a ~> b) (t a ~> t b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

SingI d => SingI (Maybe_Sym1 d a :: TyFun (a ~> b) (Maybe a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (Maybe_Sym1 d a) #

SingI (ListzipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing ListzipWithSym0 #

SingI (ZipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SingI (MapAccumRSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MapAccumRSym0 #

SingI (MapAccumLSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MapAccumLSym0 #

SMonad m => SingI (LiftMSym0 :: TyFun (a1 ~> r) (m a1 ~> m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftMSym0 #

SApplicative f => SingI (LiftASym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftASym0 #

SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing FmapSym0 #

SMonad m => SingI ((=<<@#@$) :: TyFun (a ~> m b) (m a ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (=<<@#@$) #

SFoldable t => SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldrSym0 #

SFoldable t => SingI (Foldr'Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldr'Sym0 #

SFoldable t => SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldlSym0 #

SFoldable t => SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldl'Sym0 #

(SFoldable t, SMonoid m) => SingI (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

SFoldable t => SingI (ConcatMapSym0 :: TyFun (a ~> [b]) (t a ~> [b]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

SingI (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing FlipSym0 #

SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (.@#@$) #

SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (<$>@#@$) #

SingI d => SingI (Option_Sym1 d a :: TyFun (a ~> b) (Option a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing (Option_Sym1 d a) #

SingI (Unzip4Sym0 :: TyFun [(a, b, c, d)] ([a], [b], [c], [d]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip4Sym0 #

SingI d => SingI (ListzipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListzipWithSym1 d) #

(SingI d1, SingI d2) => SingI (ListscanrSym2 d1 d2 :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListscanrSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (ListscanlSym2 d1 d2 :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListscanlSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (ListfoldrSym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfoldrSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (ListfoldlSym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListfoldlSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (Listfoldl'Sym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl'Sym2 d1 d2) #

SingI d => SingI (ZipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWithSym1 d) #

SingI d => SingI (Zip3Sym1 d b c :: TyFun [b] ([c] ~> [(a, b, c)]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Zip3Sym1 d b c) #

(SingI d1, SingI d2) => SingI (ScanrSym2 d1 d2 :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanrSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (ScanlSym2 d1 d2 :: TyFun [a] [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanlSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl'Sym2 d1 d2) #

(SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FoldrSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 :: TyFun [a] b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (FoldlSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (Maybe_Sym2 d1 d2 :: TyFun (Maybe a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (Maybe_Sym2 d1 d2) #

SingI d => SingI (UncurrySym1 d :: TyFun (a, b) c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing (UncurrySym1 d) #

SingI d => SingI (CurrySym1 d :: TyFun a (b ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing (CurrySym1 d) #

(STraversable t, SApplicative f) => SingI (ForSym0 :: TyFun (t a) ((a ~> f b) ~> f (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing ForSym0 #

(STraversable t, SMonad m) => SingI (ForMSym0 :: TyFun (t a) ((a ~> m b) ~> m (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing ForMSym0 #

(STraversable t, SMonoid m, SingI d) => SingI (FoldMapDefaultSym1 d t :: TyFun (t a) m -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (FoldMapDefaultSym1 d t) #

(STraversable t, SingI d) => SingI (FmapDefaultSym1 d t :: TyFun (t a) (t b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (FmapDefaultSym1 d t) #

SingI d => SingI (MapAccumRSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumRSym1 d) #

SingI d => SingI (MapAccumLSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumLSym1 d) #

(SMonadPlus m, SingI d) => SingI (MplusSym1 d :: TyFun (m a) (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (MplusSym1 d) #

(SMonad m, SingI d) => SingI (LiftMSym1 d m :: TyFun (m a1) (m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftMSym1 d m) #

(SApplicative f, SingI d) => SingI (LiftASym1 d f :: TyFun (f a) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftASym1 d f) #

(SFunctor f, SingI d) => SingI (FmapSym1 d f :: TyFun (f a) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (FmapSym1 d f) #

(SMonad m, SingI d) => SingI (ApSym1 d :: TyFun (m a) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (ApSym1 d) #

SMonad m => SingI ((>>@#@$) :: TyFun (m a) (m b ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (>>@#@$) #

(SMonad m, SingI d) => SingI ((=<<@#@$$) d :: TyFun (m a) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((=<<@#@$$) d) #

(SAlternative f, SingI d) => SingI ((<|>@#@$$) d :: TyFun (f a) (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((<|>@#@$$) d) #

SApplicative f => SingI ((<*@#@$) :: TyFun (f a) (f b ~> f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (<*@#@$) #

(SApplicative f, SingI d) => SingI ((<*>@#@$$) d :: TyFun (f a) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((<*>@#@$$) d) #

(SApplicative f, SingI d) => SingI (d <**>@#@$$ b :: TyFun (f (a ~> b)) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d <**>@#@$$ b) #

(SFunctor f, SingI d) => SingI ((d <$@#@$$ f) b :: TyFun (f b) (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ((d <$@#@$$ f) b) #

SApplicative f => SingI ((*>@#@$) :: TyFun (f a) (f b ~> f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (*>@#@$) #

(SFoldable t, SMonadPlus m) => SingI (MsumSym0 :: TyFun (t (m a)) (m a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MsumSym0 #

(SFoldable t, SApplicative f) => SingI (For_Sym0 :: TyFun (t a) ((a ~> f b) ~> f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing For_Sym0 #

(SFoldable t, SMonad m) => SingI (ForM_Sym0 :: TyFun (t a) ((a ~> m b) ~> m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ForM_Sym0 #

(SFoldable t, SingI d) => SingI (FoldrSym1 d t :: TyFun b (t a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldrSym1 d t) #

(SFoldable t, SingI d) => SingI (Foldr'Sym1 d t :: TyFun b (t a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldr'Sym1 d t) #

(SFoldable t, SingI d) => SingI (FoldlSym1 d t :: TyFun b (t a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldlSym1 d t) #

(SFoldable t, SingI d) => SingI (Foldl'Sym1 d t :: TyFun b (t a ~> b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldl'Sym1 d t) #

(SFoldable t, SMonoid m, SingI d) => SingI (FoldMapSym1 d t :: TyFun (t a) m -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldMapSym1 d t) #

(SFoldable t, SingI d) => SingI (ConcatMapSym1 d t :: TyFun (t a) [b] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (ConcatMapSym1 d t) #

(SFoldable t, SAlternative f) => SingI (AsumSym0 :: TyFun (t (f a)) (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AsumSym0 #

SingI d => SingI (FlipSym1 d :: TyFun b (a ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FlipSym1 d) #

SingI (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple4Sym0 #

SingI d => SingI (Tuple3Sym1 d b c :: TyFun b (c ~> (a, b, c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple3Sym1 d b c) #

(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ComparingSym2 d1 d2) #

(SFunctor f, SingI d) => SingI (d <$>@#@$$ f :: TyFun (f a) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (d <$>@#@$$ f) #

(SFunctor f, SingI d) => SingI (d $>@#@$$ b :: TyFun b (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (d $>@#@$$ b) #

(SingI d1, SingI d2) => SingI (Option_Sym2 d1 d2 :: TyFun (Option a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing (Option_Sym2 d1 d2) #

(STraversable t, SApplicative f) => SingI (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

(STraversable t, SMonad m) => SingI (MapMSym0 :: TyFun (a ~> m b) (t a ~> m (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing MapMSym0 #

STraversable t => SingI (MapAccumRSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

STraversable t => SingI (MapAccumLSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

SingI (ZipWith3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) ([a] ~> ([b] ~> ([c] ~> [d]))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

SMonad m => SingI (LiftM2Sym0 :: TyFun (a1 ~> (a2 ~> r)) (m a1 ~> (m a2 ~> m r)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftM2Sym0 #

SApplicative f => SingI (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftA2Sym0 #

(SMonad m, SingI d) => SingI (d >>=@#@$$ b :: TyFun (a ~> m b) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d >>=@#@$$ b) #

(SFoldable t, SApplicative f) => SingI (Traverse_Sym0 :: TyFun (a ~> f b) (t a ~> f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

(SFoldable t, SMonad m) => SingI (MapM_Sym0 :: TyFun (a ~> m b) (t a ~> m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MapM_Sym0 #

(SFoldable t, SMonad m) => SingI (FoldrMSym0 :: TyFun (a ~> (b ~> m b)) (b ~> (t a ~> m b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldrMSym0 #

(SFoldable t, SMonad m) => SingI (FoldlMSym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldlMSym0 #

SingI d => SingI (Either_Sym1 d b :: TyFun (b ~> c) (Either a b ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing (Either_Sym1 d b) #

SingI d => SingI (d .@#@$$ a :: TyFun (a ~> b) (a ~> c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (d .@#@$$ a) #

(SFunctor f, SingI d) => SingI (d <&>@#@$$ b :: TyFun (a ~> b) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing (d <&>@#@$$ b) #

SingI (Unzip5Sym0 :: TyFun [(a, b, c, d, e)] ([a], [b], [c], [d], [e]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip5Sym0 #

(SingI d1, SingI d2) => SingI (ListzipWithSym2 d1 d2 :: TyFun [b] [c] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal.Disambiguation

Methods

sing :: Sing (ListzipWithSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (ZipWithSym2 d1 d2 :: TyFun [b] [c] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWithSym2 d1 d2) #

SingI d2 => SingI (ZipWith3Sym1 d2 :: TyFun [a] ([b] ~> ([c] ~> [d1])) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWith3Sym1 d2) #

(SingI d1, SingI d2) => SingI (Zip3Sym2 d1 d2 c :: TyFun [c] [(a, b, c)] -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Zip3Sym2 d1 d2 c) #

(SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumRSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumLSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing (Either_Sym2 d1 d2) #

(SingI d1, SingI d2) => SingI (CurrySym2 d1 d2 :: TyFun b c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing (CurrySym2 d1 d2) #

(STraversable t, SApplicative f, SingI d) => SingI (TraverseSym1 d t :: TyFun (t a) (f (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (TraverseSym1 d t) #

(STraversable t, SMonad m, SingI d) => SingI (MapMSym1 d t :: TyFun (t a) (m (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapMSym1 d t) #

(STraversable t, SingI d) => SingI (MapAccumRSym1 d t :: TyFun a (t b ~> (a, t c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapAccumRSym1 d t) #

(STraversable t, SingI d) => SingI (MapAccumLSym1 d t :: TyFun a (t b ~> (a, t c)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapAccumLSym1 d t) #

(SMonad m, SingI d) => SingI (LiftM2Sym1 d m :: TyFun (m a1) (m a2 ~> m r) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM2Sym1 d m) #

(SApplicative f, SingI d) => SingI (LiftA2Sym1 d f :: TyFun (f a) (f b ~> f c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA2Sym1 d f) #

(SMonad m, SingI d) => SingI (d >>@#@$$ b :: TyFun (m b) (m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d >>@#@$$ b) #

(SApplicative f, SingI d) => SingI (d <*@#@$$ b :: TyFun (f b) (f a) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d <*@#@$$ b) #

(SApplicative f, SingI d) => SingI (d *>@#@$$ b :: TyFun (f b) (f b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (d *>@#@$$ b) #

(SFoldable t, SApplicative f, SingI d) => SingI (Traverse_Sym1 d t :: TyFun (t a) (f ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Traverse_Sym1 d t) #

(SFoldable t, SMonad m, SingI d) => SingI (MapM_Sym1 d t :: TyFun (t a) (m ()) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (MapM_Sym1 d t) #

(SFoldable t, SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 t :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldrSym2 d1 d2 t) #

(SFoldable t, SMonad m, SingI d) => SingI (FoldrMSym1 d t :: TyFun b (t a ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldrMSym1 d t) #

(SFoldable t, SingI d1, SingI d2) => SingI (Foldr'Sym2 d1 d2 t :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldr'Sym2 d1 d2 t) #

(SFoldable t, SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 t :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldlSym2 d1 d2 t) #

(SFoldable t, SMonad m, SingI d) => SingI (FoldlMSym1 d t :: TyFun b (t a ~> m b) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldlMSym1 d t) #

(SFoldable t, SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 t :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (Foldl'Sym2 d1 d2 t) #

(SingI d1, SingI d2) => SingI (FlipSym2 d1 d2 :: TyFun a c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FlipSym2 d1 d2) #

(SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (d1 .@#@$$$ d2) #

SingI (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple5Sym0 #

SingI d2 => SingI (Tuple4Sym1 d2 b c d1 :: TyFun b (c ~> (d1 ~> (a, b, c, d1))) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple4Sym1 d2 b c d1) #

(SingI d1, SingI d2) => SingI (Tuple3Sym2 d1 d2 c :: TyFun c (a, b, c) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple3Sym2 d1 d2 c) #

(STraversable t, SApplicative f, SingI d) => SingI (ForSym1 d f b :: TyFun (a ~> f b) (f (t b)) -> Type) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (ForSym1 d f b) #

(STraversable t, SMonad m, SingI d) => SingI (ForMSym1 d m b ::