morley-1.20.0: Developer tools for the Michelson Language
Safe HaskellSafe-Inferred
LanguageHaskell2010

Morley.Michelson.Typed

Synopsis

Documentation

data And Source #

Instances

Instances details
ArithOp And 'TBool 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes And 'TBool 'TBool :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes And 'TBool 'TBool)) Source #

commutativityProof :: Maybe $ Dict (ArithRes And 'TBool 'TBool ~ ArithRes And 'TBool 'TBool, ArithOp And 'TBool 'TBool) Source #

ArithOp And 'TBytes 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes And 'TBytes 'TBytes :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TBytes -> Value' instr 'TBytes -> Either (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes)) (Value' instr (ArithRes And 'TBytes 'TBytes)) Source #

commutativityProof :: Maybe $ Dict (ArithRes And 'TBytes 'TBytes ~ ArithRes And 'TBytes 'TBytes, ArithOp And 'TBytes 'TBytes) Source #

ArithOp And 'TInt 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes And 'TInt 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes And 'TInt 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes And 'TInt 'TNat ~ ArithRes And 'TNat 'TInt, ArithOp And 'TNat 'TInt) Source #

ArithOp And 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes And 'TNat 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy And -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes And 'TNat 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes And 'TNat 'TNat ~ ArithRes And 'TNat 'TNat, ArithOp And 'TNat 'TNat) Source #

type ArithRes And 'TBool 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes And 'TBytes 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes And 'TInt 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes And 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

data T Source #

Michelson language type with annotations stripped off.

Instances

Instances details
Data T Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Methods

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

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

toConstr :: T -> Constr #

dataTypeOf :: T -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic T Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Associated Types

type Rep T :: Type -> Type #

Methods

from :: T -> Rep T x #

to :: Rep T x -> T #

Show T Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Methods

showsPrec :: Int -> T -> ShowS #

show :: T -> String #

showList :: [T] -> ShowS #

NFData T Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Methods

rnf :: T -> () #

Eq T Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Methods

(==) :: T -> T -> Bool #

(/=) :: T -> T -> Bool #

ToExpression T Source # 
Instance details

Defined in Morley.Micheline.Class

RenderDoc T Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Buildable T Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Methods

build :: T -> Doc

buildList :: [T] -> Doc

SingKind T Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Associated Types

type Demote T = (r :: Type) #

Methods

fromSing :: forall (a :: T). Sing a -> Demote T #

toSing :: Demote T -> SomeSing T #

(SDecide T, SDecide Peano) => SDecide T Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

(%~) :: forall (a :: T) (b :: T). Sing a -> Sing b -> Decision (a :~: b) #

(SDecide T, SDecide Peano) => TestCoercion SingT Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

testCoercion :: forall (a :: k) (b :: k). SingT a -> SingT b -> Maybe (Coercion a b) #

(SDecide T, SDecide Peano) => TestEquality SingT Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

testEquality :: forall (a :: k) (b :: k). SingT a -> SingT b -> Maybe (a :~: b) #

FromExp x T Source # 
Instance details

Defined in Morley.Micheline.Class

Methods

fromExp :: Exp x -> Either (FromExpError x) T Source #

SingI 'TAddress Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TAddress #

SingI 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381Fr #

SingI 'TBls12381G1 Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381G1 #

SingI 'TBls12381G2 Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381G2 #

SingI 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBool #

SingI 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBytes #

SingI 'TChainId Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChainId #

SingI 'TChest Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChest #

SingI 'TChestKey Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChestKey #

SingI 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TInt #

SingI 'TKey Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TKey #

SingI 'TKeyHash Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TKeyHash #

SingI 'TMutez Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TMutez #

SingI 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TNat #

SingI 'TNever Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TNever #

SingI 'TOperation Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TOperation #

SingI 'TSignature Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TSignature #

SingI 'TString Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TString #

SingI 'TTimestamp Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TTimestamp #

SingI 'TUnit Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TUnit #

SingI1 'TContract Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TContract x) #

SingI1 'TList Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TList x) #

SingI1 'TOption Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TOption x) #

SingI1 'TSet Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TSet x) #

SingI1 'TTicket Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TTicket x) #

SingI1 'TSaplingState Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TSaplingState x) #

SingI1 'TSaplingTransaction Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TSaplingTransaction x) #

SingI2 'TBigMap Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TBigMap x y) #

SingI2 'TLambda Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TLambda x y) #

SingI2 'TMap Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TMap x y) #

SingI2 'TOr Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TOr x y) #

SingI2 'TPair Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TPair x y) #

