Michelson.Typed.Scope

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.

Scopes

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

Alias for constraints which Michelson applies to pushed constants.

type StorageScope t = (Typeable t, SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t)

Alias for constraints which Michelson applies to contract storage.

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

Alias for constraints which Michelson applies to packed values.

type ParameterScope t = (Typeable t, SingI t, HasNoOp t, HasNoNestedBigMaps t)

Alias for constraints which Michelson applies to parameter.

type PrintedValScope t = (SingI t, HasNoOp t)

Alias for constraints which are required for printing.

type UnpackedValScope t = (PackedValScope t, ConstantScope t)

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.

type ProperParameterBetterErrors t = (Typeable t, SingI t, ForbidOp t, ForbidNestedBigMaps t)

type ProperStorageBetterErrors t = (Typeable t, SingI t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)

type ProperConstantBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidContract t)

type ProperPackedValBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t)

type ProperUnpackedValBetterErrors t = (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)

type ProperPrintedValBetterErrors t = (SingI t, ForbidOp t)

properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t

properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t

properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t

properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t

properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t

properPrintedValEvi :: forall t. ProperPrintedValBetterErrors t :- PrintedValScope t

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

Category (:-)

Possible since GHC 7.8, when Category was made polykinded.

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))

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

a => HasDict b (a :- b)

Defined in Data.Constraint

Methods

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

Eq (a :- b)

Assumes IncoherentInstances doesn't exist.

Defined in Data.Constraint

Methods

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

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

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

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.

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)

Defined in Data.Constraint

Methods

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

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

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

a => NFData (a :- b)

Defined in Data.Constraint

Methods

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

data BadTypeForScope

Constructors

BtNotComparable

BtIsOperation

BtHasBigMap

BtHasNestedBigMap

BtHasContract

Instances

Eq BadTypeForScope

Defined in Michelson.Typed.Scope

Methods

(==) :: BadTypeForScope -> BadTypeForScope -> Bool

(/=) :: BadTypeForScope -> BadTypeForScope -> Bool

Show BadTypeForScope

Defined in Michelson.Typed.Scope

Methods

showsPrec :: Int -> BadTypeForScope -> ShowS

show :: BadTypeForScope -> String

showList :: [BadTypeForScope] -> ShowS

Generic BadTypeForScope

Defined in Michelson.Typed.Scope

Associated Types

type Rep BadTypeForScope :: Type -> Type

Methods

from :: BadTypeForScope -> Rep BadTypeForScope x

to :: Rep BadTypeForScope x -> BadTypeForScope

NFData BadTypeForScope

Defined in Michelson.Typed.Scope

Methods

rnf :: BadTypeForScope -> ()

Buildable BadTypeForScope

Defined in Michelson.Typed.Scope

Methods

build :: BadTypeForScope -> Builder

type Rep BadTypeForScope

Defined in Michelson.Typed.Scope

type Rep BadTypeForScope = D1 ('MetaData "BadTypeForScope" "Michelson.Typed.Scope" "morley-1.2.0-GFTR6HhJxtXGRHqcKAr6TU" '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

Should be present for common scopes.

Methods

checkScope :: Either BadTypeForScope (Dict c)

Check that constraint hold for a given type.

Instances

(Typeable t, SingI t) => CheckScope (UnpackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))

(Typeable t, SingI t) => CheckScope (PackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (PackedValScope t))

(Typeable t, SingI t) => CheckScope (ConstantScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ConstantScope t))

(Typeable t, SingI t) => CheckScope (StorageScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (StorageScope t))

(Typeable t, SingI t) => CheckScope (ParameterScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ParameterScope t))

SingI t => CheckScope (HasNoNestedBigMaps t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoNestedBigMaps t))

SingI t => CheckScope (HasNoBigMap t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoBigMap t))

SingI t => CheckScope (HasNoContract t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoContract t))

SingI t => CheckScope (HasNoOp t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoOp t))

(Typeable t, SingI t) => CheckScope (ComparabilityScope t)

Defined in Michelson.Typed.Value

Methods

checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))

SingI t => CheckScope (Comparable t)

Defined in Michelson.Typed.Value

Methods

checkScope :: Either BadTypeForScope (Dict (Comparable t))

Implementation internals

class ContainsBigMap t ~ 'False => HasNoBigMap t

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

Instances

ContainsBigMap t ~ 'False => HasNoBigMap t

