Morley.Michelson.Typed.Scope.Internal.Presence

Documentation

data TPresence p t where

Whether a value of this type _may_ contain a type defined by TPredicateSym.

Constructors

TPresent :: ContainsT p t ~ 'True => TPresence p t

TAbsent :: ContainsT p t ~ 'False => TPresence p t

Instances

Show (TPresence t p)

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

Methods

showsPrec :: Int -> TPresence t p -> ShowS

show :: TPresence t p -> String

showList :: [TPresence t p] -> ShowS

checkTPresence :: forall p ty. Sing p -> Sing ty -> TPresence p ty

Check for presence of type defined by TPredicateSym at runtime. Use TPredicateSym singletons (i.e. SingTPredicateSym) as the first parameter, e.g.:

>>> checkTPresence SPSOp STOperation
TPresent
>>> checkTPresence SPSOp STUnit
TAbsent

To only prove absence of some type, it is more efficient to use deMorganForbidT or withDeMorganScope.

tPresence :: Sing p -> Sing t -> Maybe (ContainsT p t :~: 'True)

tAbsence :: Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)