SingI n => SingI1 ('TBigMap n :: T -> T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TBigMap n x) #

SingI n => SingI1 ('TLambda n :: T -> T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TLambda n x) #

SingI n => SingI1 ('TMap n :: T -> T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TMap n x) #

SingI n => SingI1 ('TOr n :: T -> T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TOr n x) #

SingI n => SingI1 ('TPair n :: T -> T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TPair n x) #

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

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TContract n) #

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

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TList n) #

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

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TOption n) #

SingI n => SingI ('TSaplingState n :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TSaplingState n) #

SingI n => SingI ('TSaplingTransaction n :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

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

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TSet n) #

SingI n => SingI ('TTicket n :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TTicket n) #

(forall (t :: T). Eq (meta t)) => GEq (StkEl meta :: T -> Type) Source # 
Instance details

Defined in Morley.Michelson.Interpret

Methods

geq :: forall (a :: k) (b :: k). StkEl meta a -> StkEl meta b -> Maybe (a :~: b) #

GEq (Value' instr :: T -> Type) Source # 
Instance details

Defined in Morley.Michelson.Typed.Value

Methods

geq :: forall (a :: k) (b :: k). Value' instr a -> Value' instr b -> Maybe (a :~: b) #

(WhenStuck t (TypeError (ForbidManyTStuckErr c ps' t) :: Constraint), FailWhen a (ForbidTErrorMsg p t)) => DelayedContainsTCheck (c :: Constraint) (ps' :: [TPredicateSym]) (p :: TPredicateSym) (t :: T) a Source # 
Instance details

Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT

(SingI inp, SingI out) => FromExp RegularExp (Instr '[inp] '[out]) Source # 
Instance details

Defined in Morley.Micheline.Class

(SingI n1, SingI n2) => SingI ('TBigMap n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TBigMap n1 n2) #

(SingI n1, SingI n2) => SingI ('TLambda n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TLambda n1 n2) #

(SingI n1, SingI n2) => SingI ('TMap n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TMap n1 n2) #

(SingI n1, SingI n2) => SingI ('TOr n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TOr n1 n2) #

(SingI n1, SingI n2) => SingI ('TPair n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TPair n1 n2) #

(forall (t :: T). cs t => ForbidOp t) => RenderDoc (SomeConstrainedValue cs) Source # 
Instance details

Defined in Morley.Michelson.Typed.Existential

Buildable (MismatchError T) Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Methods

build :: MismatchError T -> Doc

buildList :: [MismatchError T] -> Doc

Buildable (MismatchError [T]) Source # 
Instance details

Defined in Morley.Michelson.Typed.T

Methods

build :: MismatchError [T] -> Doc

buildList :: [MismatchError [T]] -> Doc

Applicative m => StkElMeta (NoStkElMeta :: T -> Type) m Source # 
Instance details

Defined in Morley.Michelson.Interpret

Methods

mkStkElMeta :: forall (t :: T). Maybe (NoStkElMeta t) -> Value t -> m (NoStkElMeta t) Source #

type Rep T Source # 
Instance details

Defined in Morley.Michelson.Typed.T

type Rep T = D1 ('MetaData "T" "Morley.Michelson.Typed.T" "morley-1.20.0-inplace" 'False) (((((C1 ('MetaCons "TKey" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TUnit" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TSignature" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TChainId" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TOption" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T)) :+: C1 ('MetaCons "TList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T))) :+: (C1 ('MetaCons "TSet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T)) :+: C1 ('MetaCons "TOperation" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "TContract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T)) :+: C1 ('MetaCons "TTicket" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T))) :+: (C1 ('MetaCons "TPair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T)) :+: C1 ('MetaCons "TOr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T)))) :+: ((C1 ('MetaCons "TLambda" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T)) :+: C1 ('MetaCons "TMap" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T))) :+: (C1 ('MetaCons "TBigMap" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 T)) :+: C1 ('MetaCons "TInt" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: ((((C1 ('MetaCons "TNat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TString" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TBytes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TMutez" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TBool" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TKeyHash" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TBls12381Fr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TBls12381G1" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "TBls12381G2" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TTimestamp" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TAddress" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TChest" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TChestKey" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TSaplingState" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Peano))) :+: (C1 ('MetaCons "TSaplingTransaction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Peano)) :+: C1 ('MetaCons "TNever" 'PrefixI 'False) (U1 :: Type -> Type))))))
type Demote T Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

type Demote T = T
type Sing Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

type Sing = SingT

data Not Source #

Instances

Instances details
UnaryArithOp Not 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TBool :: T Source #

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TBool -> Value' instr (UnaryArithRes Not 'TBool) Source #

UnaryArithOp Not 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TBytes :: T Source #

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TBytes -> Value' instr (UnaryArithRes Not 'TBytes) Source #

UnaryArithOp Not 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TInt :: T Source #

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TInt -> Value' instr (UnaryArithRes Not 'TInt) Source #

UnaryArithOp Not 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type UnaryArithRes Not 'TNat :: T Source #

Methods

evalUnaryArithOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Not -> Value' instr 'TNat -> Value' instr (UnaryArithRes Not 'TNat) Source #

type UnaryArithRes Not 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type UnaryArithRes Not 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type UnaryArithRes Not 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type UnaryArithRes Not 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

data Xor Source #

Instances

Instances details
ArithOp Xor 'TBool 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Xor 'TBool 'TBool :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Xor -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes Xor 'TBool 'TBool)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Xor 'TBool 'TBool ~ ArithRes Xor 'TBool 'TBool, ArithOp Xor 'TBool 'TBool) Source #

ArithOp Xor 'TBytes 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Xor 'TBytes 'TBytes :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Xor -> Value' instr 'TBytes -> Value' instr 'TBytes -> Either (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes)) (Value' instr (ArithRes Xor 'TBytes 'TBytes)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Xor 'TBytes 'TBytes ~ ArithRes Xor 'TBytes 'TBytes, ArithOp Xor 'TBytes 'TBytes) Source #

ArithOp Xor 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Xor 'TNat 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Xor -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Xor 'TNat 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Xor 'TNat 'TNat ~ ArithRes Xor 'TNat 'TNat, ArithOp Xor 'TNat 'TNat) Source #

type ArithRes Xor 'TBool 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Xor 'TBytes 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Xor 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

class SingI (a :: k) where #

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

Methods

sing :: Sing a #

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

Instances

Instances details
SingI 'MPTConstant Source # 
Instance details

Defined in Morley.Micheline.Expression.Internal.MichelinePrimitive

Methods

sing :: Sing 'MPTConstant #

SingI 'MPTInstr Source # 
Instance details

Defined in Morley.Micheline.Expression.Internal.MichelinePrimitive

Methods

sing :: Sing 'MPTInstr #

SingI 'MPTKeyword Source # 
Instance details

Defined in Morley.Micheline.Expression.Internal.MichelinePrimitive

Methods

sing :: Sing 'MPTKeyword #

SingI 'MPTRemoved Source # 
Instance details

Defined in Morley.Micheline.Expression.Internal.MichelinePrimitive

Methods

sing :: Sing 'MPTRemoved #

SingI 'MPTType Source # 
Instance details

Defined in Morley.Micheline.Expression.Internal.MichelinePrimitive

Methods

sing :: Sing 'MPTType #

SingI 'MPTValue Source # 
Instance details

Defined in Morley.Micheline.Expression.Internal.MichelinePrimitive

Methods

sing :: Sing 'MPTValue #

SingI 'AlwaysFailing Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI 'FailingNormal Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI 'DoesHaveNonStandardAnns Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI 'DoesHaveStandardAnns Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI 'DoesNotHaveAnns Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI 'Additional Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing 'Additional #

SingI 'FromMichelson Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI 'Phantom Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing 'Phantom #

SingI 'Structural Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing 'Structural #

SingI 'HasIndirectChildren Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI 'MayHaveChildren Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI 'NoChildren Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing 'NoChildren #

SingI 'OneChild Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing 'OneChild #

SingI 'TwoChildren Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing 'TwoChildren #

SingI 'PSBigMap Source # 
Instance details

Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT

Methods

sing :: Sing 'PSBigMap #

SingI 'PSContract Source # 
Instance details

Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT

Methods

sing :: Sing 'PSContract #

SingI 'PSNestedBigMaps Source # 
Instance details

Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT

SingI 'PSNonComparable Source # 
Instance details

Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT

SingI 'PSOp Source # 
Instance details

Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT

Methods

sing :: Sing 'PSOp #

SingI 'PSSaplingState Source # 
Instance details

Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT

SingI 'PSTicket Source # 
Instance details

Defined in Morley.Michelson.Typed.Scope.Internal.ForbidT

Methods

sing :: Sing 'PSTicket #

SingI 'TAddress Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TAddress #

SingI 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381Fr #

SingI 'TBls12381G1 Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381G1 #

SingI 'TBls12381G2 Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381G2 #

SingI 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBool #

SingI 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBytes #

SingI 'TChainId Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChainId #

SingI 'TChest Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChest #

SingI 'TChestKey Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChestKey #

SingI 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TInt #

SingI 'TKey Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TKey #

SingI 'TKeyHash Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TKeyHash #

SingI 'TMutez Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TMutez #

SingI 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TNat #

SingI 'TNever Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TNever #

SingI 'TOperation Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TOperation #

SingI 'TSignature Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TSignature #

SingI 'TString Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TString #

SingI 'TTimestamp Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TTimestamp #

SingI 'TUnit Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TUnit #

SingI 'AddressKindContract Source # 
Instance details

Defined in Morley.Tezos.Address.Kinds

SingI 'AddressKindImplicit Source # 
Instance details

Defined in Morley.Tezos.Address.Kinds

SingI 'AddressKindSmartRollup Source # 
Instance details

Defined in Morley.Tezos.Address.Kinds

SingI 'Z Source # 
Instance details

Defined in Morley.Util.Peano

Methods

sing :: Sing 'Z #

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

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TContract n) #

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

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TList n) #

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

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TOption n) #