Defined in Michelson.Typed.Scope

(Typeable t, SingI t) => CheckScope (UnpackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))

(Typeable t, SingI t) => CheckScope (PackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (PackedValScope t))

(Typeable t, SingI t) => CheckScope (ConstantScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ConstantScope t))

SingI t => CheckScope (HasNoBigMap t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoBigMap t))

class ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t

Constraint which ensures that there are no nested bigmaps.

Instances

ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t

Defined in Michelson.Typed.Scope

(Typeable t, SingI t) => CheckScope (StorageScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (StorageScope t))

(Typeable t, SingI t) => CheckScope (ParameterScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ParameterScope t))

SingI t => CheckScope (HasNoNestedBigMaps t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoNestedBigMaps t))

class ContainsOp t ~ 'False => HasNoOp t

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

ContainsOp t ~ 'False => HasNoOp t

Defined in Michelson.Typed.Scope

(Typeable t, SingI t) => CheckScope (UnpackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))

(Typeable t, SingI t) => CheckScope (PackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (PackedValScope t))

(Typeable t, SingI t) => CheckScope (ConstantScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ConstantScope t))

(Typeable t, SingI t) => CheckScope (StorageScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (StorageScope t))

(Typeable t, SingI t) => CheckScope (ParameterScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ParameterScope t))

SingI t => CheckScope (HasNoOp t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoOp t))

class ContainsContract t ~ 'False => HasNoContract t

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

Instances

ContainsContract t ~ 'False => HasNoContract t

Defined in Michelson.Typed.Scope

(Typeable t, SingI t) => CheckScope (UnpackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))

(Typeable t, SingI t) => CheckScope (ConstantScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ConstantScope t))

(Typeable t, SingI t) => CheckScope (StorageScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (StorageScope t))

SingI t => CheckScope (HasNoContract t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoContract t))

type family ContainsBigMap (t :: T) :: Bool where ...

Whether this type contains TBigMap type.

Equations

ContainsBigMap 'TKey = 'False

ContainsBigMap 'TUnit = 'False

ContainsBigMap 'TSignature = 'False

ContainsBigMap 'TChainId = 'False

