Safe Haskell | None |
---|---|
Language | Haskell2010 |
Module, providing singleton boilerplate for
T
data types.
Some functions from Data.Singletons are provided alternative version here.
Synopsis
- data SingT z where
- STKey :: SingT ('TKey :: T)
- STUnit :: SingT ('TUnit :: T)
- STSignature :: SingT ('TSignature :: T)
- STChainId :: SingT ('TChainId :: T)
- STOption :: forall (n :: T). (Sing n) -> SingT ('TOption n :: T)
- STList :: forall (n :: T). (Sing n) -> SingT ('TList n :: T)
- STSet :: forall (n :: T). (Sing n) -> SingT ('TSet n :: T)
- STOperation :: SingT ('TOperation :: T)
- STContract :: forall (n :: T). (Sing n) -> SingT ('TContract n :: T)
- STTicket :: forall (n :: T). (Sing n) -> SingT ('TTicket n :: T)
- STPair :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TPair n n :: T)
- STOr :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TOr n n :: T)
- STLambda :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TLambda n n :: T)
- STMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TMap n n :: T)
- STBigMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TBigMap n n :: T)
- STInt :: SingT ('TInt :: T)
- STNat :: SingT ('TNat :: T)
- STString :: SingT ('TString :: T)
- STBytes :: SingT ('TBytes :: T)
- STMutez :: SingT ('TMutez :: T)
- STBool :: SingT ('TBool :: T)
- STKeyHash :: SingT ('TKeyHash :: T)
- STBls12381Fr :: SingT ('TBls12381Fr :: T)
- STBls12381G1 :: SingT ('TBls12381G1 :: T)
- STBls12381G2 :: SingT ('TBls12381G2 :: T)
- STTimestamp :: SingT ('TTimestamp :: T)
- STAddress :: SingT ('TAddress :: T)
- STChest :: SingT ('TChest :: T)
- STChestKey :: SingT ('TChestKey :: T)
- STSaplingState :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingState n :: T)
- STSaplingTransaction :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingTransaction n :: T)
- STNever :: SingT ('TNever :: T)
- castSingE :: forall (a :: T) (b :: T) t. (SingI a, SingI b) => t a -> Either Text (t b)
- castM :: forall (a :: T) (b :: T) t m. (SingI a, SingI b, Monad m) => t a -> (forall x. MismatchError T -> m x) -> m (t b)
- eqP :: forall (a :: T) (b :: T). (SingI a, SingI b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- requireEq :: forall (a :: T) (b :: T) m. (SingI a, SingI b, Monad m) => (forall x. MismatchError T -> m x) -> m (a :~: b)
Documentation
STKey :: SingT ('TKey :: T) | |
STUnit :: SingT ('TUnit :: T) | |
STSignature :: SingT ('TSignature :: T) | |
STChainId :: SingT ('TChainId :: T) | |
STOption :: forall (n :: T). (Sing n) -> SingT ('TOption n :: T) | |
STList :: forall (n :: T). (Sing n) -> SingT ('TList n :: T) | |
STSet :: forall (n :: T). (Sing n) -> SingT ('TSet n :: T) | |
STOperation :: SingT ('TOperation :: T) | |
STContract :: forall (n :: T). (Sing n) -> SingT ('TContract n :: T) | |
STTicket :: forall (n :: T). (Sing n) -> SingT ('TTicket n :: T) | |
STPair :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TPair n n :: T) | |
STOr :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TOr n n :: T) | |
STLambda :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TLambda n n :: T) | |
STMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TMap n n :: T) | |
STBigMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TBigMap n n :: T) | |
STInt :: SingT ('TInt :: T) | |
STNat :: SingT ('TNat :: T) | |
STString :: SingT ('TString :: T) | |
STBytes :: SingT ('TBytes :: T) | |
STMutez :: SingT ('TMutez :: T) | |
STBool :: SingT ('TBool :: T) | |
STKeyHash :: SingT ('TKeyHash :: T) | |
STBls12381Fr :: SingT ('TBls12381Fr :: T) | |
STBls12381G1 :: SingT ('TBls12381G1 :: T) | |
STBls12381G2 :: SingT ('TBls12381G2 :: T) | |
STTimestamp :: SingT ('TTimestamp :: T) | |
STAddress :: SingT ('TAddress :: T) | |
STChest :: SingT ('TChest :: T) | |
STChestKey :: SingT ('TChestKey :: T) | |
STSaplingState :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingState n :: T) | |
STSaplingTransaction :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingTransaction n :: T) | |
STNever :: SingT ('TNever :: T) |
Instances
(SDecide T, SDecide Peano) => TestCoercion SingT Source # | |
Defined in Morley.Michelson.Typed.Sing | |
(SDecide T, SDecide Peano) => TestEquality SingT Source # | |
Defined in Morley.Michelson.Typed.Sing |
castM :: forall (a :: T) (b :: T) t m. (SingI a, SingI b, Monad m) => t a -> (forall x. MismatchError T -> m x) -> m (t b) Source #
Monadic version of castSing
.
Throws an error using the given function if the cast fails.
eqP :: forall (a :: T) (b :: T). (SingI a, SingI b) => Proxy a -> Proxy b -> Maybe (a :~: b) Source #
requireEq :: forall (a :: T) (b :: T) m. (SingI a, SingI b, Monad m) => (forall x. MismatchError T -> m x) -> m (a :~: b) Source #
Monadic version of eqI
.
Throws an error using the given function if the two types are not equal.