SingI n => SingI ('TSaplingState n :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TSaplingState n) #

SingI n => SingI ('TSaplingTransaction n :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

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

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TSet n) #

SingI n => SingI ('TTicket n :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TTicket n) #

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

Defined in Morley.Util.Peano

Methods

sing :: Sing ('S n) #

(SingI n1, SingI n2) => SingI ('TBigMap n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TBigMap n1 n2) #

(SingI n1, SingI n2) => SingI ('TLambda n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TLambda n1 n2) #

(SingI n1, SingI n2) => SingI ('TMap n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TMap n1 n2) #

(SingI n1, SingI n2) => SingI ('TOr n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TOr n1 n2) #

(SingI n1, SingI n2) => SingI ('TPair n1 n2 :: T) Source # 
Instance details

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TPair n1 n2) #

(SingI n1, SingI n2, SingI n3, SingI n4) => SingI ('InstrClass n1 n2 n3 n4 :: InstrClass) Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing ('InstrClass n1 n2 n3 n4) #

SingI n => SingI ('MaxInternal n :: MaxInternal a) 
Instance details

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ('MaxInternal n) #

SingI n => SingI ('MinInternal n :: MinInternal a) 
Instance details

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ('MinInternal n) #

SingI GetAllSym0 
Instance details

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetAllSym0 #

SingI GetAnySym0 
Instance details

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetAnySym0 #

SingI ThenCmpSym0 
Instance details

Defined in Data.Ord.Singletons

SingI InstrClassSym0 Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

SingI EfdtNatDnSym0 
Instance details

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EfdtNatDnSym0 #

SingI EfdtNatSym0 
Instance details

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EfdtNatSym0 #

SingI EfdtNatUpSym0 
Instance details

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EfdtNatUpSym0 #

SingI EftNatSym0 
Instance details

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EftNatSym0 #

SingI AllSym0 
Instance details

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing AllSym0 #

SingI All_Sym0 
Instance details

Defined in Data.Semigroup.Singletons.Internal.Disambiguation

Methods

sing :: Sing All_Sym0 #

SingI AnySym0 
Instance details

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing AnySym0 #

SingI Any_Sym0 
Instance details

Defined in Data.Semigroup.Singletons.Internal.Disambiguation

Methods

sing :: Sing Any_Sym0 #

SingI ShowParenSym0 
Instance details

Defined in Text.Show.Singletons

SingI ShowCharSym0 
Instance details

Defined in Text.Show.Singletons

SingI ShowStringSym0 
Instance details

Defined in Text.Show.Singletons

SingI ShowCommaSpaceSym0 
Instance details

Defined in Text.Show.Singletons

SingI ShowSpaceSym0 
Instance details

Defined in Text.Show.Singletons

SingI Show_tupleSym0 
Instance details

Defined in Text.Show.Singletons

Methods

sing :: Sing Show_tupleSym0 #

SingI AndSym0 
Instance details

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing AndSym0 #

SingI OrSym0 
Instance details

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing OrSym0 #

SingI UnlinesSym0 
Instance details

Defined in Data.List.Singletons.Internal

SingI UnwordsSym0 
Instance details

Defined in Data.List.Singletons.Internal

SingI DivSym0 
Instance details

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing DivSym0 #

SingI ModSym0 
Instance details

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing ModSym0 #

SingI (^@#@$) 
Instance details

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

SingI Log2Sym0 
Instance details

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing Log2Sym0 #

SingI NatToCharSym0 
Instance details

Defined in GHC.TypeLits.Singletons

SingI (&&@#@$) 
Instance details

Defined in Data.Bool.Singletons

Methods

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

SingI (||@#@$) 
Instance details

Defined in Data.Bool.Singletons

Methods

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

SingI NotSym0 
Instance details

Defined in Data.Bool.Singletons

Methods

sing :: Sing NotSym0 #

SingI ConsSymbolSym0 
Instance details

Defined in GHC.TypeLits.Singletons

SingI CharToNatSym0 
Instance details

Defined in GHC.TypeLits.Singletons

SingI UnconsSymbolSym0 
Instance details

Defined in GHC.TypeLits.Singletons

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

Defined in Data.Singletons.Base.Instances

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

Defined in Data.Monoid.Singletons

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

Defined in Data.Monoid.Singletons

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

Defined in Data.Ord.Singletons

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

Defined in Data.Semigroup.Singletons.Internal

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

Defined in Data.Semigroup.Singletons.Internal

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetMaxSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetMinSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

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

Defined in Data.Semigroup.Singletons.Internal

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

Defined in Data.Semigroup.Singletons.Internal

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetSumSym0 #

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ThenCmpSym1 d) #

SingI d => SingI (InstrClassSym1 d :: TyFun FailureType (IsMichelson ~> (HasAnns ~> InstrClass)) -> Type) Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing (InstrClassSym1 d) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowParenSym1 d) #

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

Defined in Text.Show.Singletons

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SortBySym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListsortBySym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MaximumBySym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MinimumBySym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NubBySym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListnubBySym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Elem_bySym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Scanl1Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Scanr1Sym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing Listscanr1Sym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Foldl1Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Foldr1Sym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing Listfoldl1Sym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing Listfoldr1Sym0 #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing UntilSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing FindSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing BreakSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SpanSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListpartitionSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListspanSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing AllSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing AnySym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing FilterSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListdropWhileSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListfilterSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListtakeWhileSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SelectSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AppEndoSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing GetMaxInternalSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing GetMinInternalSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

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

Defined in Data.Monoid.Singletons

Methods

sing :: Sing FirstSym0 #

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

Defined in Data.Monoid.Singletons

Methods

sing :: Sing LastSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MaxInternalSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MinInternalSym0 #

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

Defined in Data.Maybe.Singletons

Methods

sing :: Sing IsJustSym0 #

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

Defined in Data.Maybe.Singletons

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

Defined in Data.Maybe.Singletons

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

Defined in Data.Maybe.Singletons

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatDnSym1 d) #

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatSym1 d) #

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatUpSym1 d) #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListsplitAtSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing DropSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing TakeSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListdropSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListtakeSym0 #

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

Defined in Text.Show.Singletons

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EftNatSym1 d) #

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing ToEnumSym0 #

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

Defined in GHC.Num.Singletons

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing UnlessSym0 #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing WhenSym0 #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing GuardSym0 #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowCharSym1 d) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowStringSym1 d) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (Show_tupleSym1 d) #

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

Defined in Data.Maybe.Singletons

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListtransposeSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ConcatSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

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

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListindexSym0 #

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

Defined in Text.Show.Singletons

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListisPrefixOfSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing UnionSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

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

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

Defined in GHC.Base.Singletons

Methods

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

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

Defined in Data.Maybe.Singletons

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing LengthSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListlengthSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NullSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListnullSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing GroupSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing InitsSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NonEmptySubsequencesSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing TailsSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListinitsSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListtailsSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing InitSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NubSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SortSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing TailSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListinitSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListreverseSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListsortSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing HeadSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing LastSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MaximumSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MinimumSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ProductSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SumSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListlastSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListmaximumSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListminimumSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListproductSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListsumSym0 #

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

Defined in Data.Monoid.Singletons

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

Defined in Data.Singletons.Base.Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing DownSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing FirstSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing LastSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing MaxSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing MinSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing DualSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

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

Defined in Data.Semigroup.Singletons.Internal.Disambiguation

Methods

sing :: Sing Product_Sym0 #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing SumSym0 #

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

Defined in Data.Semigroup.Singletons.Internal.Disambiguation

Methods

sing :: Sing Sum_Sym0 #

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

Defined in Data.Maybe.Singletons

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

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowsSym0 #

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

Defined in Data.Singletons.Base.Instances

Methods

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

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ElemSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NotElemSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListelemSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing DeleteSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing InsertSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing PrependToAllSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListinsertSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListintersperseSym0 #

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

Defined in Data.Singletons.Base.Instances

Methods

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

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

Defined in Data.Ord.Singletons

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

Defined in Data.Bool.Singletons

Methods

sing :: Sing Bool_Sym0 #

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

Defined in Data.Singletons.Base.Enum

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Singletons.Base.Enum

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

Defined in Data.Monoid.Singletons

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing MaxSym0 #

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing MinSym0 #

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

Defined in Data.Ord.Singletons.Disambiguation

Methods

sing :: Sing Max_Sym0 #

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

Defined in Data.Ord.Singletons.Disambiguation

Methods

sing :: Sing Min_Sym0 #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

Defined in GHC.Base.Singletons

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

Defined in GHC.Num.Singletons

Methods

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

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

Defined in GHC.Num.Singletons

Methods

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

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

Defined in GHC.Num.Singletons

Methods

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

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

Defined in GHC.Num.Singletons

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing JustSym0 #

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

Defined in Data.Singletons.Base.Enum

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

Defined in Text.Show.Singletons

Methods

sing :: Sing Show_Sym0 #

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing PredSym0 #

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing SuccSym0 #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing IdSym0 #

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

Defined in GHC.Num.Singletons

Methods

sing :: Sing AbsSym0 #

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

Defined in GHC.Num.Singletons

Methods

sing :: Sing NegateSym0 #

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

Defined in GHC.Num.Singletons

Methods

sing :: Sing SignumSym0 #

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

Defined in Data.Semigroup.Singletons.Internal

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AndSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing OrSym0 #

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

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

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

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing (DivSym1 x) #

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

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing (ModSym1 x) #

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

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

SingI (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type) 
Instance details

Defined in Data.Bool.Singletons

Methods

sing :: Sing IfSym0 #

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

Defined in Data.Bool.Singletons

Methods

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

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

Defined in Data.Bool.Singletons

Methods

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

SingI x => SingI (ConsSymbolSym1 x :: TyFun Symbol Symbol -> Type) 
Instance details

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing (ConsSymbolSym1 x) #

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

Defined in Data.Either.Singletons

Methods

sing :: Sing IsLeftSym0 #

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

Defined in Data.Either.Singletons

(SingI d1, SingI d2) => SingI (InstrClassSym2 d1 d2 :: TyFun IsMichelson (HasAnns ~> InstrClass) -> Type) Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing (InstrClassSym2 d1 d2) #

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Foldl1Sym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Foldr1Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ScanrSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListscanrSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListfoldrSym0 #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing FoldrSym0 #

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

Defined in Data.Maybe.Singletons

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

Defined in Control.Monad.Singletons

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FindSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AllSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AnySym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ConcatMapSym0 #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (UntilSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListmapSym0 #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing MapSym0 #

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

Defined in GHC.Base.Singletons

Methods

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

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

Defined in GHC.Base.Singletons

Methods

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

SApplicative m => SingI (FilterMSym0 :: TyFun (a ~> m Bool) ([a] ~> m [a]) -> Type) 
Instance details

Defined in Control.Monad.Singletons

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ScanlSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListscanlSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Foldl'Sym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing Listfoldl'Sym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListfoldlSym0 #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing FoldlSym0 #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.Ord.Singletons

SingI (RunStateLSym0 :: TyFun (StateL s a) (s ~> (s, a)) -> Type) 
Instance details

Defined in Data.Traversable.Singletons

Methods

sing :: Sing RunStateLSym0 #

SingI (RunStateRSym0 :: TyFun (StateR s a) (s ~> (s, a)) -> Type) 
Instance details

Defined in Data.Traversable.Singletons

Methods

sing :: Sing RunStateRSym0 #

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

Defined in Data.Maybe.Singletons

Methods

sing :: Sing (FromMaybeSym1 d) #

SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Natural (m a ~> m ()) -> Type) 
Instance details

Defined in Control.Monad.Singletons

SApplicative m => SingI (ReplicateMSym0 :: TyFun Natural (m a ~> m [a]) -> Type) 
Instance details

Defined in Control.Monad.Singletons

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatDnSym2 d1 d2) #

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatSym2 d1 d2) #

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatUpSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

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

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListindexSym1 d) #

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

Defined in Data.Tuple.Singletons

Methods

sing :: Sing SwapSym0 #

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

Defined in Data.Tuple.Singletons

Methods

sing :: Sing FstSym0 #

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

Defined in Data.Tuple.Singletons

Methods

sing :: Sing SndSym0 #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowListSym1 d) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowParenSym2 d1 d2) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowsSym1 d) #

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

Defined in GHC.TypeLits.Singletons.Internal

Methods

sing :: Sing ErrorSym0 #

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

Defined in GHC.TypeLits.Singletons.Internal

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

Defined in Data.Either.Singletons

Methods

sing :: Sing PartitionEithersSym0 #

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

Defined in Data.Either.Singletons

Methods

sing :: Sing LeftsSym0 #

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

Defined in Data.Either.Singletons

Methods

sing :: Sing RightsSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing UnzipSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListunzipSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntercalateSym1 d) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowListWithSym1 d) #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntersectBySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (UnionBySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ZipSym0 #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListzipSym0 #

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

Defined in Data.Singletons.Base.Instances

Methods

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

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ElemIndexSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (FindIndexSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (FindSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (BreakSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (PartitionSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SpanSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SplitAtSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListpartitionSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListspanSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListsplitAtSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (AllSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (AnySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ElemSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IsInfixOfSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IsPrefixOfSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IsSuffixOfSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (NotElemSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListelemSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListisPrefixOfSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ElemIndicesSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (FindIndicesSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (GroupBySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DropSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DropWhileEndSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DropWhileSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (FilterSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (InsertSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntersectSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntersperseSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (NubBySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (PrependToAllSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Scanl1Sym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Scanr1Sym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SortBySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (TakeSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (TakeWhileSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (UnionSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

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

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListdropSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListdropWhileSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfilterSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListinsertSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListintersperseSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListnubBySym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listscanr1Sym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListsortBySym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListtakeSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListtakeWhileSym1 d) #

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

Defined in Data.Singletons.Base.Instances

Methods

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

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

Defined in GHC.Base.Singletons

Methods

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

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldl1'Sym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldl1Sym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldr1Sym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MaximumBySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MinimumBySym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl1Sym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listfoldr1Sym1 d) #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing LeftSym0 #

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (CompareSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SelectSym1 d) #

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

Defined in Data.Bool.Singletons

Methods

sing :: Sing (Bool_Sym1 d) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowsPrecSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing LookupSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Elem_bySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteBySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (InsertBySym1 d) #

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

Defined in Data.Singletons.Base.Enum

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

Defined in Data.Semigroup.Singletons

Methods

sing :: Sing ArgSym0 #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple2Sym0 #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing ConstSym0 #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing SeqSym0 #

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

Defined in Data.Proxy.Singletons

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ElemSym0 #

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ReplicateSym1 d) #

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EnumFromToSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (AppEndoSym1 d) #

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

Defined in Data.Monoid.Singletons

Methods

sing :: Sing (MappendSym1 d) #

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (MaxSym1 d) #

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (MinSym1 d) #

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

Defined in Data.Ord.Singletons.Disambiguation

Methods

sing :: Sing (Max_Sym1 d) #

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

Defined in Data.Ord.Singletons.Disambiguation

Methods

sing :: Sing (Min_Sym1 d) #

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

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (AsTypeOfSym1 d) #

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

Defined in GHC.Num.Singletons

Methods

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

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

Defined in GHC.Num.Singletons

Methods

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

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

Defined in GHC.Num.Singletons

Methods

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

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

Defined in GHC.Num.Singletons

Methods

sing :: Sing (SubtractSym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing PureSym0 #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ReturnSym0 #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing RightSym0 #

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

Defined in Data.Maybe.Singletons

Methods

sing :: Sing Maybe_Sym0 #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (UnlessSym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (WhenSym1 d) #

SAlternative f => SingI (OptionalSym0 :: TyFun (f a) (f (Maybe a)) -> Type) 
Instance details

Defined in Control.Applicative.Singletons

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

Defined in Data.Functor.Singletons

Methods

sing :: Sing VoidSym0 #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing JoinSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ConcatSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ToListSym0 #

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing SumSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldSym0 #

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

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

SingI c => SingI (IfSym1 c :: TyFun k (k ~> k) -> Type) 
Instance details

Defined in Data.Bool.Singletons

Methods

sing :: Sing (IfSym1 c) #

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

Defined in Data.Singletons

Methods

sing :: Sing ('WrapSing s) #

SingI (GetConstSym0 :: TyFun (Const a b) a -> Type) 
Instance details

Defined in Data.Functor.Const.Singletons

(SingI d1, SingI d2, SingI d3) => SingI (InstrClassSym3 d1 d2 d3 :: TyFun HasAnns InstrClass -> Type) Source # 
Instance details

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

Methods

sing :: Sing (InstrClassSym3 d1 d2 d3) #

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

Defined in Data.Tuple.Singletons

Methods

sing :: Sing CurrySym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Foldr'Sym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldrSym0 #

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

Defined in Data.Tuple.Singletons

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListzipWithSym0 #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing FlipSym0 #

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Maybe.Singletons

Methods

sing :: Sing (Maybe_Sym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing FmapSym0 #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftASym0 #

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

Defined in Data.Functor.Singletons

Methods

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

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

Defined in Control.Monad.Singletons

Methods

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

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

Defined in Data.Traversable.Singletons

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

Defined in Data.Either.Singletons

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Traversable.Singletons

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftMSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MapAccumLSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MapAccumRSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Foldl'Sym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldlSym0 #

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

Defined in GHC.Base.Singletons

Methods

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

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SelectSym2 d1 d2) #

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

Defined in Data.Bool.Singletons

Methods

sing :: Sing (Bool_Sym2 d1 d2) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowListWithSym2 d1 d2) #

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

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowsPrecSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (LookupSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip3Sym0 #

SMonadFail m => SingI (FailSym0 :: TyFun [Char] (m a) -> Type) 
Instance details

Defined in Control.Monad.Fail.Singletons

Methods

sing :: Sing FailSym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Zip3Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Elem_bySym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteBySym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteFirstsBySym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (InsertBySym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntersectBySym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (UnionBySym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ConcatMapSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListmapSym1 d) #

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

Defined in Data.Maybe.Singletons

Methods

sing :: Sing (MapMaybeSym1 d) #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (MapSym1 d) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FilterMSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListzipSym1 d) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple3Sym0 #

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EnumFromThenToSym2 d1 d2) #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (UntilSym2 d1 d2) #

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

Defined in GHC.Base.Singletons

Methods

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

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

Defined in GHC.Base.Singletons

Methods

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

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

Defined in Data.Semigroup.Singletons

Methods

sing :: Sing (ArgSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ScanlSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ScanrSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListscanlSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListscanrSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldl'Sym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl'Sym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfoldlSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfoldrSym1 d) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (FoldlSym1 d) #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (FoldrSym1 d) #

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ComparingSym1 d) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple2Sym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (UnfoldrSym1 d) #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (ConstSym1 d) #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (SeqSym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Data.Functor.Singletons

Methods

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

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

Defined in Data.Functor.Singletons

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ApSym0 #

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing MplusSym0 #

(SApplicative m, SingI d) => SingI (ReplicateM_Sym1 d :: TyFun (m a) (m ()) -> Type) 
Instance details

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ReplicateM_Sym1 d) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ReplicateMSym1 d) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (MfilterSym1 d) #

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

Defined in Data.Proxy.Singletons

SingI d => SingI (RunStateLSym1 d :: TyFun s (s, a) -> Type) 
Instance details

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (RunStateLSym1 d) #

SingI d => SingI (RunStateRSym1 d :: TyFun s (s, a) -> Type) 
Instance details

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (RunStateRSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FindSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing LengthSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (AllSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (AnySym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (ElemSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (NotElemSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing NullSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldl1Sym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldr1Sym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (MaximumBySym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (MinimumBySym1 d) #

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Traversable.Singletons

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Traversable.Singletons

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

Defined in Data.Functor.Const.Singletons

Methods

sing :: Sing ConstSym0 #

(SingI c, SingI t) => SingI (IfSym2 c t :: TyFun k k -> Type) 
Instance details

Defined in Data.Bool.Singletons

Methods

sing :: Sing (IfSym2 c t) #

(forall (a :: k1). SingI a => SingI (f a), (ApplyTyCon :: (k1 -> kr) -> TyFun k1 kr -> Type) ~ (ApplyTyConAux1 :: (k1 -> kr) -> TyFun k1 kr -> Type)) => SingI (TyCon1 f :: TyFun k1 kr -> Type) 
Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon1 f) #

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

Defined in Data.List.Singletons.Internal

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

Defined in Data.Traversable.Singletons

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

Defined in Data.Traversable.Singletons

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftA2Sym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldrMSym0 #

SApplicative m => SingI (ZipWithM_Sym0 :: TyFun (a ~> (b ~> m c)) ([a] ~> ([b] ~> m ())) -> Type) 
Instance details

Defined in Control.Monad.Singletons

SApplicative m => SingI (ZipWithMSym0 :: TyFun (a ~> (b ~> m c)) ([a] ~> ([b] ~> m [c])) -> Type) 
Instance details

Defined in Control.Monad.Singletons

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

Defined in GHC.Base.Singletons

Methods

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

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

Defined in Data.Functor.Singletons

Methods

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

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

Defined in Data.Foldable.Singletons

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

Defined in Data.Traversable.Singletons

SApplicative m => SingI (MapAndUnzipMSym0 :: TyFun (a ~> m (b, c)) ([a] ~> m ([b], [c])) -> Type) 
Instance details

Defined in Control.Monad.Singletons

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

Defined in Control.Monad.Singletons

Methods

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

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MapM_Sym0 #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing MapMSym0 #

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftM2Sym0 #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing FoldM_Sym0 #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing FoldMSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldlMSym0 #

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

Defined in Data.Either.Singletons

Methods

sing :: Sing (Either_Sym1 d) #

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

Defined in Control.Monad.Singletons

Methods

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

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

Defined in Data.Maybe.Singletons

Methods

sing :: Sing (Maybe_Sym2 d1 d2) #

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

Defined in Data.Tuple.Singletons

Methods

sing :: Sing (UncurrySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip4Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWithSym1 d) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListzipWithSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ScanlSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ScanrSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListscanlSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListscanrSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

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

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

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

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfoldlSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfoldrSym2 d1 d2) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (FoldlSym2 d1 d2) #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (FoldrSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Zip3Sym1 d) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple4Sym0 #

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

Defined in Data.Tuple.Singletons

Methods

sing :: Sing (CurrySym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MapAccumLSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MapAccumRSym1 d) #

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ComparingSym2 d1 d2) #

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (FlipSym1 d) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple3Sym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldl'Sym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldlSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldr'Sym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldrSym1 d) #

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

Defined in Data.Functor.Singletons

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (FmapSym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftASym1 d) #

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

Defined in Data.Functor.Singletons

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (MplusSym1 d) #

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

Defined in Control.Monad.Singletons

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (ApSym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftMSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing For_Sym0 #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing ForSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ForM_Sym0 #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing ForMSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (ConcatMapSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldMapSym1 d) #

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

Defined in Data.Traversable.Singletons

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (FmapDefaultSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AsumSym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MsumSym0 #

(forall (a :: k1) (b :: k2). (SingI a, SingI b) => SingI (f a b), (ApplyTyCon :: (k2 -> kr) -> TyFun k2 kr -> Type) ~ (ApplyTyConAux1 :: (k2 -> kr) -> TyFun k2 kr -> Type)) => SingI (TyCon2 f :: TyFun k1 (k2 ~> kr) -> Type) 
Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon2 f) #

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

Defined in Data.Either.Singletons

Methods

sing :: Sing (Either_Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftA3Sym0 #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (For_Sym1 d) #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (ForSym1 d) #

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

Defined in Control.Monad.Singletons

Methods

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

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (ForM_Sym1 d) #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (ForMSym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftM3Sym0 #

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

Defined in Control.Monad.Singletons

Methods

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

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip5Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWith3Sym1 d2) #

(SApplicative m, SingI d) => SingI (ZipWithM_Sym1 d :: TyFun [a] ([b] ~> m ()) -> Type) 
Instance details

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ZipWithM_Sym1 d) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ZipWithMSym1 d) #

(SApplicative m, SingI d) => SingI (MapAndUnzipMSym1 d :: TyFun [a] (m ([b], [c])) -> Type) 
Instance details

Defined in Control.Monad.Singletons

Methods

sing :: Sing (MapAndUnzipMSym1 d) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWithSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListzipWithSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Zip3Sym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MapAccumLSym2 d1 d2) #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MapAccumRSym2 d1 d2) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple5Sym0 #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapAccumLSym1 d) #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapAccumRSym1 d) #

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

Defined in GHC.Base.Singletons

Methods

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

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

Defined in GHC.Base.Singletons

Methods

sing :: Sing (FlipSym2 d1 d2) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple4Sym1 d1) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FoldM_Sym1 d) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FoldMSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldlMSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldrMSym1 d) #

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

Defined in Data.Tuple.Singletons

Methods

sing :: Sing (CurrySym2 d1 d2) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple3Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA2Sym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM2Sym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Data.Foldable.Singletons

Methods

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

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldlSym2 d1 d2) #

(SFoldable t, SingI d1, SingI d2) => SingI (Foldr'Sym2 d1 d2 :: TyFun (t a) b -> Type) 
Instance details

Defined in Data.Foldable.Singletons

Methods

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

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldrSym2 d1 d2) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Traverse_Sym1 d) #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (TraverseSym1 d) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (MapM_Sym1 d) #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapMSym1 d) #

(forall (a :: k1) (b :: k2) (c :: k3). (SingI a, SingI b, SingI c) => SingI (f a b c), (ApplyTyCon :: (k3 -> kr) -> TyFun k3 kr -> Type) ~ (ApplyTyConAux1 :: (k3 -> kr) -> TyFun k3 kr -> Type)) => SingI (TyCon3 f :: TyFun k1 (k2 ~> (k3 ~> kr)) -> Type) 
Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon3 f) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftM4Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip6Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWith3Sym2 d2 d3) #

(SApplicative m, SingI d1, SingI d2) => SingI (ZipWithM_Sym2 d1 d2 :: TyFun [b] (m ()) -> Type) 
Instance details

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ZipWithM_Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ZipWithMSym2 d1 d2) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple6Sym0 #

(SMonad m, SingI d1, SingI d2) => SingI (d1 <=<@#@$$$ d2 :: TyFun a (m c) -> Type) 
Instance details

Defined in Control.Monad.Singletons

Methods

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

(SMonad m, SingI d1, SingI d2) => SingI (d1 >=>@#@$$$ d2 :: TyFun a (m c) -> Type) 
Instance details

Defined in Control.Monad.Singletons

Methods

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

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple5Sym1 d1) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple4Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA3Sym1 d2) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA2Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM3Sym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM2Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FoldM_Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FoldMSym2 d1 d2) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldlMSym2 d1 d2) #

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

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldrMSym2 d1 d2) #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapAccumLSym2 d1 d2) #

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

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapAccumRSym2 d1 d2) #

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d), (ApplyTyCon :: (k4 -> kr) -> TyFun k4 kr -> Type) ~ (ApplyTyConAux1 :: (k4 -> kr) -> TyFun k4 kr -> Type)) => SingI (TyCon4 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> kr))) -> Type) 
Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon4 f) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftM5Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip7Sym0 #

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

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWith3Sym3 d2 d3 d4) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple7Sym0 #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym1 d1) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple5Sym2 d1 d2) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple4Sym3 d1 d2 d3) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA3Sym2 d2 d3) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM4Sym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM3Sym2 d1 d2) #

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (SingI a, SingI b, SingI c, SingI d, SingI e) => SingI (f a b c d e), (ApplyTyCon :: (k5 -> kr) -> TyFun k5 kr -> Type) ~ (ApplyTyConAux1 :: (k5 -> kr) -> TyFun k5 kr -> Type)) => SingI (TyCon5 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> kr)))) -> Type) 
Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon5 f) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym1 d1) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym2 d1 d2) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple5Sym3 d1 d2 d3) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA3Sym3 d2 d3 d4) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM5Sym1 d) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM4Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM3Sym3 d1 d2 d3) #

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f') => SingI (f a b c d e f'), (ApplyTyCon :: (k6 -> kr) -> TyFun k6 kr -> Type) ~ (ApplyTyConAux1 :: (k6 -> kr) -> TyFun k6 kr -> Type)) => SingI (TyCon6 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> kr))))) -> Type) 
Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon6 f) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym2 d1 d2) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym3 d1 d2 d3) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple5Sym4 d1 d2 d3 d5) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM5Sym2 d1 d2) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM4Sym3 d1 d2 d3) #

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g) => SingI (f a b c d e f' g), (ApplyTyCon :: (k7 -> kr) -> TyFun k7 kr -> Type) ~ (ApplyTyConAux1 :: (k7 -> kr) -> TyFun k7 kr -> Type)) => SingI (TyCon7 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> kr)))))) -> Type) 
Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon7 f) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym3 d1 d2 d3) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym4 d1 d2 d3 d5) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM5Sym3 d1 d2 d3) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM4Sym4 d1 d2 d3 d4) #

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h) => SingI (f a b c d e f' g h), (ApplyTyCon :: (k8 -> kr) -> TyFun k8 kr -> Type) ~ (ApplyTyConAux1 :: (k8 -> kr) -> TyFun k8 kr -> Type)) => SingI (TyCon8 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> kr))))))) -> Type) 
Instance details

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym4 d1 d2 d3 d5) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym5 d1 d2 d3 d5 d6) #

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM5Sym4 d1 d2 d3 d4) #

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym5 d1 d2 d3 d5 d6) #

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