ContainsBigMap ('TOption t) = ContainsBigMap t

ContainsBigMap ('TList t) = ContainsBigMap t

ContainsBigMap ('TSet _) = 'False

ContainsBigMap 'TOperation = 'False

ContainsBigMap ('TContract t) = ContainsBigMap t

ContainsBigMap ('TPair a b) = ContainsBigMap a || ContainsBigMap b

ContainsBigMap ('TOr a b) = ContainsBigMap a || ContainsBigMap b

ContainsBigMap ('TLambda _ _) = 'False

ContainsBigMap ('TMap _ v) = ContainsBigMap v

ContainsBigMap ('TBigMap _ _) = 'True

ContainsBigMap _ = 'False

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

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.

Equations

ContainsNestedBigMaps 'TKey = 'False

ContainsNestedBigMaps 'TUnit = 'False

ContainsNestedBigMaps 'TSignature = 'False

ContainsNestedBigMaps 'TChainId = 'False

ContainsNestedBigMaps ('TOption t) = ContainsNestedBigMaps t

ContainsNestedBigMaps ('TList t) = ContainsNestedBigMaps t

ContainsNestedBigMaps ('TSet _) = 'False

ContainsNestedBigMaps 'TOperation = 'False

ContainsNestedBigMaps ('TContract t) = ContainsNestedBigMaps t

ContainsNestedBigMaps ('TPair a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b

ContainsNestedBigMaps ('TOr a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b

ContainsNestedBigMaps ('TLambda _ _) = 'False

ContainsNestedBigMaps ('TMap _ v) = ContainsNestedBigMaps v

ContainsNestedBigMaps ('TBigMap _ v) = ContainsBigMap v

ContainsNestedBigMaps _ = 'False

type ForbidOp t = FailOnOperationFound (ContainsOp t)

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)

type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t)

type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)

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

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 ...

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 ...

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)

Whether the type contains TOperation, with proof.

Constructors

ContainsOp t ~ 'True => OpPresent

ContainsOp t ~ 'False => OpAbsent

data ContractPresence (t :: T)

Constructors

ContainsContract t ~ 'True => ContractPresent

ContainsContract t ~ 'False => ContractAbsent

data BigMapPresence (t :: T)

Constructors

ContainsBigMap t ~ 'True => BigMapPresent

ContainsBigMap t ~ 'False => BigMapAbsent

data NestedBigMapsPresence (t :: T)

Constructors

ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent

ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent

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

Check at runtime whether the given type contains TOperation.

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

Check at runtime whether the given type contains TContract.

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

Check at runtime whether the given type contains TBigMap.

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

Check at runtime whether the given type contains TBigMap.

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

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

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

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

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

Check at runtime that the given type does not containt TBigMap

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

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

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

Reify HasNoOp contraint from ForbidOp.

Left for backward compatibility.

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

Reify HasNoContract contraint from ForbidContract.

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

forbiddenNestedBigMaps :: forall t a. (SingI t, ForbidNestedBigMaps t) => (HasNoNestedBigMaps t => a) -> a

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

SingI 'Z

Defined in Util.Peano

Methods

sing :: Sing 'Z

SingI 'TKey

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TKey

SingI 'TUnit

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TUnit

SingI 'TSignature

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TSignature

SingI 'TChainId

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TChainId

SingI 'TOperation

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TOperation

SingI 'TInt

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TInt

SingI 'TNat

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TNat

SingI 'TString

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TString

SingI 'TBytes

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TBytes

SingI 'TMutez

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TMutez

SingI 'TBool

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TBool

SingI 'TKeyHash

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TKeyHash

SingI 'TTimestamp

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TTimestamp

SingI 'TAddress

Defined in Michelson.Typed.Sing

Methods

sing :: Sing 'TAddress

(SingI n, KnownPeano n) => SingI ('S n :: Nat)

Defined in Util.Peano

Methods

sing :: Sing ('S n)

(SingI a, Typeable a) => SingI ('TOption a :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TOption a)

(SingI a, Typeable a) => SingI ('TList a :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TList a)

(SingI a, Typeable a) => SingI ('TSet a :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TSet a)

(SingI a, Typeable a) => SingI ('TContract a :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TContract a)

(SingI a, Typeable a, Typeable b, SingI b) => SingI ('TPair a b :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TPair a b)

(SingI a, Typeable a, Typeable b, SingI b) => SingI ('TOr a b :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TOr a b)

(SingI a, Typeable a, Typeable b, SingI b) => SingI ('TLambda a b :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TLambda a b)

(SingI a, Typeable a, Typeable b, SingI b) => SingI ('TMap a b :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TMap a b)

(SingI a, Typeable a, Typeable b, SingI b) => SingI ('TBigMap a b :: T)

Defined in Michelson.Typed.Sing

Methods

sing :: Sing ('TBigMap a b)

(Typeable t, SingI t) => CheckScope (UnpackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))

(Typeable t, SingI t) => CheckScope (PackedValScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (PackedValScope t))

(Typeable t, SingI t) => CheckScope (ConstantScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ConstantScope t))

(Typeable t, SingI t) => CheckScope (StorageScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (StorageScope t))

(Typeable t, SingI t) => CheckScope (ParameterScope t)

Defined in Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ParameterScope t))

(Typeable t, SingI t) => CheckScope (ComparabilityScope t)

Defined in Michelson.Typed.Value

Methods

checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))

SingI NotSym0

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing NotSym0

SingI (||@#@$)

Defined in Data.Singletons.Prelude.Bool

Methods

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

SingI (&&@#@$)

Defined in Data.Singletons.Prelude.Bool

Methods

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

SingI Log2Sym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing Log2Sym0

SingI (<=?@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

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

SingI ModSym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing ModSym0

SingI DivSym0

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing DivSym0

SingI (^@#@$)

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing (^@#@$)

SingI AllSym0

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing AllSym0

SingI AnySym0

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing AnySym0

SingI ShowParenSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowParenSym0

SingI OrSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing OrSym0

SingI AndSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AndSym0

SingI UnwordsSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnwordsSym0

SingI UnlinesSym0

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnlinesSym0

SingI Show_tupleSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_tupleSym0

SingI ThenCmpSym0

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ThenCmpSym0

SingI EftNatSym0

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EftNatSym0

SingI EfdtNatSym0

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatSym0

SingI EfdtNatDnSym0

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatDnSym0

SingI EfdtNatUpSym0

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EfdtNatUpSym0

SingI ShowCommaSpaceSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCommaSpaceSym0

SingI ShowSpaceSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowSpaceSym0

SingI ShowStringSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowStringSym0

SingI ShowCharSym0

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowCharSym0

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

Defined in Data.Singletons.Prelude.Bool

Methods

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

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

Defined in Data.Singletons.Prelude.Bool

Methods

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

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (ModSym1 x)

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

Defined in Data.Singletons.TypeLits

Methods

sing :: Sing (DivSym1 x)

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

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing GuardSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing WhenSym0

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

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

Methods

sing :: Sing ListtransposeSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TransposeSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ConcatSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing CatMaybesSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowListSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing ListToMaybeSym0

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

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

Methods

sing :: Sing ListtailsSym0

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

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

Methods

sing :: Sing ListsumSym0

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

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

Methods

sing :: Sing ListsortSym0

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

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

Methods

sing :: Sing ListreverseSym0

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

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

Methods

sing :: Sing ListproductSym0

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

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

Methods

sing :: Sing ListnullSym0

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

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

Methods

sing :: Sing ListminimumSym0

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

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

Methods

sing :: Sing ListmaximumSym0

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

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

Methods

sing :: Sing ListlengthSym0

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

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

Methods

sing :: Sing ListlastSym0

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

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

Methods

sing :: Sing ListisPrefixOfSym0

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

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

Methods

sing :: Sing ListinitsSym0

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

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

Methods

sing :: Sing ListinitSym0

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

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

Methods

sing :: Sing ListindexSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnionSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TailsSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TailSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SumSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SubsequencesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SortSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ReverseSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ProductSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PermutationsSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NullSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NubSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NonEmptySubsequencesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MinimumSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MaximumSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LengthSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LastSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsSuffixOfSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsPrefixOfSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IsInfixOfSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersectSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntercalateSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InitsSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InitSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing HeadSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GroupSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing MconcatSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing MaybeToListSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing IsNothingSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing IsJustSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing FromJustSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing OptionSym0

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing LastSym0

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing FirstSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ThenCmpSym1 d)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EftNatSym1 d)

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing FromIntegerSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing ToEnumSym0

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

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

Methods

sing :: Sing ListtakeSym0

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

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

Methods

sing :: Sing ListsplitAtSym0

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

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

Methods

sing :: Sing ListdropSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SplitAtSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatSym1 d)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatDnSym1 d)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatUpSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsPrecSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ReplicateSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowStringSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowCharSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (Show_tupleSym1 d)

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

Defined in Data.Singletons.Prelude.IsString

Methods

sing :: Sing FromStringSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowsSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing Show_Sym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SubtractSym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing SignumSym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing NegateSym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing AbsSym0

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (-@#@$)

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (+@#@$)

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (*@#@$)

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing FromMaybeSym0

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

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

Methods

sing :: Sing ListintersperseSym0

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

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

Methods

sing :: Sing ListinsertSym0

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

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

Methods

sing :: Sing ListelemSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PrependToAllSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NotElemSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersperseSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InsertSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndicesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ElemIndexSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing OrSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AndSym0

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

Defined in Data.Singletons.Prelude.Eq

Methods

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

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

Defined in Data.Singletons.Prelude.Eq

Methods

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

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing SuccSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing PredSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing FromEnumSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EnumFromToSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing EnumFromThenToSym0

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

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing Bool_Sym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing IdSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing AsTypeOfSym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing JustSym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing IdentitySym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (:@#@$)

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MinSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MaxSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing DownSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing CompareSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>@#@$)

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<@#@$)

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing WrapMonoidSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing SumSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing ProductSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing MinSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing MaxSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing LastSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing FirstSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing DualSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing MappendSym0

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sing :: Sing SconcatSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing ShowListWithSym0

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

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

Methods

sing :: Sing ListtakeWhileSym0

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

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

Methods

sing :: Sing ListspanSym0

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

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

Methods

sing :: Sing ListsortBySym0

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

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

Methods

sing :: Sing Listscanr1Sym0

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

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

Methods

sing :: Sing ListpartitionSym0

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

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

Methods

sing :: Sing ListnubBySym0

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

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

Methods

sing :: Sing Listfoldr1Sym0

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

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

Methods

sing :: Sing Listfoldl1Sym0

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

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

Methods

sing :: Sing ListfilterSym0

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

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

Methods

sing :: Sing ListdropWhileSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnionBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing TakeWhileSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SpanSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SortBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing SelectSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Scanr1Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Scanl1Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing PartitionSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing NubBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MinimumBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MaximumBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing IntersectBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing InsertBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GroupBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldr1Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl1Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl1'Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndicesSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FindIndexSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing FilterSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Elem_bySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropWhileSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DropWhileEndSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteFirstsBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing DeleteBySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing BreakSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AnySym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing AllSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing UntilSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntercalateSym1 d)

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing RightsSym0

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing PartitionEithersSym0

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing LeftsSym0

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

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

Methods

sing :: Sing ListunzipSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnzipSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListWithSym1 d)

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

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

Methods

sing :: Sing ListzipSym0

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

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

Methods

sing :: Sing (ListtakeWhileSym1 d)

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

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)

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

Methods

sing :: Sing (ListsplitAtSym1 d a)

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

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

Methods

sing :: Sing (ListspanSym1 d)

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

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

Methods

sing :: Sing (ListsortBySym1 d)

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

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

Methods

sing :: Sing (Listscanr1Sym1 d)

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

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

Methods

sing :: Sing (ListpartitionSym1 d)

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

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

Methods

sing :: Sing (ListnubBySym1 d)

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

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

Methods

sing :: Sing (ListisPrefixOfSym1 d)

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

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

Methods

sing :: Sing (ListintersperseSym1 d)

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

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

Methods

sing :: Sing (ListinsertSym1 d)

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

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

Methods

sing :: Sing (Listfoldr1Sym1 d)

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

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

Methods

sing :: Sing (Listfoldl1Sym1 d)

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

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

Methods

sing :: Sing (ListfilterSym1 d)

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

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

Methods

sing :: Sing (ListelemSym1 d)

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

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

Methods

sing :: Sing (ListdropWhileSym1 d)

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

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

Methods

sing :: Sing (ListdropSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnionBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (TakeWhileSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (TakeSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SplitAtSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SpanSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SortBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Scanr1Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Scanl1Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (PrependToAllSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (PartitionSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (NubBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (NotElemSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MinimumBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MaximumBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsSuffixOfSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsPrefixOfSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IsInfixOfSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersperseSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (IntersectBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (GroupBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing GenericLengthSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldr1Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl1Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Foldl1'Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndicesSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FindIndexSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (FilterSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndicesSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ElemIndexSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropWhileSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropWhileEndSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DropSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteFirstsBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (BreakSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (AnySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (AllSym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

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

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (FromMaybeSym1 d)

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing IsRightSym0

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing IsLeftSym0

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatDnSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EfdtNatUpSym2 d1 d2)

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

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

Methods

sing :: Sing (ListindexSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowParenSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsSym1 d)

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowListSym1 d)

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

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorWithoutStackTraceSym0

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

Defined in Data.Singletons.TypeLits.Internal

Methods

sing :: Sing ErrorSym0

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing SwapSym0

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing SndSym0

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing FstSym0

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

Defined in Data.Singletons.Prelude.Show

Methods

sing :: Sing (ShowsPrecSym1 d a)

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

Defined in Data.Singletons.Prelude.Num

Methods

sing :: Sing (SubtractSym1 d)

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

Defined in Data.Singletons.Prelude.Num

Methods

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

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

Defined in Data.Singletons.Prelude.Num

Methods

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

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

Defined in Data.Singletons.Prelude.Num

Methods

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

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing Maybe_Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (SelectSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ReplicateSym1 d a)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing LookupSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (InsertBySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (Elem_bySym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteBySym1 d)

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (WhenSym1 d f)

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ReturnSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing PureSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing JoinSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ToListSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing SumSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ProductSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing NotElemSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MinimumSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MaximumSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ElemSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ConcatSym0

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

Defined in Data.Singletons.Prelude.Eq

Methods

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

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

Defined in Data.Singletons.Prelude.Eq

Methods

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

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromToSym1 d)

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

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromThenToSym1 d)

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

Defined in Data.Singletons.Prelude.Bool

Methods

sing :: Sing (Bool_Sym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing SeqSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ConstSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (AsTypeOfSym1 d)

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple2Sym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing RightSym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing LeftSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MinSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MaxSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (CompareSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monoid

Methods

sing :: Sing (MappendSym1 d)

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

Defined in Data.Singletons.Prelude.Functor

Methods

sing :: Sing VoidSym0

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

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing Option_Sym0

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

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing ArgSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing MapMaybeSym0

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

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

Methods

sing :: Sing ListscanrSym0

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

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

Methods

sing :: Sing ListscanlSym0

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

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

Methods

sing :: Sing ListmapSym0

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

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

Methods

sing :: Sing ListfoldrSym0

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

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

Methods

sing :: Sing ListfoldlSym0

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

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

Methods

sing :: Sing Listfoldl'Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing UnfoldrSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ScanrSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ScanlSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Foldl'Sym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ConcatMapSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MinimumBySym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing MaximumBySym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldr1Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldl1Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FindSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AnySym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AllSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (UntilSym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing MapSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing FoldrSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing ($@#@$)

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing FoldlSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ComparingSym0

SingI (ConstSym0 :: TyFun a6989586621679095645 (Const a6989586621679095645 b6989586621679095646) -> Type)

Defined in Data.Singletons.Prelude.Const

Methods

sing :: Sing ConstSym0

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

Defined in Data.Singletons.Internal

Methods

sing :: Sing ('WrapSing s)

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

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (LookupSym1 d b)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip3Sym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (MapMaybeSym1 d)

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

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

Methods

sing :: Sing (ListzipSym1 d b)

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

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

Methods

sing :: Sing (ListmapSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipSym1 d b)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Zip3Sym0

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

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (DeleteBySym2 d1 d2)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ConcatMapSym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (MapSym1 d)

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

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)

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)

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)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing SequenceSym0

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

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing SequenceASym0

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

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

Methods

sing :: Sing (ListscanrSym1 d)

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

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

Methods

sing :: Sing (ListscanlSym1 d)

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

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

Methods

sing :: Sing (ListfoldrSym1 d)

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

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

Methods

sing :: Sing (ListfoldlSym1 d)

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

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

Methods

sing :: Sing (Listfoldl'Sym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (UnfoldrSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanrSym1 d)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ScanlSym1 d)

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

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)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing MplusSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing ApSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Sequence_Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing SequenceA_Sym0

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

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)

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)

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)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (MaximumBySym1 d t)

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing LengthSym0

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

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Enum

Methods

sing :: Sing (EnumFromThenToSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (UntilSym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (SeqSym1 d b)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FoldrSym1 d)

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (ConstSym1 d b)

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple3Sym0

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple2Sym1 d b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (FoldlSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ComparingSym1 d)

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

Defined in Data.Singletons.Prelude.Functor

Methods

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

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

Defined in Data.Singletons.Prelude.Functor

Methods

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

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

Defined in Data.Singletons.Prelude.Semigroup

Methods

sing :: Sing (ArgSym1 d b)

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing CurrySym0

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing UncurrySym0

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

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing FoldMapDefaultSym0

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

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing FmapDefaultSym0

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

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (Maybe_Sym1 d a)

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

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

Methods

sing :: Sing ListzipWithSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipWithSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MapAccumRSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing MapAccumLSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftMSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftASym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing FmapSym0

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldrSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldr'Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldlSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Foldl'Sym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing FoldMapSym0

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

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing ConcatMapSym0

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

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing Either_Sym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing FlipSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (.@#@$)

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

Defined in Data.Singletons.Prelude.Functor

Methods

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

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

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip4Sym0

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FoldrSym2 d1 d2)

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

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)

Defined in Data.Singletons.Prelude.Maybe

Methods

sing :: Sing (Maybe_Sym2 d1 d2)

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

Defined in Data.Singletons.Prelude.Tuple

Methods

sing :: Sing (UncurrySym1 d)

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

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (FmapDefaultSym1 d t)

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (MapAccumRSym1 d)

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

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (ApSym1 d)

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

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)

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)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

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

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing AsumSym0

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

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FlipSym1 d)

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

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple4Sym0

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

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)

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)

Defined in Data.Singletons.Prelude.Functor

Methods

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

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

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)

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)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing TraverseSym0

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

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)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing MapAccumRSym0

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

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing MapAccumLSym0

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

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing ZipWith3Sym0

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

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)

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)

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)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing Traverse_Sym0

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

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)

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)

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)

Defined in Data.Singletons.Prelude.Either

Methods

sing :: Sing (Either_Sym1 d b)

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

Defined in Data.Singletons.Prelude.Base

Methods

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

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

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip5Sym0

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

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)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWithSym2 d1 d2)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Base

Methods

sing :: Sing (FlipSym2 d1 d2)

(SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type)

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)

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)

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)

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)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (ForSym1 d f b)

(STraversable t, SMonad m, SingI d) => SingI (ForMSym1 d m b :: TyFun (a ~> m b) (m (t b)) -> Type)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (ForMSym1 d m b)

SMonad m => SingI (LiftM3Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> r))) (m a1 ~> (m a2 ~> (m a3 ~> m r))) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftM3Sym0

SApplicative f => SingI (LiftA3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) (f a ~> (f b ~> (f c ~> f d))) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftA3Sym0

(SFoldable t, SApplicative f, SingI d) => SingI (For_Sym1 d f b :: TyFun (a ~> f b) (f ()) -> Type)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (For_Sym1 d f b)

(SFoldable t, SMonad m, SingI d) => SingI (ForM_Sym1 d m b :: TyFun (a ~> m b) (m ()) -> Type)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (ForM_Sym1 d m b)

SingI (Unzip6Sym0 :: TyFun [(a, b, c, d, e, f)] ([a], [b], [c], [d], [e], [f]) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip6Sym0

(SingI d2, SingI d3) => SingI (ZipWith3Sym2 d2 d3 :: TyFun [b] ([c] ~> [d1]) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWith3Sym2 d2 d3)

(STraversable t, SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 t :: TyFun (t b) (a, t c) -> Type)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapAccumRSym2 d1 d2 t)

(STraversable t, SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 t :: TyFun (t b) (a, t c) -> Type)

Defined in Data.Singletons.Prelude.Traversable

Methods

sing :: Sing (MapAccumLSym2 d1 d2 t)

(SMonad m, SingI d) => SingI (LiftM3Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> m r)) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM3Sym1 d m)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM2Sym2 d1 d2 :: TyFun (m a2) (m r) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM2Sym2 d1 d2)

(SApplicative f, SingI d2) => SingI (LiftA3Sym1 d2 f :: TyFun (f a) (f b ~> (f c ~> f d1)) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA3Sym1 d2 f)

(SApplicative f, SingI d1, SingI d2) => SingI (LiftA2Sym2 d1 d2 :: TyFun (f b) (f c) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA2Sym2 d1 d2)

(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldrMSym2 d1 d2 t :: TyFun (t a) (m b) -> Type)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldrMSym2 d1 d2 t)

(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldlMSym2 d1 d2 t :: TyFun (t a) (m b) -> Type)

Defined in Data.Singletons.Prelude.Foldable

Methods

sing :: Sing (FoldlMSym2 d1 d2 t)

SingI (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple6Sym0

SingI d2 => SingI (Tuple5Sym1 d2 b c d1 e :: TyFun b (c ~> (d1 ~> (e ~> (a, b, c, d1, e)))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple5Sym1 d2 b c d1 e)

(SingI d2, SingI d3) => SingI (Tuple4Sym2 d2 d3 c d1 :: TyFun c (d1 ~> (a, b, c, d1)) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple4Sym2 d2 d3 c d1)

SMonad m => SingI (LiftM4Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> r)))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> m r)))) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftM4Sym0

