Safe Haskell	None
Language	Haskell2010

Lorentz.Contracts.Upgradeable.Common.Base

Contents

Re-exports

Synopsis

newtype Version = Version {
- unVersion :: Natural
}
type VersionKind = ContractVersionTag -> Type
class KnownContractVersion (v :: VersionKind) where
- type VerInterface v :: [EntrypointKind]
- type VerUStoreTemplate v :: Type
- type VerPermanent v :: Type
- contractVersion :: Proxy v -> Version
type VerParam v = UParam (VerInterface v)
type VerUStore v = UStore (VerUStoreTemplate v)
data EmptyContractVersion (perm :: Type) :: VersionKind
data SomeContractVersion (perm :: Type) :: VersionKind
type UStore_ = UStore SomeUTemplate
newtype MigrationScript (oldStore :: Type) (newStore :: Type) = MigrationScript {
- unMigrationScript :: Lambda UStore_ UStore_
}
type MigrationScriptFrom oldStore = MigrationScript oldStore SomeUTemplate
type MigrationScriptTo newStore = MigrationScript SomeUTemplate newStore
newtype UContractRouter (ver :: VersionKind) = UContractRouter {
- unUContractRouter :: Lambda (VerParam ver, VerUStore ver) ([Operation], VerUStore ver)
}
type SomeUContractRouter = UContractRouter (SomeContractVersion ())
data UpgradeableEntrypointsKind
newtype PermanentImpl ver = PermanentImpl {
- unPermanentImpl :: Entrypoint (VerPermanent ver) (VerUStore ver)
}
type SomePermanentImpl perm = PermanentImpl (SomeContractVersion perm)
data PermanentEntrypointsKind
mkUContractRouter :: ([VerParam ver, VerUStore ver] :-> '[([Operation], VerUStore ver)]) -> UContractRouter ver
coerceUContractRouter :: (Coercible_ (VerParam s1) (VerParam s2), Coercible_ (VerUStore s1) (VerUStore s2)) => UContractRouter s1 -> UContractRouter s2
emptyPermanentImpl :: VerPermanent ver ~ Empty => PermanentImpl ver
mkSmallPermanentImpl :: forall ver dt out inp clauses. (CaseTC dt out inp clauses, DocumentEntrypoints PermanentEntrypointsKind dt, dt ~ VerPermanent ver, inp ~ '[VerUStore ver], out ~ ContractOut (VerUStore ver)) => IsoRecTuple clauses -> PermanentImpl ver
data Nat
data Empty
absurd_ :: forall (s :: [Type]) (s' :: [Type]). (Empty ': s) :-> s'

Documentation

newtype Version Source #

Version of a contract.

Our current versioning suggests that this type is a term-level reflection of types which have KnownContractVersion instance, so this version item should uniquely identify storage structure and entrypoints set for a given contract for all of its instances.

The old semantics of this type was that it counts number of given contract instance upgrades, so different contract instances, being upgraded to the recent version, could have different Versions. For old contracts we have to follow this behaviour.

Constructors

Version
Fields unVersion :: Natural

Instances

Instances details

Eq Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods (==) :: Version -> Version -> Bool # (/=) :: Version -> Version -> Bool #
Num Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods (+) :: Version -> Version -> Version # (-) :: Version -> Version -> Version # (*) :: Version -> Version -> Version # negate :: Version -> Version # abs :: Version -> Version # signum :: Version -> Version # fromInteger :: Integer -> Version #
Ord Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods compare :: Version -> Version -> Ordering # (<) :: Version -> Version -> Bool # (<=) :: Version -> Version -> Bool # (>) :: Version -> Version -> Bool # (>=) :: Version -> Version -> Bool # max :: Version -> Version -> Version # min :: Version -> Version -> Version #
Show Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods showsPrec :: Int -> Version -> ShowS # show :: Version -> String # showList :: [Version] -> ShowS #
Generic Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type Rep Version :: Type -> Type # Methods from :: Version -> Rep Version x # to :: Rep Version x -> Version #
Buildable Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods build :: Version -> Builder #
ParameterHasEntrypoints Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type ParameterEntrypointsDerivation Version #
HasAnnotation Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods getAnnotation :: FollowEntrypointFlag -> Notes (ToT Version) # annOptions :: AnnOptions #
IsoValue Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type ToT Version :: T # Methods toVal :: Version -> Value (ToT Version) # fromVal :: Value (ToT Version) -> Version #
TypeHasDoc Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type TypeDocFieldDescriptions Version :: FieldDescriptions # Methods typeDocName :: Proxy Version -> Text # typeDocMdDescription :: Markdown # typeDocMdReference :: Proxy Version -> WithinParens -> Markdown # typeDocDependencies :: Proxy Version -> [SomeDocDefinitionItem] # typeDocHaskellRep :: TypeDocHaskellRep Version # typeDocMichelsonRep :: TypeDocMichelsonRep Version #
ArithOpHs Add Natural Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type ArithResHs Add Natural Version #
type Rep Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type Rep Version = D1 ('MetaData "Version" "Lorentz.Contracts.Upgradeable.Common.Base" "morley-upgradeable-0.3-inplace" 'True) (C1 ('MetaCons "Version" 'PrefixI 'True) (S1 ('MetaSel ('Just "unVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Natural)))
type ParameterEntrypointsDerivation Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type ParameterEntrypointsDerivation Version = EpdNone
type ToT Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type ToT Version = ToT Natural
type TypeDocFieldDescriptions Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type TypeDocFieldDescriptions Version = '[] :: [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]
type ArithResHs Add Natural Version Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type ArithResHs Add Natural Version = Version

type VersionKind = ContractVersionTag -> Type Source #

Kind of type-level contract version.

class KnownContractVersion (v :: VersionKind) where Source #

Declare given type as contract version identifier.

Instances of this typeclass (versions) uniquely identify contract storage scheme and code. Normally the opposite should also hold, i.e. contract version - (contract storage scheme, code) relation is a bijection.

If as part of migration you need to update contract storage without modifying its structure, then contract version should not change, and you should perform an upgrade to the same version as the current one.

We allow upgrades between arbitrary two versions, so one can not only upgrade to the next adjacent version, but also upgrade a new contract from V0 to the recent version immediately, or leave version the same (as a versatile way to change storage).

Minimal complete definition

Nothing

Associated Types

type VerInterface v :: [EntrypointKind] Source #

List of entrypoints of given contract version.

type VerUStoreTemplate v :: Type Source #

Storage template of given contract version.

type VerPermanent v :: Type Source #

Set of permanent entrypoints (as a sum type).

We tie this type to contract version for convenience, in order not to carry one more type argument everywhere. We do not ensure right here that all versions of a contract have the same permanent entrypoints, but if this does not hold, then (ideally) it will not be possible to construct migration between such contract versions.

type VerPermanent _ = Empty

Methods

contractVersion :: Proxy v -> Version Source #

Get term-level contract version. Returned value will be stored within the contract designating the current contract version.

default contractVersion :: (v ~ cid ver, KnownNat ver) => Proxy v -> Version Source #

Instances

Instances details

KnownContractVersion UnsafeLedgerV1 Source #
Instance details Defined in Lorentz.Contracts.UpgradeableUnsafeLedger.V1 Associated Types type VerInterface UnsafeLedgerV1 :: [EntrypointKind] Source # type VerUStoreTemplate UnsafeLedgerV1 Source # type VerPermanent UnsafeLedgerV1 Source # Methods contractVersion :: Proxy UnsafeLedgerV1 -> Version Source #
KnownContractVersion UnsafeLedgerV2 Source #
Instance details Defined in Lorentz.Contracts.UpgradeableUnsafeLedger.V2 Associated Types type VerInterface UnsafeLedgerV2 :: [EntrypointKind] Source # type VerUStoreTemplate UnsafeLedgerV2 Source # type VerPermanent UnsafeLedgerV2 Source # Methods contractVersion :: Proxy UnsafeLedgerV2 -> Version Source #
KnownContractVersion CounterV1 Source #
Instance details Defined in Lorentz.Contracts.UpgradeableCounter.V1 Associated Types type VerInterface CounterV1 :: [EntrypointKind] Source # type VerUStoreTemplate CounterV1 Source # type VerPermanent CounterV1 Source # Methods contractVersion :: Proxy CounterV1 -> Version Source #
KnownContractVersion CounterV2 Source #
Instance details Defined in Lorentz.Contracts.UpgradeableCounter.V2 Associated Types type VerInterface CounterV2 :: [EntrypointKind] Source # type VerUStoreTemplate CounterV2 Source # type VerPermanent CounterV2 Source # Methods contractVersion :: Proxy CounterV2 -> Version Source #
KnownContractVersion (SomeContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type VerInterface (SomeContractVersion perm) :: [EntrypointKind] Source # type VerUStoreTemplate (SomeContractVersion perm) Source # type VerPermanent (SomeContractVersion perm) Source # Methods contractVersion :: Proxy (SomeContractVersion perm) -> Version Source #
KnownContractVersion (EmptyContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type VerInterface (EmptyContractVersion perm) :: [EntrypointKind] Source # type VerUStoreTemplate (EmptyContractVersion perm) Source # type VerPermanent (EmptyContractVersion perm) Source # Methods contractVersion :: Proxy (EmptyContractVersion perm) -> Version Source #
KnownContractVersion (CounterSduV 0) Source #
Instance details Defined in Lorentz.Contracts.UpgradeableCounterSdu Associated Types type VerInterface (CounterSduV 0) :: [EntrypointKind] Source # type VerUStoreTemplate (CounterSduV 0) Source # type VerPermanent (CounterSduV 0) Source # Methods contractVersion :: Proxy (CounterSduV 0) -> Version Source #
KnownContractVersion (CounterSduV 1) Source #
Instance details Defined in Lorentz.Contracts.UpgradeableCounterSdu.V1 Associated Types type VerInterface (CounterSduV 1) :: [EntrypointKind] Source # type VerUStoreTemplate (CounterSduV 1) Source # type VerPermanent (CounterSduV 1) Source # Methods contractVersion :: Proxy (CounterSduV 1) -> Version Source #
KnownContractVersion (CounterSduV 2) Source #
Instance details Defined in Lorentz.Contracts.UpgradeableCounterSdu.V2 Associated Types type VerInterface (CounterSduV 2) :: [EntrypointKind] Source # type VerUStoreTemplate (CounterSduV 2) Source # type VerPermanent (CounterSduV 2) Source # Methods contractVersion :: Proxy (CounterSduV 2) -> Version Source #

type VerParam v = UParam (VerInterface v) Source #

type VerUStore v = UStore (VerUStoreTemplate v) Source #

data EmptyContractVersion (perm :: Type) :: VersionKind Source #

Contract with empty interface and storage.

Instances

Instances details

KnownContractVersion (EmptyContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type VerInterface (EmptyContractVersion perm) :: [EntrypointKind] Source # type VerUStoreTemplate (EmptyContractVersion perm) Source # type VerPermanent (EmptyContractVersion perm) Source # Methods contractVersion :: Proxy (EmptyContractVersion perm) -> Version Source #
type VerInterface (EmptyContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type VerInterface (EmptyContractVersion perm) = '[] :: [EntrypointKind]
type VerUStoreTemplate (EmptyContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type VerUStoreTemplate (EmptyContractVersion perm) = ()
type VerPermanent (EmptyContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type VerPermanent (EmptyContractVersion perm) = perm

data SomeContractVersion (perm :: Type) :: VersionKind Source #

Version which forgets about particular interface/storage.

Instances

Instances details

KnownContractVersion (SomeContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type VerInterface (SomeContractVersion perm) :: [EntrypointKind] Source # type VerUStoreTemplate (SomeContractVersion perm) Source # type VerPermanent (SomeContractVersion perm) Source # Methods contractVersion :: Proxy (SomeContractVersion perm) -> Version Source #
type VerInterface (SomeContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type VerInterface (SomeContractVersion perm) = SomeInterface
type VerUStoreTemplate (SomeContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type VerUStoreTemplate (SomeContractVersion perm) = SomeUTemplate
type VerPermanent (SomeContractVersion perm) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type VerPermanent (SomeContractVersion perm) = perm

type UStore_ = UStore SomeUTemplate Source #

UStore with hidden template.

newtype MigrationScript (oldStore :: Type) (newStore :: Type) Source #

Code of migration for UStore.

Invariant: preferably should fit into op size / gas limits (quite obvious). Often this stands for exactly one stage of migration (one Tezos transaction).

Constructors

MigrationScript
Fields unMigrationScript :: Lambda UStore_ UStore_

Instances

Instances details

CanCastTo (Lambda (UStore ot1) (UStore nt1)) (Lambda (UStore ot2) (UStore nt2)) => CanCastTo (MigrationScript ot1 nt1 :: Type) (MigrationScript ot2 nt2 :: Type) Source #
Instance details Defined in Lorentz.UStore.Migration.Base Methods castDummy :: Proxy (MigrationScript ot1 nt1) -> Proxy (MigrationScript ot2 nt2) -> () #
Show (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base Methods showsPrec :: Int -> MigrationScript oldStore newStore -> ShowS # show :: MigrationScript oldStore newStore -> String # showList :: [MigrationScript oldStore newStore] -> ShowS #
Generic (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base Associated Types type Rep (MigrationScript oldStore newStore) :: Type -> Type # Methods from :: MigrationScript oldStore newStore -> Rep (MigrationScript oldStore newStore) x # to :: Rep (MigrationScript oldStore newStore) x -> MigrationScript oldStore newStore #
Wrappable (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base Associated Types type Unwrappable (MigrationScript oldStore newStore) #
HasAnnotation (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base Methods getAnnotation :: FollowEntrypointFlag -> Notes (ToT (MigrationScript oldStore newStore)) # annOptions :: AnnOptions #
IsoValue (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base Associated Types type ToT (MigrationScript oldStore newStore) :: T # Methods toVal :: MigrationScript oldStore newStore -> Value (ToT (MigrationScript oldStore newStore)) # fromVal :: Value (ToT (MigrationScript oldStore newStore)) -> MigrationScript oldStore newStore #
Each '[Typeable :: Type -> Constraint, UStoreTemplateHasDoc] '[oldStore, newStore] => TypeHasDoc (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base Associated Types type TypeDocFieldDescriptions (MigrationScript oldStore newStore) :: FieldDescriptions # Methods typeDocName :: Proxy (MigrationScript oldStore newStore) -> Text # typeDocMdDescription :: Markdown # typeDocMdReference :: Proxy (MigrationScript oldStore newStore) -> WithinParens -> Markdown # typeDocDependencies :: Proxy (MigrationScript oldStore newStore) -> [SomeDocDefinitionItem] # typeDocHaskellRep :: TypeDocHaskellRep (MigrationScript oldStore newStore) # typeDocMichelsonRep :: TypeDocMichelsonRep (MigrationScript oldStore newStore) #
type Rep (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base type Rep (MigrationScript oldStore newStore) = D1 ('MetaData "MigrationScript" "Lorentz.UStore.Migration.Base" "morley-upgradeable-0.3-inplace" 'True) (C1 ('MetaCons "MigrationScript" 'PrefixI 'True) (S1 ('MetaSel ('Just "unMigrationScript") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Lambda UStore_ UStore_))))
type Unwrappable (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base type Unwrappable (MigrationScript oldStore newStore) = GUnwrappable (Rep (MigrationScript oldStore newStore))
type ToT (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base type ToT (MigrationScript oldStore newStore) = GValueType (Rep (MigrationScript oldStore newStore))
type TypeDocFieldDescriptions (MigrationScript oldStore newStore) Source #
Instance details Defined in Lorentz.UStore.Migration.Base type TypeDocFieldDescriptions (MigrationScript oldStore newStore) = '[] :: [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]

type MigrationScriptFrom oldStore = MigrationScript oldStore SomeUTemplate Source #

Corner case of MigrationScript with some type argument unknown.

You can turn this into MigrationScript using checkedCoerce.

type MigrationScriptTo newStore = MigrationScript SomeUTemplate newStore Source #

newtype UContractRouter (ver :: VersionKind) Source #

Keeps parameter dispatching logic.

Constructors

UContractRouter
Fields unUContractRouter :: Lambda (VerParam ver, VerUStore ver) ([Operation], VerUStore ver)

Instances

Instances details

Show (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods showsPrec :: Int -> UContractRouter ver -> ShowS # show :: UContractRouter ver -> String # showList :: [UContractRouter ver] -> ShowS #
Generic (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type Rep (UContractRouter ver) :: Type -> Type # Methods from :: UContractRouter ver -> Rep (UContractRouter ver) x # to :: Rep (UContractRouter ver) x -> UContractRouter ver #
Wrappable (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type Unwrappable (UContractRouter ver) #
MapLorentzInstr (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods mapLorentzInstr :: (forall (i :: [Type]) (o :: [Type]). (i :-> o) -> i :-> o) -> UContractRouter ver -> UContractRouter ver #
HasAnnotation (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods getAnnotation :: FollowEntrypointFlag -> Notes (ToT (UContractRouter ver)) # annOptions :: AnnOptions #
IsoValue (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type ToT (UContractRouter ver) :: T # Methods toVal :: UContractRouter ver -> Value (ToT (UContractRouter ver)) # fromVal :: Value (ToT (UContractRouter ver)) -> UContractRouter ver #
(Typeable ver, Typeable (VerInterface ver), Typeable (VerUStoreTemplate ver), TypeHasDoc (VerUStore ver)) => TypeHasDoc (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type TypeDocFieldDescriptions (UContractRouter ver) :: FieldDescriptions # Methods typeDocName :: Proxy (UContractRouter ver) -> Text # typeDocMdDescription :: Markdown # typeDocMdReference :: Proxy (UContractRouter ver) -> WithinParens -> Markdown # typeDocDependencies :: Proxy (UContractRouter ver) -> [SomeDocDefinitionItem] # typeDocHaskellRep :: TypeDocHaskellRep (UContractRouter ver) # typeDocMichelsonRep :: TypeDocMichelsonRep (UContractRouter ver) #
(CanCastTo (VerParam ver1) (VerParam ver2), CanCastTo (VerUStore ver1) (VerUStore ver2)) => CanCastTo (UContractRouter ver1 :: Type) (UContractRouter ver2 :: Type) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods castDummy :: Proxy (UContractRouter ver1) -> Proxy (UContractRouter ver2) -> () #
type Rep (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type Rep (UContractRouter ver) = D1 ('MetaData "UContractRouter" "Lorentz.Contracts.Upgradeable.Common.Base" "morley-upgradeable-0.3-inplace" 'True) (C1 ('MetaCons "UContractRouter" 'PrefixI 'True) (S1 ('MetaSel ('Just "unUContractRouter") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Lambda (VerParam ver, VerUStore ver) ([Operation], VerUStore ver)))))
type Unwrappable (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type Unwrappable (UContractRouter ver) = GUnwrappable (Rep (UContractRouter ver))
type ToT (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type ToT (UContractRouter ver) = GValueType (Rep (UContractRouter ver))
type TypeDocFieldDescriptions (UContractRouter ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type TypeDocFieldDescriptions (UContractRouter ver) = '[] :: [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]

type SomeUContractRouter = UContractRouter (SomeContractVersion ()) Source #

data UpgradeableEntrypointsKind Source #

Common marker for upgradeable, or virtual, entrypoints. Can be used when each upgradeable entrypoint is simple, i.e. does not itself consist of multiple entrypoints.

Instances

Instances details

EntrypointKindHasDoc UpgradeableEntrypointsKind Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Doc Methods entrypointKindPos :: Natural # entrypointKindSectionName :: Text # entrypointKindSectionDescription :: Maybe Markdown #

newtype PermanentImpl ver Source #

Implementation of permanent entrypoints.

This will be injected into contract storage as one of fields, so make sure that code within does not exceed several instructions; an actual entrypoint logic can be put into UStore and called from within PermanentImpl only when necessary.

Regarding documentation - this have to provide code pieces wrapped into DEntrypoint with PermanentEntrypointsKind, so always use entryCase as implementation of this type or inject documentation of code which does so unless you know what you are doing.

Constructors

PermanentImpl
Fields unPermanentImpl :: Entrypoint (VerPermanent ver) (VerUStore ver)

Instances

Instances details

Show (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods showsPrec :: Int -> PermanentImpl ver -> ShowS # show :: PermanentImpl ver -> String # showList :: [PermanentImpl ver] -> ShowS #
Generic (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type Rep (PermanentImpl ver) :: Type -> Type # Methods from :: PermanentImpl ver -> Rep (PermanentImpl ver) x # to :: Rep (PermanentImpl ver) x -> PermanentImpl ver #
Wrappable (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type Unwrappable (PermanentImpl ver) #
MapLorentzInstr (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods mapLorentzInstr :: (forall (i :: [Type]) (o :: [Type]). (i :-> o) -> i :-> o) -> PermanentImpl ver -> PermanentImpl ver #
HasAnnotation (VerPermanent ver) => HasAnnotation (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods getAnnotation :: FollowEntrypointFlag -> Notes (ToT (PermanentImpl ver)) # annOptions :: AnnOptions #
WellTypedIsoValue (VerPermanent ver) => IsoValue (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type ToT (PermanentImpl ver) :: T # Methods toVal :: PermanentImpl ver -> Value (ToT (PermanentImpl ver)) # fromVal :: Value (ToT (PermanentImpl ver)) -> PermanentImpl ver #
(Typeable ver, Typeable (VerUStoreTemplate ver), TypeHasDoc (VerUStore ver), TypeHasDoc (VerPermanent ver), KnownValue (VerPermanent ver)) => TypeHasDoc (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Associated Types type TypeDocFieldDescriptions (PermanentImpl ver) :: FieldDescriptions # Methods typeDocName :: Proxy (PermanentImpl ver) -> Text # typeDocMdDescription :: Markdown # typeDocMdReference :: Proxy (PermanentImpl ver) -> WithinParens -> Markdown # typeDocDependencies :: Proxy (PermanentImpl ver) -> [SomeDocDefinitionItem] # typeDocHaskellRep :: TypeDocHaskellRep (PermanentImpl ver) # typeDocMichelsonRep :: TypeDocMichelsonRep (PermanentImpl ver) #
(CanCastTo (VerPermanent ver1) (VerPermanent ver2), CanCastTo (VerUStore ver1) (VerUStore ver2)) => CanCastTo (PermanentImpl ver1 :: Type) (PermanentImpl ver2 :: Type) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods castDummy :: Proxy (PermanentImpl ver1) -> Proxy (PermanentImpl ver2) -> () #
type Rep (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type Rep (PermanentImpl ver) = D1 ('MetaData "PermanentImpl" "Lorentz.Contracts.Upgradeable.Common.Base" "morley-upgradeable-0.3-inplace" 'True) (C1 ('MetaCons "PermanentImpl" 'PrefixI 'True) (S1 ('MetaSel ('Just "unPermanentImpl") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Entrypoint (VerPermanent ver) (VerUStore ver)))))
type Unwrappable (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type Unwrappable (PermanentImpl ver) = GUnwrappable (Rep (PermanentImpl ver))
type ToT (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type ToT (PermanentImpl ver) = GValueType (Rep (PermanentImpl ver))
type TypeDocFieldDescriptions (PermanentImpl ver) Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base type TypeDocFieldDescriptions (PermanentImpl ver) = '[] :: [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]

type SomePermanentImpl perm = PermanentImpl (SomeContractVersion perm) Source #

data PermanentEntrypointsKind Source #

Common marker for permanent entrypoints. Can be used when parameter for permanent entrypoints is flat, i.e. does not have nested subparameters with multiple entrypoints.

Instances

Instances details

EntrypointKindHasDoc PermanentEntrypointsKind Source #
Instance details Defined in Lorentz.Contracts.Upgradeable.Common.Base Methods entrypointKindPos :: Natural # entrypointKindSectionName :: Text # entrypointKindSectionDescription :: Maybe Markdown #

mkUContractRouter :: ([VerParam ver, VerUStore ver] :-> '[([Operation], VerUStore ver)]) -> UContractRouter ver Source #

coerceUContractRouter :: (Coercible_ (VerParam s1) (VerParam s2), Coercible_ (VerUStore s1) (VerUStore s2)) => UContractRouter s1 -> UContractRouter s2 Source #

emptyPermanentImpl :: VerPermanent ver ~ Empty => PermanentImpl ver Source #

Common implementation of permanent part in case contract has no such.

mkSmallPermanentImpl :: forall ver dt out inp clauses. (CaseTC dt out inp clauses, DocumentEntrypoints PermanentEntrypointsKind dt, dt ~ VerPermanent ver, inp ~ '[VerUStore ver], out ~ ContractOut (VerUStore ver)) => IsoRecTuple clauses -> PermanentImpl ver Source #

Construct implementation of permanent part in a common case; this works similarly to entryCase.

Use this function only for very small implementations.

Re-exports

data Nat #

(Kind) This is the kind of type-level natural numbers.

Instances

Instances details

PShow Nat
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg1 arg2 :: Symbol # type Show_ arg :: Symbol # type ShowList arg arg1 :: Symbol #
SShow Nat
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: forall (t1 :: Nat) (t2 :: Nat) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) # sShow_ :: forall (t :: Nat). Sing t -> Sing (Apply Show_Sym0 t) # sShowList :: forall (t1 :: [Nat]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #
PEnum Nat
Instance details Defined in Data.Singletons.Prelude.Enum Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg1 :: [a] # type EnumFromThenTo arg arg1 arg2 :: [a] #
SEnum Nat
Instance details Defined in Data.Singletons.Prelude.Enum Methods sSucc :: forall (t :: Nat). Sing t -> Sing (Apply SuccSym0 t) # sPred :: forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t) # sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: forall (t :: Nat). Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) # sEnumFromThenTo :: forall (t1 :: Nat) (t2 :: Nat) (t3 :: Nat). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) #
PNum Nat
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
SNum Nat
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t) # sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t) # sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) #
KnownNat n => Reifies (n :: Nat) Integer
Instance details Defined in Data.Reflection Methods reflect :: proxy n -> Integer #
SingI Log2Sym0
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing Log2Sym0 #
SingI (<=?@#@$)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (<=?@#@$) #
SingI ModSym0
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing ModSym0 #
SingI DivSym0
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing DivSym0 #
SingI (^@#@$)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (^@#@$) #
SingI EftNatSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EftNatSym0 #
SingI EfdtNatDnSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EfdtNatDnSym0 #
SingI EfdtNatSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EfdtNatSym0 #
SingI EfdtNatUpSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EfdtNatUpSym0 #
SuppressUnusedWarnings FromEnum_6989586621680203592Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings FromEnum_6989586621680203616Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ToEnum_6989586621680203579Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ToEnum_6989586621680203600Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings KnownNatSym0
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings Log2Sym0
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings FromEnum_6989586621680180412Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings Pred_6989586621680180398Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings Succ_6989586621680180391Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ToEnum_6989586621680180405Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ToEnum_6989586621680203623Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsPrec_6989586621680653401Sym0
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsPrec_6989586621680653423Sym0
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (<=?@#@$)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings EftNatSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings EnumFromTo_6989586621680180420Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings RemSym0
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings QuotSym0
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ModSym0
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings DivSym0
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (^@#@$)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings QuotRemSym0
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings DivModSym0
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings EfdtNatDnSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings EfdtNatSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings EfdtNatUpSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings EnumFromThenTo_6989586621680180436Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsNatSym0
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsPrec_6989586621680636163Sym0
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsPrec_6989586621680653251Sym0
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsPrec_6989586621680653451Sym0
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsPrec_6989586621681186574Sym0
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsPrec_6989586621681186600Sym0
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings FromEnum_6989586621680203633Sym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((<=?@#@$$) x) #
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (ModSym1 x) #
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (DivSym1 x) #
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((^@#@$$) x) #
SingI (ListlengthSym0 :: TyFun [a] Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListlengthSym0 #
SingI (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListindexSym0 #
SingI (LengthSym0 :: TyFun [a] Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing LengthSym0 #
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (!!@#@$) #
SingI d => SingI (EftNatSym1 d :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EftNatSym1 d) #
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing FromIntegerSym0 #
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing ToEnumSym0 #
SingI (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListtakeSym0 #
SingI (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListsplitAtSym0 #
SingI (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListdropSym0 #
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TakeSym0 #
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SplitAtSym0 #
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropSym0 #
SingI d => SingI (EfdtNatDnSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatDnSym1 d) #
SingI d => SingI (EfdtNatSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatSym1 d) #
SingI d => SingI (EfdtNatUpSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatUpSym1 d) #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 #
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ReplicateSym0 #
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndicesSym0 #
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndexSym0 #
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing FromEnumSym0 #
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndicesSym0 #
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndexSym0 #
SuppressUnusedWarnings (ListlengthSym0 :: TyFun [a] Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (LengthSym0 :: TyFun [a] Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Length_6989586621680822577Sym0 :: TyFun [a] Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((<=?@#@$$) a6989586621679910080 :: TyFun Nat Bool -> Type)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EftNatSym1 a6989586621680180297 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EnumFromTo_6989586621680180420Sym1 a6989586621680180429 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (RemSym1 a6989586621679947797 :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (QuotSym1 a6989586621679947808 :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ModSym1 a6989586621679947332 :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (DivSym1 a6989586621679946991 :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((^@#@$$) a6989586621679909783 :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (QuotRemSym1 a6989586621679947819 :: TyFun Nat (Nat, Nat) -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (DivModSym1 a6989586621679947826 :: TyFun Nat (Nat, Nat) -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnum_6989586621681202456Sym0 :: TyFun Nat (Min a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromInteger_6989586621681202618Sym0 :: TyFun Nat (Min a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnum_6989586621681202733Sym0 :: TyFun Nat (Max a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromInteger_6989586621681202895Sym0 :: TyFun Nat (Max a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnum_6989586621681203181Sym0 :: TyFun Nat (First a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnum_6989586621681203389Sym0 :: TyFun Nat (Last a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnum_6989586621681203558Sym0 :: TyFun Nat (WrappedMonoid a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnum_6989586621681011727Sym0 :: TyFun Nat (Identity a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Identity Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromInteger_6989586621681011824Sym0 :: TyFun Nat (Identity a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Identity Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromInteger_6989586621680268620Sym0 :: TyFun Nat (Sum a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromInteger_6989586621680268749Sym0 :: TyFun Nat (Product a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromInteger_6989586621679975423Sym0 :: TyFun Nat (Down a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680636145Sym0 :: TyFun Nat ([a] ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680653283Sym0 :: TyFun Nat (Maybe a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EfdtNatDnSym1 a6989586621680180205 :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EfdtNatSym1 a6989586621680180279 :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EfdtNatUpSym1 a6989586621680180242 :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EnumFromThenTo_6989586621680180436Sym1 a6989586621680180448 :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680636113Sym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186687Sym0 :: TyFun Nat (Min a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186716Sym0 :: TyFun Nat (Max a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186745Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186774Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186803Sym0 :: TyFun Nat (WrappedMonoid m ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186519Sym0 :: TyFun Nat (Option a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681011844Sym0 :: TyFun Nat (Identity a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Identity Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680697367Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monoid Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680697396Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monoid Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186548Sym0 :: TyFun Nat (Dual a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186629Sym0 :: TyFun Nat (Sum a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681186658Sym0 :: TyFun Nat (Product a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680653377Sym0 :: TyFun Nat (NonEmpty a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnum_6989586621681202465Sym0 :: TyFun (Min a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnum_6989586621681202742Sym0 :: TyFun (Max a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnum_6989586621681203190Sym0 :: TyFun (First a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnum_6989586621681203398Sym0 :: TyFun (Last a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnum_6989586621681203567Sym0 :: TyFun (WrappedMonoid a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Length_6989586621681011993Sym0 :: TyFun (Identity a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Identity Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnum_6989586621681011734Sym0 :: TyFun (Identity a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Identity Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Length_6989586621680822986Sym0 :: TyFun (Dual a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Length_6989586621680823161Sym0 :: TyFun (Sum a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Length_6989586621680823336Sym0 :: TyFun (Product a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndicesSym1 d) #
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndexSym1 d) #
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndicesSym1 d) #
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndexSym1 d) #
(SingI d1, SingI d2) => SingI (EfdtNatDnSym2 d1 d2 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatDnSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (EfdtNatSym2 d1 d2 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (EfdtNatUpSym2 d1 d2 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatUpSym2 d1 d2) #
SingI d => SingI (ListindexSym1 d :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListindexSym1 d) #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ((!!@#@$$) d) #
SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ReplicateM_Sym0 #
SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods sing :: Sing ReplicateMSym0 #
SuppressUnusedWarnings (FindIndicesSym1 a6989586621680378968 :: TyFun [a] [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FindIndexSym1 a6989586621680378991 :: TyFun [a] (Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ElemIndicesSym1 a6989586621680379000 :: TyFun [a] [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ElemIndexSym1 a6989586621680379009 :: TyFun [a] (Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Length_6989586621680822759Sym0 :: TyFun (Either a1 a2) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EfdtNatDnSym2 a6989586621680180205 a6989586621680180206 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EfdtNatSym2 a6989586621680180279 a6989586621680180280 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EfdtNatUpSym2 a6989586621680180242 a6989586621680180243 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (EnumFromThenTo_6989586621680180436Sym2 a6989586621680180448 a6989586621680180449 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ListindexSym1 a6989586621680764614 :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ((!!@#@$$) a6989586621680378633 :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ToEnum_6989586621680786603Sym0 :: TyFun Nat (Proxy s) -> Type)
Instance details Defined in Data.Singletons.Prelude.Proxy Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680653337Sym0 :: TyFun Nat (Either a b ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680636181Sym0 :: TyFun Nat ((a, b) ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681203049Sym0 :: TyFun Nat (Arg a b ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680786572Sym0 :: TyFun Nat (Proxy s ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Proxy Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Length_6989586621680822833Sym0 :: TyFun (Proxy a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnum_6989586621680786597Sym0 :: TyFun (Proxy s) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Proxy Methods suppressUnusedWarnings :: () #
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing LengthSym0 #
SuppressUnusedWarnings (ToEnum_6989586621681043885Sym0 :: TyFun Nat (Const a b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromInteger_6989586621681043982Sym0 :: TyFun Nat (Const a b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680636196Sym0 :: TyFun Nat ((a, b, c) ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621681044002Sym0 :: TyFun Nat (Const a b ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621680378972BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) -> Type) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Length_6989586621680822341Sym0 :: TyFun (t a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (LengthSym0 :: TyFun (t a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621681500653LoopSym0 :: TyFun k (TyFun (m6989586621681500247 a6989586621681500248) (TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) -> Type) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621681500635LoopSym0 :: TyFun k (TyFun (m6989586621681500245 a) (TyFun Nat (m6989586621681500245 ()) -> Type) -> Type) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (FromEnum_6989586621681043892Sym0 :: TyFun (Const a b) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680636212Sym0 :: TyFun Nat ((a, b, c, d) ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621680378972BuildListSym1 p6989586621680378970 :: TyFun k2 (TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621681500653LoopSym1 cnt06989586621681500651 :: TyFun (m6989586621681500247 a6989586621681500248) (TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621681500635LoopSym1 cnt06989586621681500633 :: TyFun (m6989586621681500245 a) (TyFun Nat (m6989586621681500245 ()) -> Type) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621681500653LoopSym2 cnt06989586621681500651 f6989586621681500652 :: TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621681500635LoopSym2 cnt06989586621681500633 f6989586621681500634 :: TyFun Nat (m6989586621681500245 ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621680378972BuildListSym2 p6989586621680378970 xs6989586621680378971 :: TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680636229Sym0 :: TyFun Nat ((a, b, c, d, e) ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Let6989586621680378972BuildListSym3 p6989586621680378970 xs6989586621680378971 a6989586621680378973 :: TyFun [b6989586621680374883] [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680636247Sym0 :: TyFun Nat ((a, b, c, d, e, f) ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621680636266Sym0 :: TyFun Nat ((a, b, c, d, e, f, g) ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods suppressUnusedWarnings :: () #
type Sing
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Demote Nat
Instance details Defined in Data.Singletons.TypeLits.Internal type Demote Nat = Natural
type MulK Nat Nat
Instance details Defined in Time.Rational type MulK Nat Nat = Nat
type MulK Nat Rat
Instance details Defined in Time.Rational type MulK Nat Rat = Rat
type MulK Rat Nat
Instance details Defined in Time.Rational type MulK Rat Nat = Rat
type DivK Nat Nat
Instance details Defined in Time.Rational type DivK Nat Nat = Rat
type DivK Nat Rat
Instance details Defined in Time.Rational type DivK Nat Rat = Rat
type DivK Rat Nat
Instance details Defined in Time.Rational type DivK Rat Nat = Rat
type Show_ (arg :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg :: Nat) = Apply (Show__6989586621680636125Sym0 :: TyFun Nat Symbol -> Type) arg
type FromEnum (a :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type FromEnum (a :: Nat) = Apply FromEnum_6989586621680180412Sym0 a
type ToEnum a
Instance details Defined in Data.Singletons.Prelude.Enum type ToEnum a = Apply ToEnum_6989586621680180405Sym0 a
type Pred (a :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Pred (a :: Nat) = Apply Pred_6989586621680180398Sym0 a
type Succ (a :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Succ (a :: Nat) = Apply Succ_6989586621680180391Sym0 a
type FromInteger a
Instance details Defined in Data.Singletons.Prelude.Num type FromInteger a = a
type Signum (a :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type Signum (a :: Nat) = SignumNat a
type Abs (a :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type Abs (a :: Nat) = a
type Negate (a :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type Negate (a :: Nat) = Error "Cannot negate a natural number" :: Nat
type ShowList (arg1 :: [Nat]) arg2
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Nat]) arg2 = Apply (Apply (ShowList_6989586621680636133Sym0 :: TyFun [Nat] (Symbol ~> Symbol) -> Type) arg1) arg2
type EnumFromTo (a1 :: Nat) (a2 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type EnumFromTo (a1 :: Nat) (a2 :: Nat) = Apply (Apply EnumFromTo_6989586621680180420Sym0 a1) a2
type (a :: Nat) * (b :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) * (b :: Nat) = a * b
type (a :: Nat) - (b :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) - (b :: Nat) = a - b
type (a :: Nat) + (b :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type (a :: Nat) + (b :: Nat) = a + b
type Min (arg1 :: Nat) (arg2 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type Min (arg1 :: Nat) (arg2 :: Nat) = Apply (Apply (Min_6989586621679836854Sym0 :: TyFun Nat (Nat ~> Nat) -> Type) arg1) arg2
type Max (arg1 :: Nat) (arg2 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type Max (arg1 :: Nat) (arg2 :: Nat) = Apply (Apply (Max_6989586621679836838Sym0 :: TyFun Nat (Nat ~> Nat) -> Type) arg1) arg2
type (arg1 :: Nat) >= (arg2 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) >= (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679836822Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg1) arg2
type (arg1 :: Nat) > (arg2 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) > (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679836806Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg1) arg2
type (arg1 :: Nat) <= (arg2 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) <= (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679836790Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg1) arg2
type (arg1 :: Nat) < (arg2 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type (arg1 :: Nat) < (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679836774Sym0 :: TyFun Nat (Nat ~> Bool) -> Type) arg1) arg2
type Compare (a :: Nat) (b :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type Compare (a :: Nat) (b :: Nat) = CmpNat a b
type (x :: Nat) /= (y :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Nat) /= (y :: Nat) = Not (x == y)
type (x :: Nat) == (y :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Nat) == (y :: Nat) = DefaultEq x y
type (a :: Nat) * (b :: Nat)
Instance details Defined in Time.Rational type (a :: Nat) * (b :: Nat) = a * b
type (a :: Nat) * (b :: Rat)
Instance details Defined in Time.Rational type (a :: Nat) * (b :: Rat) = MulNatRat a b
type (a :: Rat) * (b :: Nat)
Instance details Defined in Time.Rational type (a :: Rat) * (b :: Nat) = MulNatRat b a
type (a :: Nat) / (b :: Nat)
Instance details Defined in Time.Rational type (a :: Nat) / (b :: Nat) = a % b
type (a :: Nat) / (b :: Rat)
Instance details Defined in Time.Rational type (a :: Nat) / (b :: Rat) = DivRat (a :% 1) b
type (a :: Rat) / (b :: Nat)
Instance details Defined in Time.Rational type (a :: Rat) / (b :: Nat) = DivRatNat a b
type ShowsPrec _1 (n :: Nat) x
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec _1 (n :: Nat) x = ShowsNat n x
type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type EnumFromThenTo (a1 :: Nat) (a2 :: Nat) (a3 :: Nat) = Apply (Apply (Apply EnumFromThenTo_6989586621680180436Sym0 a1) a2) a3
type Apply FromEnum_6989586621680203592Sym0 (a6989586621680203596 :: Bool)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply FromEnum_6989586621680203592Sym0 (a6989586621680203596 :: Bool) = FromEnum_6989586621680203592Sym1 a6989586621680203596
type Apply FromEnum_6989586621680203616Sym0 (a6989586621680203620 :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply FromEnum_6989586621680203616Sym0 (a6989586621680203620 :: Ordering) = FromEnum_6989586621680203616Sym1 a6989586621680203620
type Apply ToEnum_6989586621680203579Sym0 (a6989586621680203583 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply ToEnum_6989586621680203579Sym0 (a6989586621680203583 :: Nat) = ToEnum_6989586621680203579Sym1 a6989586621680203583
type Apply ToEnum_6989586621680203600Sym0 (a6989586621680203604 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply ToEnum_6989586621680203600Sym0 (a6989586621680203604 :: Nat) = ToEnum_6989586621680203600Sym1 a6989586621680203604
type Apply KnownNatSym0 (a6989586621679946208 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply KnownNatSym0 (a6989586621679946208 :: Nat) = KnownNatSym1 a6989586621679946208
type Apply Log2Sym0 (a6989586621679946778 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply Log2Sym0 (a6989586621679946778 :: Nat) = Log2Sym1 a6989586621679946778
type Apply FromEnum_6989586621680180412Sym0 (a6989586621680180416 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply FromEnum_6989586621680180412Sym0 (a6989586621680180416 :: Nat) = FromEnum_6989586621680180412Sym1 a6989586621680180416
type Apply Pred_6989586621680180398Sym0 (a6989586621680180402 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply Pred_6989586621680180398Sym0 (a6989586621680180402 :: Nat) = Pred_6989586621680180398Sym1 a6989586621680180402
type Apply Succ_6989586621680180391Sym0 (a6989586621680180395 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply Succ_6989586621680180391Sym0 (a6989586621680180395 :: Nat) = Succ_6989586621680180391Sym1 a6989586621680180395
type Apply ToEnum_6989586621680180405Sym0 (a6989586621680180409 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply ToEnum_6989586621680180405Sym0 (a6989586621680180409 :: Nat) = ToEnum_6989586621680180405Sym1 a6989586621680180409
type Apply ToEnum_6989586621680203623Sym0 (a6989586621680203627 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply ToEnum_6989586621680203623Sym0 (a6989586621680203627 :: Nat) = ToEnum_6989586621680203623Sym1 a6989586621680203627
type Apply FromEnum_6989586621680203633Sym0 (a6989586621680203637 :: ())
Instance details Defined in Data.Singletons.Prelude.Enum type Apply FromEnum_6989586621680203633Sym0 (a6989586621680203637 :: ()) = FromEnum_6989586621680203633Sym1 a6989586621680203637
type Apply ((<=?@#@$$) a6989586621679910080 :: TyFun Nat Bool -> Type) (a6989586621679910081 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((<=?@#@$$) a6989586621679910080 :: TyFun Nat Bool -> Type) (a6989586621679910081 :: Nat) = a6989586621679910080 <=?@#@$$$ a6989586621679910081
type Apply (RemSym1 a6989586621679947797 :: TyFun Nat Nat -> Type) (a6989586621679947798 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply (RemSym1 a6989586621679947797 :: TyFun Nat Nat -> Type) (a6989586621679947798 :: Nat) = RemSym2 a6989586621679947797 a6989586621679947798
type Apply (QuotSym1 a6989586621679947808 :: TyFun Nat Nat -> Type) (a6989586621679947809 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotSym1 a6989586621679947808 :: TyFun Nat Nat -> Type) (a6989586621679947809 :: Nat) = QuotSym2 a6989586621679947808 a6989586621679947809
type Apply (ModSym1 a6989586621679947332 :: TyFun Nat Nat -> Type) (a6989586621679947333 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply (ModSym1 a6989586621679947332 :: TyFun Nat Nat -> Type) (a6989586621679947333 :: Nat) = ModSym2 a6989586621679947332 a6989586621679947333
type Apply (DivSym1 a6989586621679946991 :: TyFun Nat Nat -> Type) (a6989586621679946992 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply (DivSym1 a6989586621679946991 :: TyFun Nat Nat -> Type) (a6989586621679946992 :: Nat) = DivSym2 a6989586621679946991 a6989586621679946992
type Apply ((^@#@$$) a6989586621679909783 :: TyFun Nat Nat -> Type) (a6989586621679909784 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply ((^@#@$$) a6989586621679909783 :: TyFun Nat Nat -> Type) (a6989586621679909784 :: Nat) = a6989586621679909783 ^@#@$$$ a6989586621679909784
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (a6989586621679975349 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> Type) (a6989586621679975349 :: Nat) = FromIntegerSym1 a6989586621679975349 :: k2
type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621680180326 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (ToEnumSym0 :: TyFun Nat k2 -> Type) (a6989586621680180326 :: Nat) = ToEnumSym1 a6989586621680180326 :: k2
type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621680180329 :: a)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (FromEnumSym0 :: TyFun a Nat -> Type) (a6989586621680180329 :: a) = FromEnumSym1 a6989586621680180329
type Apply (ListindexSym1 a6989586621680764614 :: TyFun Nat a -> Type) (a6989586621680764615 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation type Apply (ListindexSym1 a6989586621680764614 :: TyFun Nat a -> Type) (a6989586621680764615 :: Nat) = ListindexSym2 a6989586621680764614 a6989586621680764615
type Apply ((!!@#@$$) a6989586621680378633 :: TyFun Nat a -> Type) (a6989586621680378634 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply ((!!@#@$$) a6989586621680378633 :: TyFun Nat a -> Type) (a6989586621680378634 :: Nat) = a6989586621680378633 !!@#@$$$ a6989586621680378634
type Apply (EftNatSym1 a6989586621680180297 :: TyFun Nat [Nat] -> Type) (a6989586621680180298 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EftNatSym1 a6989586621680180297 :: TyFun Nat [Nat] -> Type) (a6989586621680180298 :: Nat) = EftNatSym2 a6989586621680180297 a6989586621680180298
type Apply (EnumFromTo_6989586621680180420Sym1 a6989586621680180429 :: TyFun Nat [Nat] -> Type) (a6989586621680180430 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromTo_6989586621680180420Sym1 a6989586621680180429 :: TyFun Nat [Nat] -> Type) (a6989586621680180430 :: Nat) = EnumFromTo_6989586621680180420Sym2 a6989586621680180429 a6989586621680180430
type Apply (ToEnum_6989586621681202456Sym0 :: TyFun Nat (Min a) -> Type) (a6989586621681202462 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ToEnum_6989586621681202456Sym0 :: TyFun Nat (Min a) -> Type) (a6989586621681202462 :: Nat) = ToEnum_6989586621681202456Sym1 a6989586621681202462 :: Min a
type Apply (FromInteger_6989586621681202618Sym0 :: TyFun Nat (Min a) -> Type) (a6989586621681202624 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (FromInteger_6989586621681202618Sym0 :: TyFun Nat (Min a) -> Type) (a6989586621681202624 :: Nat) = FromInteger_6989586621681202618Sym1 a6989586621681202624 :: Min a
type Apply (ToEnum_6989586621681202733Sym0 :: TyFun Nat (Max a) -> Type) (a6989586621681202739 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ToEnum_6989586621681202733Sym0 :: TyFun Nat (Max a) -> Type) (a6989586621681202739 :: Nat) = ToEnum_6989586621681202733Sym1 a6989586621681202739 :: Max a
type Apply (FromInteger_6989586621681202895Sym0 :: TyFun Nat (Max a) -> Type) (a6989586621681202901 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (FromInteger_6989586621681202895Sym0 :: TyFun Nat (Max a) -> Type) (a6989586621681202901 :: Nat) = FromInteger_6989586621681202895Sym1 a6989586621681202901 :: Max a
type Apply (ToEnum_6989586621681203181Sym0 :: TyFun Nat (First a) -> Type) (a6989586621681203187 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ToEnum_6989586621681203181Sym0 :: TyFun Nat (First a) -> Type) (a6989586621681203187 :: Nat) = ToEnum_6989586621681203181Sym1 a6989586621681203187 :: First a
type Apply (ToEnum_6989586621681203389Sym0 :: TyFun Nat (Last a) -> Type) (a6989586621681203395 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ToEnum_6989586621681203389Sym0 :: TyFun Nat (Last a) -> Type) (a6989586621681203395 :: Nat) = ToEnum_6989586621681203389Sym1 a6989586621681203395 :: Last a
type Apply (ToEnum_6989586621681203558Sym0 :: TyFun Nat (WrappedMonoid a) -> Type) (a6989586621681203564 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ToEnum_6989586621681203558Sym0 :: TyFun Nat (WrappedMonoid a) -> Type) (a6989586621681203564 :: Nat) = ToEnum_6989586621681203558Sym1 a6989586621681203564 :: WrappedMonoid a
type Apply (ToEnum_6989586621681011727Sym0 :: TyFun Nat (Identity a) -> Type) (a6989586621681011731 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Identity type Apply (ToEnum_6989586621681011727Sym0 :: TyFun Nat (Identity a) -> Type) (a6989586621681011731 :: Nat) = ToEnum_6989586621681011727Sym1 a6989586621681011731 :: Identity a
type Apply (FromInteger_6989586621681011824Sym0 :: TyFun Nat (Identity a) -> Type) (a6989586621681011828 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Identity type Apply (FromInteger_6989586621681011824Sym0 :: TyFun Nat (Identity a) -> Type) (a6989586621681011828 :: Nat) = FromInteger_6989586621681011824Sym1 a6989586621681011828 :: Identity a
type Apply (FromInteger_6989586621680268620Sym0 :: TyFun Nat (Sum a) -> Type) (a6989586621680268624 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Apply (FromInteger_6989586621680268620Sym0 :: TyFun Nat (Sum a) -> Type) (a6989586621680268624 :: Nat) = FromInteger_6989586621680268620Sym1 a6989586621680268624 :: Sum a
type Apply (FromInteger_6989586621680268749Sym0 :: TyFun Nat (Product a) -> Type) (a6989586621680268753 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Apply (FromInteger_6989586621680268749Sym0 :: TyFun Nat (Product a) -> Type) (a6989586621680268753 :: Nat) = FromInteger_6989586621680268749Sym1 a6989586621680268753 :: Product a
type Apply (FromInteger_6989586621679975423Sym0 :: TyFun Nat (Down a) -> Type) (a6989586621679975427 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromInteger_6989586621679975423Sym0 :: TyFun Nat (Down a) -> Type) (a6989586621679975427 :: Nat) = FromInteger_6989586621679975423Sym1 a6989586621679975427 :: Down a
type Apply (EfdtNatDnSym2 a6989586621680180205 a6989586621680180206 :: TyFun Nat [Nat] -> Type) (a6989586621680180207 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EfdtNatDnSym2 a6989586621680180205 a6989586621680180206 :: TyFun Nat [Nat] -> Type) (a6989586621680180207 :: Nat) = EfdtNatDnSym3 a6989586621680180205 a6989586621680180206 a6989586621680180207
type Apply (EfdtNatSym2 a6989586621680180279 a6989586621680180280 :: TyFun Nat [Nat] -> Type) (a6989586621680180281 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EfdtNatSym2 a6989586621680180279 a6989586621680180280 :: TyFun Nat [Nat] -> Type) (a6989586621680180281 :: Nat) = EfdtNatSym3 a6989586621680180279 a6989586621680180280 a6989586621680180281
type Apply (EfdtNatUpSym2 a6989586621680180242 a6989586621680180243 :: TyFun Nat [Nat] -> Type) (a6989586621680180244 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EfdtNatUpSym2 a6989586621680180242 a6989586621680180243 :: TyFun Nat [Nat] -> Type) (a6989586621680180244 :: Nat) = EfdtNatUpSym3 a6989586621680180242 a6989586621680180243 a6989586621680180244
type Apply (EnumFromThenTo_6989586621680180436Sym2 a6989586621680180448 a6989586621680180449 :: TyFun Nat [Nat] -> Type) (a6989586621680180450 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromThenTo_6989586621680180436Sym2 a6989586621680180448 a6989586621680180449 :: TyFun Nat [Nat] -> Type) (a6989586621680180450 :: Nat) = EnumFromThenTo_6989586621680180436Sym3 a6989586621680180448 a6989586621680180449 a6989586621680180450
type Apply (Let6989586621681500635LoopSym2 cnt06989586621681500633 f6989586621681500634 :: TyFun Nat (m6989586621681500245 ()) -> Type) (a6989586621681500636 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681500635LoopSym2 cnt06989586621681500633 f6989586621681500634 :: TyFun Nat (m6989586621681500245 ()) -> Type) (a6989586621681500636 :: Nat) = Let6989586621681500635LoopSym3 cnt06989586621681500633 f6989586621681500634 a6989586621681500636
type Apply (Let6989586621681500653LoopSym2 cnt06989586621681500651 f6989586621681500652 :: TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) (a6989586621681500654 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681500653LoopSym2 cnt06989586621681500651 f6989586621681500652 :: TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) (a6989586621681500654 :: Nat) = Let6989586621681500653LoopSym3 cnt06989586621681500651 f6989586621681500652 a6989586621681500654
type Eval (Length (a2 ': as) :: Nat -> Type)
Instance details Defined in Fcf.Data.List type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)
type Eval (Length ('[] :: [a]) :: Nat -> Type)
Instance details Defined in Fcf.Data.List type Eval (Length ('[] :: [a]) :: Nat -> Type) = 0
type Eval (Sum ns :: Nat -> Type)
Instance details Defined in Fcf.Class.Foldable type Eval (Sum ns :: Nat -> Type) = Eval (Foldr (+) 0 ns)
type Eval (a + b :: Nat -> Type)
Instance details Defined in Fcf.Data.Nat type Eval (a + b :: Nat -> Type) = a + b
type Eval (a - b :: Nat -> Type)
Instance details Defined in Fcf.Data.Nat type Eval (a - b :: Nat -> Type) = a - b
type Eval (a * b :: Nat -> Type)
Instance details Defined in Fcf.Data.Nat type Eval (a * b :: Nat -> Type) = a * b
type Eval (a ^ b :: Nat -> Type)
Instance details Defined in Fcf.Data.Nat type Eval (a ^ b :: Nat -> Type) = a ^ b
type Apply ShowsPrec_6989586621680653401Sym0 (a6989586621680653411 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680653401Sym0 (a6989586621680653411 :: Nat) = ShowsPrec_6989586621680653401Sym1 a6989586621680653411
type Apply ShowsPrec_6989586621680653423Sym0 (a6989586621680653435 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680653423Sym0 (a6989586621680653435 :: Nat) = ShowsPrec_6989586621680653423Sym1 a6989586621680653435
type Apply (<=?@#@$) (a6989586621679910080 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (<=?@#@$) (a6989586621679910080 :: Nat) = (<=?@#@$$) a6989586621679910080
type Apply EftNatSym0 (a6989586621680180297 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply EftNatSym0 (a6989586621680180297 :: Nat) = EftNatSym1 a6989586621680180297
type Apply EnumFromTo_6989586621680180420Sym0 (a6989586621680180429 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply EnumFromTo_6989586621680180420Sym0 (a6989586621680180429 :: Nat) = EnumFromTo_6989586621680180420Sym1 a6989586621680180429
type Apply RemSym0 (a6989586621679947797 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply RemSym0 (a6989586621679947797 :: Nat) = RemSym1 a6989586621679947797
type Apply QuotSym0 (a6989586621679947808 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply QuotSym0 (a6989586621679947808 :: Nat) = QuotSym1 a6989586621679947808
type Apply ModSym0 (a6989586621679947332 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply ModSym0 (a6989586621679947332 :: Nat) = ModSym1 a6989586621679947332
type Apply DivSym0 (a6989586621679946991 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply DivSym0 (a6989586621679946991 :: Nat) = DivSym1 a6989586621679946991
type Apply (^@#@$) (a6989586621679909783 :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type Apply (^@#@$) (a6989586621679909783 :: Nat) = (^@#@$$) a6989586621679909783
type Apply QuotRemSym0 (a6989586621679947819 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply QuotRemSym0 (a6989586621679947819 :: Nat) = QuotRemSym1 a6989586621679947819
type Apply DivModSym0 (a6989586621679947826 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply DivModSym0 (a6989586621679947826 :: Nat) = DivModSym1 a6989586621679947826
type Apply EfdtNatDnSym0 (a6989586621680180205 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply EfdtNatDnSym0 (a6989586621680180205 :: Nat) = EfdtNatDnSym1 a6989586621680180205
type Apply EfdtNatSym0 (a6989586621680180279 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply EfdtNatSym0 (a6989586621680180279 :: Nat) = EfdtNatSym1 a6989586621680180279
type Apply EfdtNatUpSym0 (a6989586621680180242 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply EfdtNatUpSym0 (a6989586621680180242 :: Nat) = EfdtNatUpSym1 a6989586621680180242
type Apply EnumFromThenTo_6989586621680180436Sym0 (a6989586621680180448 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply EnumFromThenTo_6989586621680180436Sym0 (a6989586621680180448 :: Nat) = EnumFromThenTo_6989586621680180436Sym1 a6989586621680180448
type Apply ShowsNatSym0 (a6989586621680652779 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowsNatSym0 (a6989586621680652779 :: Nat) = ShowsNatSym1 a6989586621680652779
type Apply ShowsPrec_6989586621680636163Sym0 (a6989586621680636173 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680636163Sym0 (a6989586621680636173 :: Nat) = ShowsPrec_6989586621680636163Sym1 a6989586621680636173
type Apply ShowsPrec_6989586621680653251Sym0 (a6989586621680653259 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680653251Sym0 (a6989586621680653259 :: Nat) = ShowsPrec_6989586621680653251Sym1 a6989586621680653259
type Apply ShowsPrec_6989586621680653451Sym0 (a6989586621680653459 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply ShowsPrec_6989586621680653451Sym0 (a6989586621680653459 :: Nat) = ShowsPrec_6989586621680653451Sym1 a6989586621680653459
type Apply ShowsPrec_6989586621681186574Sym0 (a6989586621681186582 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply ShowsPrec_6989586621681186574Sym0 (a6989586621681186582 :: Nat) = ShowsPrec_6989586621681186574Sym1 a6989586621681186582
type Apply ShowsPrec_6989586621681186600Sym0 (a6989586621681186608 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply ShowsPrec_6989586621681186600Sym0 (a6989586621681186608 :: Nat) = ShowsPrec_6989586621681186600Sym1 a6989586621681186608
type Apply (QuotRemSym1 a6989586621679947819 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679947820 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply (QuotRemSym1 a6989586621679947819 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679947820 :: Nat) = QuotRemSym2 a6989586621679947819 a6989586621679947820
type Apply (DivModSym1 a6989586621679947826 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679947827 :: Nat)
Instance details Defined in Data.Singletons.TypeLits type Apply (DivModSym1 a6989586621679947826 :: TyFun Nat (Nat, Nat) -> Type) (a6989586621679947827 :: Nat) = DivModSym2 a6989586621679947826 a6989586621679947827
type Apply (ShowsPrec_6989586621680636145Sym0 :: TyFun Nat ([a] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636155 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680636145Sym0 :: TyFun Nat ([a] ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636155 :: Nat) = ShowsPrec_6989586621680636145Sym1 a6989586621680636155 :: TyFun [a] (Symbol ~> Symbol) -> Type
type Apply (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621680764625 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation type Apply (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621680764625 :: Nat) = ListsplitAtSym1 a6989586621680764625 :: TyFun [a] ([a], [a]) -> Type
type Apply (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680764636 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation type Apply (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680764636 :: Nat) = ListdropSym1 a6989586621680764636 :: TyFun [a] [a] -> Type
type Apply (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680764647 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation type Apply (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680764647 :: Nat) = ListtakeSym1 a6989586621680764647 :: TyFun [a] [a] -> Type
type Apply (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680378795 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680378795 :: Nat) = DropSym1 a6989586621680378795 :: TyFun [a] [a] -> Type
type Apply (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680378808 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type) (a6989586621680378808 :: Nat) = TakeSym1 a6989586621680378808 :: TyFun [a] [a] -> Type
type Apply (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621680378788 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type) (a6989586621680378788 :: Nat) = SplitAtSym1 a6989586621680378788 :: TyFun [a] ([a], [a]) -> Type
type Apply (ShowsPrec_6989586621680653283Sym0 :: TyFun Nat (Maybe a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680653293 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680653283Sym0 :: TyFun Nat (Maybe a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680653293 :: Nat) = ShowsPrec_6989586621680653283Sym1 a6989586621680653293 :: TyFun (Maybe a) (Symbol ~> Symbol) -> Type
type Apply (EfdtNatDnSym1 a6989586621680180205 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180206 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EfdtNatDnSym1 a6989586621680180205 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180206 :: Nat) = EfdtNatDnSym2 a6989586621680180205 a6989586621680180206
type Apply (EfdtNatSym1 a6989586621680180279 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180280 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EfdtNatSym1 a6989586621680180279 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180280 :: Nat) = EfdtNatSym2 a6989586621680180279 a6989586621680180280
type Apply (EfdtNatUpSym1 a6989586621680180242 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180243 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EfdtNatUpSym1 a6989586621680180242 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180243 :: Nat) = EfdtNatUpSym2 a6989586621680180242 a6989586621680180243
type Apply (EnumFromThenTo_6989586621680180436Sym1 a6989586621680180448 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180449 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Enum type Apply (EnumFromThenTo_6989586621680180436Sym1 a6989586621680180448 :: TyFun Nat (Nat ~> [Nat]) -> Type) (a6989586621680180449 :: Nat) = EnumFromThenTo_6989586621680180436Sym2 a6989586621680180448 a6989586621680180449
type Apply (ShowsPrec_6989586621680636113Sym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636119 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680636113Sym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636119 :: Nat) = ShowsPrec_6989586621680636113Sym1 a6989586621680636119 :: TyFun a (Symbol ~> Symbol) -> Type
type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636099 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636099 :: Nat) = ShowsPrecSym1 a6989586621680636099 :: TyFun a (Symbol ~> Symbol) -> Type
type Apply (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) (a6989586621680378653 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type) (a6989586621680378653 :: Nat) = ReplicateSym1 a6989586621680378653 :: TyFun a [a] -> Type
type Apply (ShowsPrec_6989586621681186687Sym0 :: TyFun Nat (Min a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186695 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186687Sym0 :: TyFun Nat (Min a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186695 :: Nat) = ShowsPrec_6989586621681186687Sym1 a6989586621681186695 :: TyFun (Min a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681186716Sym0 :: TyFun Nat (Max a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186724 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186716Sym0 :: TyFun Nat (Max a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186724 :: Nat) = ShowsPrec_6989586621681186716Sym1 a6989586621681186724 :: TyFun (Max a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681186745Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186753 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186745Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186753 :: Nat) = ShowsPrec_6989586621681186745Sym1 a6989586621681186753 :: TyFun (First a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681186774Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186782 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186774Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186782 :: Nat) = ShowsPrec_6989586621681186774Sym1 a6989586621681186782 :: TyFun (Last a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681186803Sym0 :: TyFun Nat (WrappedMonoid m ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186811 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186803Sym0 :: TyFun Nat (WrappedMonoid m ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186811 :: Nat) = ShowsPrec_6989586621681186803Sym1 a6989586621681186811 :: TyFun (WrappedMonoid m) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681186519Sym0 :: TyFun Nat (Option a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186527 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186519Sym0 :: TyFun Nat (Option a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186527 :: Nat) = ShowsPrec_6989586621681186519Sym1 a6989586621681186527 :: TyFun (Option a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681011844Sym0 :: TyFun Nat (Identity a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681011852 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Identity type Apply (ShowsPrec_6989586621681011844Sym0 :: TyFun Nat (Identity a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681011852 :: Nat) = ShowsPrec_6989586621681011844Sym1 a6989586621681011852 :: TyFun (Identity a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621680697367Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680697375 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Monoid type Apply (ShowsPrec_6989586621680697367Sym0 :: TyFun Nat (First a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680697375 :: Nat) = ShowsPrec_6989586621680697367Sym1 a6989586621680697375 :: TyFun (First a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621680697396Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680697404 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Monoid type Apply (ShowsPrec_6989586621680697396Sym0 :: TyFun Nat (Last a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680697404 :: Nat) = ShowsPrec_6989586621680697396Sym1 a6989586621680697404 :: TyFun (Last a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681186548Sym0 :: TyFun Nat (Dual a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186556 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186548Sym0 :: TyFun Nat (Dual a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186556 :: Nat) = ShowsPrec_6989586621681186548Sym1 a6989586621681186556 :: TyFun (Dual a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681186629Sym0 :: TyFun Nat (Sum a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186637 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186629Sym0 :: TyFun Nat (Sum a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186637 :: Nat) = ShowsPrec_6989586621681186629Sym1 a6989586621681186637 :: TyFun (Sum a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681186658Sym0 :: TyFun Nat (Product a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186666 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681186658Sym0 :: TyFun Nat (Product a ~> (Symbol ~> Symbol)) -> Type) (a6989586621681186666 :: Nat) = ShowsPrec_6989586621681186658Sym1 a6989586621681186666 :: TyFun (Product a) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621680653377Sym0 :: TyFun Nat (NonEmpty a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680653385 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680653377Sym0 :: TyFun Nat (NonEmpty a ~> (Symbol ~> Symbol)) -> Type) (a6989586621680653385 :: Nat) = ShowsPrec_6989586621680653377Sym1 a6989586621680653385 :: TyFun (NonEmpty a) (Symbol ~> Symbol) -> Type
type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) (a6989586621680379000 :: a)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type) (a6989586621680379000 :: a) = ElemIndicesSym1 a6989586621680379000
type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) (a6989586621680379009 :: a)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type) (a6989586621680379009 :: a) = ElemIndexSym1 a6989586621680379009
type Apply (ToEnum_6989586621680786603Sym0 :: TyFun Nat (Proxy s) -> Type) (a6989586621680786607 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Proxy type Apply (ToEnum_6989586621680786603Sym0 :: TyFun Nat (Proxy s) -> Type) (a6989586621680786607 :: Nat) = ToEnum_6989586621680786603Sym1 a6989586621680786607 :: Proxy s
type Apply (ShowsPrec_6989586621680653337Sym0 :: TyFun Nat (Either a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621680653347 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680653337Sym0 :: TyFun Nat (Either a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621680653347 :: Nat) = ShowsPrec_6989586621680653337Sym1 a6989586621680653347 :: TyFun (Either a b) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621680636181Sym0 :: TyFun Nat ((a, b) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636187 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680636181Sym0 :: TyFun Nat ((a, b) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636187 :: Nat) = ShowsPrec_6989586621680636181Sym1 a6989586621680636187 :: TyFun (a, b) (Symbol ~> Symbol) -> Type
type Apply (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) (a6989586621681500631 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type) (a6989586621681500631 :: Nat) = ReplicateM_Sym1 a6989586621681500631 :: TyFun (m a) (m ()) -> Type
type Apply (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) (a6989586621681500649 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type) (a6989586621681500649 :: Nat) = ReplicateMSym1 a6989586621681500649 :: TyFun (m a) (m [a]) -> Type
type Apply (ShowsPrec_6989586621681203049Sym0 :: TyFun Nat (Arg a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621681203057 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (ShowsPrec_6989586621681203049Sym0 :: TyFun Nat (Arg a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621681203057 :: Nat) = ShowsPrec_6989586621681203049Sym1 a6989586621681203057 :: TyFun (Arg a b) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621680786572Sym0 :: TyFun Nat (Proxy s ~> (Symbol ~> Symbol)) -> Type) (a6989586621680786580 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Proxy type Apply (ShowsPrec_6989586621680786572Sym0 :: TyFun Nat (Proxy s ~> (Symbol ~> Symbol)) -> Type) (a6989586621680786580 :: Nat) = ShowsPrec_6989586621680786572Sym1 a6989586621680786580 :: TyFun (Proxy s) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621680636196Sym0 :: TyFun Nat ((a, b, c) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636202 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680636196Sym0 :: TyFun Nat ((a, b, c) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636202 :: Nat) = ShowsPrec_6989586621680636196Sym1 a6989586621680636202 :: TyFun (a, b, c) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621681044002Sym0 :: TyFun Nat (Const a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621681044010 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Const type Apply (ShowsPrec_6989586621681044002Sym0 :: TyFun Nat (Const a b ~> (Symbol ~> Symbol)) -> Type) (a6989586621681044010 :: Nat) = ShowsPrec_6989586621681044002Sym1 a6989586621681044010 :: TyFun (Const a b) (Symbol ~> Symbol) -> Type
type Apply (Let6989586621680378972BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) -> Type) -> Type) (p6989586621680378970 :: k1)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (Let6989586621680378972BuildListSym0 :: TyFun k1 (TyFun k2 (TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) -> Type) -> Type) (p6989586621680378970 :: k1) = Let6989586621680378972BuildListSym1 p6989586621680378970 :: TyFun k2 (TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) -> Type
type Apply (Let6989586621681500635LoopSym0 :: TyFun k (TyFun (m6989586621681500245 a) (TyFun Nat (m6989586621681500245 ()) -> Type) -> Type) -> Type) (cnt06989586621681500633 :: k)
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681500635LoopSym0 :: TyFun k (TyFun (m6989586621681500245 a) (TyFun Nat (m6989586621681500245 ()) -> Type) -> Type) -> Type) (cnt06989586621681500633 :: k) = Let6989586621681500635LoopSym1 cnt06989586621681500633 :: TyFun (m6989586621681500245 a) (TyFun Nat (m6989586621681500245 ()) -> Type) -> Type
type Apply (Let6989586621681500653LoopSym0 :: TyFun k (TyFun (m6989586621681500247 a6989586621681500248) (TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) -> Type) -> Type) (cnt06989586621681500651 :: k)
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681500653LoopSym0 :: TyFun k (TyFun (m6989586621681500247 a6989586621681500248) (TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) -> Type) -> Type) (cnt06989586621681500651 :: k) = Let6989586621681500653LoopSym1 cnt06989586621681500651 :: TyFun (m6989586621681500247 a6989586621681500248) (TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) -> Type
type Apply (ShowsPrec_6989586621680636212Sym0 :: TyFun Nat ((a, b, c, d) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636218 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680636212Sym0 :: TyFun Nat ((a, b, c, d) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636218 :: Nat) = ShowsPrec_6989586621680636212Sym1 a6989586621680636218 :: TyFun (a, b, c, d) (Symbol ~> Symbol) -> Type
type Apply (Let6989586621680378972BuildListSym1 p6989586621680378970 :: TyFun k2 (TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) -> Type) (xs6989586621680378971 :: k2)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (Let6989586621680378972BuildListSym1 p6989586621680378970 :: TyFun k2 (TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) -> Type) (xs6989586621680378971 :: k2) = Let6989586621680378972BuildListSym2 p6989586621680378970 xs6989586621680378971 :: TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type
type Apply (Let6989586621680378972BuildListSym2 p6989586621680378970 xs6989586621680378971 :: TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) (a6989586621680378973 :: Nat)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (Let6989586621680378972BuildListSym2 p6989586621680378970 xs6989586621680378971 :: TyFun Nat ([b6989586621680374883] ~> [Nat]) -> Type) (a6989586621680378973 :: Nat) = Let6989586621680378972BuildListSym3 p6989586621680378970 xs6989586621680378971 a6989586621680378973 :: TyFun [b6989586621680374883] [Nat] -> Type
type Apply (ShowsPrec_6989586621680636229Sym0 :: TyFun Nat ((a, b, c, d, e) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636235 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680636229Sym0 :: TyFun Nat ((a, b, c, d, e) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636235 :: Nat) = ShowsPrec_6989586621680636229Sym1 a6989586621680636235 :: TyFun (a, b, c, d, e) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621680636247Sym0 :: TyFun Nat ((a, b, c, d, e, f) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636253 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680636247Sym0 :: TyFun Nat ((a, b, c, d, e, f) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636253 :: Nat) = ShowsPrec_6989586621680636247Sym1 a6989586621680636253 :: TyFun (a, b, c, d, e, f) (Symbol ~> Symbol) -> Type
type Apply (ShowsPrec_6989586621680636266Sym0 :: TyFun Nat ((a, b, c, d, e, f, g) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636272 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Show type Apply (ShowsPrec_6989586621680636266Sym0 :: TyFun Nat ((a, b, c, d, e, f, g) ~> (Symbol ~> Symbol)) -> Type) (a6989586621680636272 :: Nat) = ShowsPrec_6989586621680636266Sym1 a6989586621680636272 :: TyFun (a, b, c, d, e, f, g) (Symbol ~> Symbol) -> Type
type Apply (ToEnum_6989586621681043885Sym0 :: TyFun Nat (Const a b) -> Type) (a6989586621681043889 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Const type Apply (ToEnum_6989586621681043885Sym0 :: TyFun Nat (Const a b) -> Type) (a6989586621681043889 :: Nat) = ToEnum_6989586621681043885Sym1 a6989586621681043889 :: Const a b
type Apply (FromInteger_6989586621681043982Sym0 :: TyFun Nat (Const a b) -> Type) (a6989586621681043986 :: Nat)
Instance details Defined in Data.Singletons.Prelude.Const type Apply (FromInteger_6989586621681043982Sym0 :: TyFun Nat (Const a b) -> Type) (a6989586621681043986 :: Nat) = FromInteger_6989586621681043982Sym1 a6989586621681043986 :: Const a b
type Apply (ListlengthSym0 :: TyFun [a] Nat -> Type) (a6989586621680764605 :: [a])
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation type Apply (ListlengthSym0 :: TyFun [a] Nat -> Type) (a6989586621680764605 :: [a]) = ListlengthSym1 a6989586621680764605
type Apply (LengthSym0 :: TyFun [a] Nat -> Type) (a6989586621680378664 :: [a])
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (LengthSym0 :: TyFun [a] Nat -> Type) (a6989586621680378664 :: [a]) = LengthSym1 a6989586621680378664
type Apply (Length_6989586621680822577Sym0 :: TyFun [a] Nat -> Type) (a6989586621680822583 :: [a])
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (Length_6989586621680822577Sym0 :: TyFun [a] Nat -> Type) (a6989586621680822583 :: [a]) = Length_6989586621680822577Sym1 a6989586621680822583
type Apply (FromEnum_6989586621681202465Sym0 :: TyFun (Min a) Nat -> Type) (a6989586621681202469 :: Min a)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (FromEnum_6989586621681202465Sym0 :: TyFun (Min a) Nat -> Type) (a6989586621681202469 :: Min a) = FromEnum_6989586621681202465Sym1 a6989586621681202469
type Apply (FromEnum_6989586621681202742Sym0 :: TyFun (Max a) Nat -> Type) (a6989586621681202746 :: Max a)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (FromEnum_6989586621681202742Sym0 :: TyFun (Max a) Nat -> Type) (a6989586621681202746 :: Max a) = FromEnum_6989586621681202742Sym1 a6989586621681202746
type Apply (FromEnum_6989586621681203190Sym0 :: TyFun (First a) Nat -> Type) (a6989586621681203194 :: First a)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (FromEnum_6989586621681203190Sym0 :: TyFun (First a) Nat -> Type) (a6989586621681203194 :: First a) = FromEnum_6989586621681203190Sym1 a6989586621681203194
type Apply (FromEnum_6989586621681203398Sym0 :: TyFun (Last a) Nat -> Type) (a6989586621681203402 :: Last a)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (FromEnum_6989586621681203398Sym0 :: TyFun (Last a) Nat -> Type) (a6989586621681203402 :: Last a) = FromEnum_6989586621681203398Sym1 a6989586621681203402
type Apply (FromEnum_6989586621681203567Sym0 :: TyFun (WrappedMonoid a) Nat -> Type) (a6989586621681203571 :: WrappedMonoid a)
Instance details Defined in Data.Singletons.Prelude.Semigroup type Apply (FromEnum_6989586621681203567Sym0 :: TyFun (WrappedMonoid a) Nat -> Type) (a6989586621681203571 :: WrappedMonoid a) = FromEnum_6989586621681203567Sym1 a6989586621681203571
type Apply (FromEnum_6989586621681011734Sym0 :: TyFun (Identity a) Nat -> Type) (a6989586621681011738 :: Identity a)
Instance details Defined in Data.Singletons.Prelude.Identity type Apply (FromEnum_6989586621681011734Sym0 :: TyFun (Identity a) Nat -> Type) (a6989586621681011738 :: Identity a) = FromEnum_6989586621681011734Sym1 a6989586621681011738
type Apply (Length_6989586621681011993Sym0 :: TyFun (Identity a) Nat -> Type) (a6989586621681011997 :: Identity a)
Instance details Defined in Data.Singletons.Prelude.Identity type Apply (Length_6989586621681011993Sym0 :: TyFun (Identity a) Nat -> Type) (a6989586621681011997 :: Identity a) = Length_6989586621681011993Sym1 a6989586621681011997
type Apply (Length_6989586621680822986Sym0 :: TyFun (Dual a) Nat -> Type) (a6989586621680822990 :: Dual a)
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (Length_6989586621680822986Sym0 :: TyFun (Dual a) Nat -> Type) (a6989586621680822990 :: Dual a) = Length_6989586621680822986Sym1 a6989586621680822990
type Apply (Length_6989586621680823161Sym0 :: TyFun (Sum a) Nat -> Type) (a6989586621680823165 :: Sum a)
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (Length_6989586621680823161Sym0 :: TyFun (Sum a) Nat -> Type) (a6989586621680823165 :: Sum a) = Length_6989586621680823161Sym1 a6989586621680823165
type Apply (Length_6989586621680823336Sym0 :: TyFun (Product a) Nat -> Type) (a6989586621680823340 :: Product a)
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (Length_6989586621680823336Sym0 :: TyFun (Product a) Nat -> Type) (a6989586621680823340 :: Product a) = Length_6989586621680823336Sym1 a6989586621680823340
type Apply (Length_6989586621680822341Sym0 :: TyFun (t a) Nat -> Type) (a6989586621680822347 :: t a)
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (Length_6989586621680822341Sym0 :: TyFun (t a) Nat -> Type) (a6989586621680822347 :: t a) = Length_6989586621680822341Sym1 a6989586621680822347
type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (a6989586621680822156 :: t a)
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (LengthSym0 :: TyFun (t a) Nat -> Type) (a6989586621680822156 :: t a) = LengthSym1 a6989586621680822156
type Apply (FindIndicesSym1 a6989586621680378968 :: TyFun [a] [Nat] -> Type) (a6989586621680378969 :: [a])
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndicesSym1 a6989586621680378968 :: TyFun [a] [Nat] -> Type) (a6989586621680378969 :: [a]) = FindIndicesSym2 a6989586621680378968 a6989586621680378969
type Apply (ElemIndicesSym1 a6989586621680379000 :: TyFun [a] [Nat] -> Type) (a6989586621680379001 :: [a])
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndicesSym1 a6989586621680379000 :: TyFun [a] [Nat] -> Type) (a6989586621680379001 :: [a]) = ElemIndicesSym2 a6989586621680379000 a6989586621680379001
type Apply (FindIndexSym1 a6989586621680378991 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621680378992 :: [a])
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndexSym1 a6989586621680378991 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621680378992 :: [a]) = FindIndexSym2 a6989586621680378991 a6989586621680378992
type Apply (ElemIndexSym1 a6989586621680379009 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621680379010 :: [a])
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (ElemIndexSym1 a6989586621680379009 :: TyFun [a] (Maybe Nat) -> Type) (a6989586621680379010 :: [a]) = ElemIndexSym2 a6989586621680379009 a6989586621680379010
type Apply (Let6989586621680378972BuildListSym3 p6989586621680378970 xs6989586621680378971 a6989586621680378973 :: TyFun [b6989586621680374883] [Nat] -> Type) (a6989586621680378974 :: [b6989586621680374883])
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (Let6989586621680378972BuildListSym3 p6989586621680378970 xs6989586621680378971 a6989586621680378973 :: TyFun [b6989586621680374883] [Nat] -> Type) (a6989586621680378974 :: [b6989586621680374883]) = Let6989586621680378972BuildListSym4 p6989586621680378970 xs6989586621680378971 a6989586621680378973 a6989586621680378974
type Apply (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type) (a6989586621680764614 :: [a])
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation type Apply (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type) (a6989586621680764614 :: [a]) = ListindexSym1 a6989586621680764614
type Apply ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) (a6989586621680378633 :: [a])
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type) (a6989586621680378633 :: [a]) = (!!@#@$$) a6989586621680378633
type Apply (Let6989586621681500635LoopSym1 cnt06989586621681500633 :: TyFun (m6989586621681500245 a) (TyFun Nat (m6989586621681500245 ()) -> Type) -> Type) (f6989586621681500634 :: m6989586621681500245 a)
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681500635LoopSym1 cnt06989586621681500633 :: TyFun (m6989586621681500245 a) (TyFun Nat (m6989586621681500245 ()) -> Type) -> Type) (f6989586621681500634 :: m6989586621681500245 a) = Let6989586621681500635LoopSym2 cnt06989586621681500633 f6989586621681500634
type Apply (Let6989586621681500653LoopSym1 cnt06989586621681500651 :: TyFun (m6989586621681500247 a6989586621681500248) (TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) -> Type) (f6989586621681500652 :: m6989586621681500247 a6989586621681500248)
Instance details Defined in Data.Singletons.Prelude.Monad type Apply (Let6989586621681500653LoopSym1 cnt06989586621681500651 :: TyFun (m6989586621681500247 a6989586621681500248) (TyFun Nat (m6989586621681500247 [a6989586621681500248]) -> Type) -> Type) (f6989586621681500652 :: m6989586621681500247 a6989586621681500248) = Let6989586621681500653LoopSym2 cnt06989586621681500651 f6989586621681500652
type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type)
Instance details Defined in Fcf.Data.List type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) = Eval (If (Eval (p a2)) (Pure ('Just 0)) ((Map ((+) 1) :: Maybe Nat -> Maybe Nat -> Type) =<< FindIndex p as))
type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type)
Instance details Defined in Fcf.Data.List type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type) = 'Nothing :: Maybe Nat
type Eval (NumIter a s :: Maybe (k, Nat) -> Type)
Instance details Defined in Fcf.Data.List type Eval (NumIter a s :: Maybe (k, Nat) -> Type) = If (Eval (s > 0)) ('Just '(a, s - 1)) ('Nothing :: Maybe (k, Nat))
type Apply (Length_6989586621680822759Sym0 :: TyFun (Either a1 a2) Nat -> Type) (a6989586621680822763 :: Either a1 a2)
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (Length_6989586621680822759Sym0 :: TyFun (Either a1 a2) Nat -> Type) (a6989586621680822763 :: Either a1 a2) = Length_6989586621680822759Sym1 a6989586621680822763
type Apply (Length_6989586621680822833Sym0 :: TyFun (Proxy a) Nat -> Type) (a6989586621680822837 :: Proxy a)
Instance details Defined in Data.Singletons.Prelude.Foldable type Apply (Length_6989586621680822833Sym0 :: TyFun (Proxy a) Nat -> Type) (a6989586621680822837 :: Proxy a) = Length_6989586621680822833Sym1 a6989586621680822837
type Apply (FromEnum_6989586621680786597Sym0 :: TyFun (Proxy s) Nat -> Type) (a6989586621680786601 :: Proxy s)
Instance details Defined in Data.Singletons.Prelude.Proxy type Apply (FromEnum_6989586621680786597Sym0 :: TyFun (Proxy s) Nat -> Type) (a6989586621680786601 :: Proxy s) = FromEnum_6989586621680786597Sym1 a6989586621680786601
type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) (a6989586621680378968 :: a ~> Bool)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type) (a6989586621680378968 :: a ~> Bool) = FindIndicesSym1 a6989586621680378968
type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) (a6989586621680378991 :: a ~> Bool)
Instance details Defined in Data.Singletons.Prelude.List.Internal type Apply (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type) (a6989586621680378991 :: a ~> Bool) = FindIndexSym1 a6989586621680378991
type Apply (FromEnum_6989586621681043892Sym0 :: TyFun (Const a b) Nat -> Type) (a6989586621681043896 :: Const a b)
Instance details Defined in Data.Singletons.Prelude.Const type Apply (FromEnum_6989586621681043892Sym0 :: TyFun (Const a b) Nat -> Type) (a6989586621681043896 :: Const a b) = FromEnum_6989586621681043892Sym1 a6989586621681043896

data Empty #

Replacement for uninhabited type.

Instances

Instances details

Generic Empty
Instance details Defined in Lorentz.Empty Associated Types type Rep Empty :: Type -> Type # Methods from :: Empty -> Rep Empty x # to :: Rep Empty x -> Empty #
HasAnnotation Empty
Instance details Defined in Lorentz.Empty Methods getAnnotation :: FollowEntrypointFlag -> Notes (ToT Empty) # annOptions :: AnnOptions #
IsoValue Empty
Instance details Defined in Lorentz.Empty Associated Types type ToT Empty :: T # Methods toVal :: Empty -> Value (ToT Empty) # fromVal :: Value (ToT Empty) -> Empty #
TypeHasDoc Empty
Instance details Defined in Lorentz.Empty Associated Types type TypeDocFieldDescriptions Empty :: FieldDescriptions # Methods typeDocName :: Proxy Empty -> Text # typeDocMdDescription :: Markdown # typeDocMdReference :: Proxy Empty -> WithinParens -> Markdown # typeDocDependencies :: Proxy Empty -> [SomeDocDefinitionItem] # typeDocHaskellRep :: TypeDocHaskellRep Empty # typeDocMichelsonRep :: TypeDocMichelsonRep Empty #
type Rep Empty
Instance details Defined in Lorentz.Empty type Rep Empty = D1 ('MetaData "Empty" "Lorentz.Empty" "lorentz-0.11.0-inplace" 'True) (C1 ('MetaCons "Empty" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ())))
type ToT Empty
Instance details Defined in Lorentz.Empty type ToT Empty = GValueType (Rep Empty)
type TypeDocFieldDescriptions Empty
Instance details Defined in Lorentz.Empty type TypeDocFieldDescriptions Empty = '[] :: [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]
type AsRPC Empty
Instance details Defined in Morley.Client.RPC.AsRPC type AsRPC Empty = Empty

absurd_ :: forall (s :: [Type]) (s' :: [Type]). (Empty ': s) :-> s' #

Witness of that this code is unreachable.