Defined in Control.Monad.Singletons.Internal

Methods

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

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

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym6 d1 d2 d3 d5 d6 d7) #

newtype a :- b infixr 9 #

This is the type of entailment.

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

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

e.g.

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

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

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

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

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

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

What are the two ways?

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

Diagrammatically,

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

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

Constructors

Sub (a => Dict b) 

Instances

Instances details
Category (:-)

Possible since GHC 7.8, when Category was made polykinded.

Instance details

Defined in Data.Constraint

Methods

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

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Show (a :- b) 
Instance details

Defined in Data.Constraint

Methods

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

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

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

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

Defined in Data.Constraint

Methods

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

Eq (a :- b)

Assumes IncoherentInstances doesn't exist.

Instance details

Defined in Data.Constraint

Methods

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

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

Ord (a :- b)

Assumes IncoherentInstances doesn't exist.

Instance details

Defined in Data.Constraint

Methods

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

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

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

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

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

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

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

data Sub Source #

Instances

Instances details
ArithOp Sub 'TInt 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TInt 'TInt :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TInt 'TInt)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TInt 'TInt ~ ArithRes Sub 'TInt 'TInt, ArithOp Sub 'TInt 'TInt) Source #

ArithOp Sub 'TInt 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TInt 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Sub 'TInt 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TInt 'TNat ~ ArithRes Sub 'TNat 'TInt, ArithOp Sub 'TNat 'TInt) Source #