SingI (Unzip7Sym0 :: TyFun [(a, b, c, d, e, f, g)] ([a], [b], [c], [d], [e], [f], [g]) -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing Unzip7Sym0

(SingI d2, SingI d3, SingI d4) => SingI (ZipWith3Sym3 d2 d3 d4 :: TyFun [c] [d1] -> Type)

Defined in Data.Singletons.Prelude.List.Internal

Methods

sing :: Sing (ZipWith3Sym3 d2 d3 d4)

(SMonad m, SingI d) => SingI (LiftM4Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> m r))) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM4Sym1 d m)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM3Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> m r) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM3Sym2 d1 d2)

(SApplicative f, SingI d2, SingI d3) => SingI (LiftA3Sym2 d2 d3 :: TyFun (f b) (f c ~> f d1) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA3Sym2 d2 d3)

SingI (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing Tuple7Sym0

SingI d2 => SingI (Tuple6Sym1 d2 b c d1 e f :: TyFun b (c ~> (d1 ~> (e ~> (f ~> (a, b, c, d1, e, f))))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym1 d2 b c d1 e f)

(SingI d2, SingI d3) => SingI (Tuple5Sym2 d2 d3 c d1 e :: TyFun c (d1 ~> (e ~> (a, b, c, d1, e))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple5Sym2 d2 d3 c d1 e)

(SingI d2, SingI d3, SingI d4) => SingI (Tuple4Sym3 d2 d3 d4 d1 :: TyFun d1 (a, b, c, d1) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple4Sym3 d2 d3 d4 d1)

SMonad m => SingI (LiftM5Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> r))))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r))))) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing LiftM5Sym0

