Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Monad.Open

Synopsis

- makeOpen :: MonadTCM tcm => a -> tcm (Open a)
- makeClosed :: a -> Open a
- getOpen :: (MonadTCM tcm, Raise a) => Open a -> tcm a
- tryOpen :: (MonadTCM tcm, Raise a) => Open a -> tcm (Maybe a)

# Documentation

makeOpen :: MonadTCM tcm => a -> tcm (Open a)

Create an open term in the current context.

makeClosed :: a -> Open a

Create an open term which is closed.

getOpen :: (MonadTCM tcm, Raise a) => Open a -> tcm a

Extract the value from an open term. Must be done in an extension of the context in which the term was created.

tryOpen :: (MonadTCM tcm, Raise a) => Open a -> tcm (Maybe a)