ArithOp Sub 'TNat 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TNat 'TInt :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TNat 'TInt)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TNat 'TInt ~ ArithRes Sub 'TInt 'TNat, ArithOp Sub 'TInt 'TNat) Source #

ArithOp Sub 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TNat 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Sub 'TNat 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TNat 'TNat ~ ArithRes Sub 'TNat 'TNat, ArithOp Sub 'TNat 'TNat) Source #

ArithOp Sub 'TTimestamp 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TTimestamp 'TInt :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Sub -> Value' instr 'TTimestamp -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt)) (Value' instr (ArithRes Sub 'TTimestamp 'TInt)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Sub 'TTimestamp 'TInt ~ ArithRes Sub 'TInt 'TTimestamp, ArithOp Sub 'TInt 'TTimestamp) Source #

ArithOp Sub 'TTimestamp 'TTimestamp Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Sub 'TTimestamp 'TTimestamp :: T Source #

type ArithRes Sub 'TInt 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Sub 'TInt 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Sub 'TNat 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Sub 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Sub 'TTimestamp 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Sub 'TTimestamp 'TTimestamp Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

data Dict a where #

Values of type Dict p capture a dictionary for a constraint of type p.

e.g.

Dict :: Dict (Eq Int)

captures a dictionary that proves we have an:

instance Eq Int

Pattern matching on the Dict constructor will bring this instance into scope.

Constructors

Dict :: forall a. a => Dict a 

Instances

Instances details
() :=> (Semigroup (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Semigroup (Dict a) #

() :=> (Show (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

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

() :=> (Eq (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

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

() :=> (Ord (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

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

a :=> (Monoid (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Monoid (Dict a) #

a :=> (Bounded (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Bounded (Dict a) #

a :=> (Enum (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Enum (Dict a) #

a :=> (Read (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Read (Dict a) #

HasDict a (Dict a) 
Instance details

Defined in Data.Constraint

Methods

evidence :: Dict a -> Dict a #

(Typeable p, p) => Data (Dict p) 
Instance details

Defined in Data.Constraint

Methods

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

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

toConstr :: Dict p -> Constr #

dataTypeOf :: Dict p -> DataType #

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

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

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

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

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

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

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

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

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

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

a => Monoid (Dict a) 
Instance details

Defined in Data.Constraint

Methods

mempty :: Dict a #

mappend :: Dict a -> Dict a -> Dict a #

mconcat :: [Dict a] -> Dict a #

Semigroup (Dict a) 
Instance details

Defined in Data.Constraint

Methods

(<>) :: Dict a -> Dict a -> Dict a #

sconcat :: NonEmpty (Dict a) -> Dict a #

stimes :: Integral b => b -> Dict a -> Dict a #

a => Bounded (Dict a) 
Instance details

Defined in Data.Constraint

Methods

minBound :: Dict a #

maxBound :: Dict a #

a => Enum (Dict a) 
Instance details

Defined in Data.Constraint

Methods

succ :: Dict a -> Dict a #

pred :: Dict a -> Dict a #

toEnum :: Int -> Dict a #

fromEnum :: Dict a -> Int #

enumFrom :: Dict a -> [Dict a] #

enumFromThen :: Dict a -> Dict a -> [Dict a] #

enumFromTo :: Dict a -> Dict a -> [Dict a] #

enumFromThenTo :: Dict a -> Dict a -> Dict a -> [Dict a] #

a => Read (Dict a) 
Instance details

Defined in Data.Constraint

Show (Dict a) 
Instance details

Defined in Data.Constraint

Methods

showsPrec :: Int -> Dict a -> ShowS #

show :: Dict a -> String #

showList :: [Dict a] -> ShowS #

NFData (Dict c) 
Instance details

Defined in Data.Constraint

Methods

rnf :: Dict c -> () #

Eq (Dict a) 
Instance details

Defined in Data.Constraint

Methods

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

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

Ord (Dict a) 
Instance details

Defined in Data.Constraint

Methods

compare :: Dict a -> Dict a -> Ordering #

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

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

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

(>=) :: Dict a -> Dict a -> Bool #

max :: Dict a -> Dict a -> Dict a #

min :: Dict a -> Dict a -> Dict a #

data Or Source #

Instances

Instances details
ArithOp Or 'TBool 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Or 'TBool 'TBool :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Or -> Value' instr 'TBool -> Value' instr 'TBool -> Either (ArithError (Value' instr 'TBool) (Value' instr 'TBool)) (Value' instr (ArithRes Or 'TBool 'TBool)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Or 'TBool 'TBool ~ ArithRes Or 'TBool 'TBool, ArithOp Or 'TBool 'TBool) Source #

ArithOp Or 'TBytes 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Or 'TBytes 'TBytes :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Or -> Value' instr 'TBytes -> Value' instr 'TBytes -> Either (ArithError (Value' instr 'TBytes) (Value' instr 'TBytes)) (Value' instr (ArithRes Or 'TBytes 'TBytes)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Or 'TBytes 'TBytes ~ ArithRes Or 'TBytes 'TBytes, ArithOp Or 'TBytes 'TBytes) Source #

ArithOp Or 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Or 'TNat 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Or -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Or 'TNat 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Or 'TNat 'TNat ~ ArithRes Or 'TNat 'TNat, ArithOp Or 'TNat 'TNat) Source #

type ArithRes Or 'TBool 'TBool Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Or 'TBytes 'TBytes Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Or 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

data Mul Source #

Instances

Instances details
ArithOp Mul 'TBls12381Fr 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TBls12381Fr 'TBls12381Fr :: T Source #

(Bottom, Bls12381MulBadOrder Bls12381Fr Bls12381G1 :: Constraint) => ArithOp Mul 'TBls12381Fr 'TBls12381G1 Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TBls12381Fr 'TBls12381G1 :: T Source #

(Bottom, Bls12381MulBadOrder Bls12381Fr Bls12381G2 :: Constraint) => ArithOp Mul 'TBls12381Fr 'TBls12381G2 Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TBls12381Fr 'TBls12381G2 :: T Source #

ArithOp Mul 'TBls12381Fr 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TBls12381Fr 'TInt :: T Source #

ArithOp Mul 'TBls12381Fr 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TBls12381Fr 'TNat :: T Source #

ArithOp Mul 'TBls12381G1 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TBls12381G1 'TBls12381Fr :: T Source #

ArithOp Mul 'TBls12381G2 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TBls12381G2 'TBls12381Fr :: T Source #

ArithOp Mul 'TInt 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TInt 'TBls12381Fr :: T Source #

ArithOp Mul 'TInt 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TInt 'TInt :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Mul 'TInt 'TInt)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TInt 'TInt ~ ArithRes Mul 'TInt 'TInt, ArithOp Mul 'TInt 'TInt) Source #

ArithOp Mul 'TInt 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TInt 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TInt 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TInt 'TNat ~ ArithRes Mul 'TNat 'TInt, ArithOp Mul 'TNat 'TInt) Source #

ArithOp Mul 'TMutez 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TMutez 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TMutez -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TMutez 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TMutez 'TNat ~ ArithRes Mul 'TNat 'TMutez, ArithOp Mul 'TNat 'TMutez) Source #

ArithOp Mul 'TNat 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TBls12381Fr :: T Source #

ArithOp Mul 'TNat 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TInt :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Mul 'TNat 'TInt)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TInt ~ ArithRes Mul 'TInt 'TNat, ArithOp Mul 'TInt 'TNat) Source #

ArithOp Mul 'TNat 'TMutez Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TMutez :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TMutez)) (Value' instr (ArithRes Mul 'TNat 'TMutez)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TMutez ~ ArithRes Mul 'TMutez 'TNat, ArithOp Mul 'TMutez 'TNat) Source #

ArithOp Mul 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Mul 'TNat 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Mul -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Mul 'TNat 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Mul 'TNat 'TNat ~ ArithRes Mul 'TNat 'TNat, ArithOp Mul 'TNat 'TNat) Source #

type ArithRes Mul 'TBls12381Fr 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TBls12381Fr 'TBls12381G1 Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TBls12381Fr 'TBls12381G2 Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TBls12381Fr 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TBls12381Fr 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TBls12381G1 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TBls12381G2 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TInt 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TInt 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TInt 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TMutez 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TNat 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TNat 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TNat 'TMutez Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Mul 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

data Add Source #

Instances

Instances details
ArithOp Add 'TBls12381Fr 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TBls12381Fr 'TBls12381Fr :: T Source #

ArithOp Add 'TBls12381G1 'TBls12381G1 Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TBls12381G1 'TBls12381G1 :: T Source #

ArithOp Add 'TBls12381G2 'TBls12381G2 Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TBls12381G2 'TBls12381G2 :: T Source #

ArithOp Add 'TInt 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TInt :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TInt 'TInt)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TInt ~ ArithRes Add 'TInt 'TInt, ArithOp Add 'TInt 'TInt) Source #

ArithOp Add 'TInt 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TNat)) (Value' instr (ArithRes Add 'TInt 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TNat ~ ArithRes Add 'TNat 'TInt, ArithOp Add 'TNat 'TInt) Source #

ArithOp Add 'TInt 'TTimestamp Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TInt 'TTimestamp :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TInt -> Value' instr 'TTimestamp -> Either (ArithError (Value' instr 'TInt) (Value' instr 'TTimestamp)) (Value' instr (ArithRes Add 'TInt 'TTimestamp)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Add 'TInt 'TTimestamp ~ ArithRes Add 'TTimestamp 'TInt, ArithOp Add 'TTimestamp 'TInt) Source #

ArithOp Add 'TMutez 'TMutez Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TMutez 'TMutez :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TMutez -> Value' instr 'TMutez -> Either (ArithError (Value' instr 'TMutez) (Value' instr 'TMutez)) (Value' instr (ArithRes Add 'TMutez 'TMutez)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Add 'TMutez 'TMutez ~ ArithRes Add 'TMutez 'TMutez, ArithOp Add 'TMutez 'TMutez) Source #

ArithOp Add 'TNat 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TNat 'TInt :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TNat -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TNat 'TInt)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Add 'TNat 'TInt ~ ArithRes Add 'TInt 'TNat, ArithOp Add 'TInt 'TNat) Source #

ArithOp Add 'TNat 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TNat 'TNat :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TNat -> Value' instr 'TNat -> Either (ArithError (Value' instr 'TNat) (Value' instr 'TNat)) (Value' instr (ArithRes Add 'TNat 'TNat)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Add 'TNat 'TNat ~ ArithRes Add 'TNat 'TNat, ArithOp Add 'TNat 'TNat) Source #

ArithOp Add 'TTimestamp 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

Associated Types

type ArithRes Add 'TTimestamp 'TInt :: T Source #

Methods

evalOp :: forall proxy (instr :: [T] -> [T] -> Type). proxy Add -> Value' instr 'TTimestamp -> Value' instr 'TInt -> Either (ArithError (Value' instr 'TTimestamp) (Value' instr 'TInt)) (Value' instr (ArithRes Add 'TTimestamp 'TInt)) Source #

commutativityProof :: Maybe $ Dict (ArithRes Add 'TTimestamp 'TInt ~ ArithRes Add 'TInt 'TTimestamp, ArithOp Add 'TInt 'TTimestamp) Source #

type ArithRes Add 'TBls12381Fr 'TBls12381Fr Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Add 'TBls12381G1 'TBls12381G1 Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Add 'TBls12381G2 'TBls12381G2 Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Add 'TInt 'TInt Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes Add 'TInt 'TNat Source # 
Instance details

Defined in Morley.Michelson.Typed.Arith

type ArithRes