(SMonad m, SingI d) => SingI (LiftM5Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r)))) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym1 d m)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM4Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> m r)) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM4Sym2 d1 d2)

(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM3Sym3 d1 d2 d3 :: TyFun (m a3) (m r) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM3Sym3 d1 d2 d3)

(SApplicative f, SingI d2, SingI d3, SingI d4) => SingI (LiftA3Sym3 d2 d3 d4 :: TyFun (f c) (f d1) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftA3Sym3 d2 d3 d4)

SingI d2 => SingI (Tuple7Sym1 d2 b c d1 e f g :: TyFun b (c ~> (d1 ~> (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g)))))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym1 d2 b c d1 e f g)

(SingI d2, SingI d3) => SingI (Tuple6Sym2 d2 d3 c d1 e f :: TyFun c (d1 ~> (e ~> (f ~> (a, b, c, d1, e, f)))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym2 d2 d3 c d1 e f)

(SingI d2, SingI d3, SingI d4) => SingI (Tuple5Sym3 d2 d3 d4 d1 e :: TyFun d1 (e ~> (a, b, c, d1, e)) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple5Sym3 d2 d3 d4 d1 e)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM5Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> (m a5 ~> m r))) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym2 d1 d2)

(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM4Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> m r) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM4Sym3 d1 d2 d3)

