Agda-2.5.1.2: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Monad.Open
Synopsis
makeOpen :: a -> TCM (Open a) Source #
Create an open term in the current context.
makeClosed :: a -> Open a Source #
Create an open term which is closed.
isClosed :: Open a -> Bool Source #
Check if an Open is closed.
Open
getOpen :: (Subst t a, MonadReader TCEnv m) => Open a -> m a Source #
Extract the value from an open term. Must be done in an extension of the context in which the term was created.
tryOpen :: (Subst t a, MonadReader TCEnv m) => Open a -> m (Maybe a) Source #
Try to use an Open the current context. Returns Nothing if current context is not an extension of the context in which the Open was created.
Nothing