(SingI d2, SingI d3) => SingI (Tuple7Sym2 d2 d3 c d1 e f g :: TyFun c (d1 ~> (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g))))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym2 d2 d3 c d1 e f g)

(SingI d2, SingI d3, SingI d4) => SingI (Tuple6Sym3 d2 d3 d4 d1 e f :: TyFun d1 (e ~> (f ~> (a, b, c, d1, e, f))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym3 d2 d3 d4 d1 e f)

(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple5Sym4 d2 d3 d4 d5 e :: TyFun e (a, b, c, d1, e) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple5Sym4 d2 d3 d4 d5 e)

(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM5Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> (m a5 ~> m r)) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym3 d1 d2 d3)

(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM4Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m r) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM4Sym4 d1 d2 d3 d4)

(SingI d2, SingI d3, SingI d4) => SingI (Tuple7Sym3 d2 d3 d4 d1 e f g :: TyFun d1 (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g)))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym3 d2 d3 d4 d1 e f g)

(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple6Sym4 d2 d3 d4 d5 e f :: TyFun e (f ~> (a, b, c, d1, e, f)) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym4 d2 d3 d4 d5 e f)

(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM5Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m a5 ~> m r) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym4 d1 d2 d3 d4)

(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple7Sym4 d2 d3 d4 d5 e f g :: TyFun e (f ~> (g ~> (a, b, c, d1, e, f, g))) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym4 d2 d3 d4 d5 e f g)

(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6) => SingI (Tuple6Sym5 d2 d3 d4 d5 d6 f :: TyFun f (a, b, c, d1, e, f) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple6Sym5 d2 d3 d4 d5 d6 f)

(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4, SingI d5) => SingI (LiftM5Sym5 d1 d2 d3 d4 d5 :: TyFun (m a5) (m r) -> Type)

Defined in Data.Singletons.Prelude.Monad.Internal

Methods

sing :: Sing (LiftM5Sym5 d1 d2 d3 d4 d5)

(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6) => SingI (Tuple7Sym5 d2 d3 d4 d5 d6 f g :: TyFun f (g ~> (a, b, c, d1, e, f, g)) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym5 d2 d3 d4 d5 d6 f g)

(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6, SingI d7) => SingI (Tuple7Sym6 d2 d3 d4 d5 d6 d7 g :: TyFun g (a, b, c, d1, e, f, g) -> Type)

Defined in Data.Singletons.Prelude.Instances

Methods

sing :: Sing (Tuple7Sym6 d2 d3 d4 d5 d6 d7 g)