Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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)Source
Create an open term in the current context.
makeClosed :: a -> Open aSource
Create an open term which is closed.
getOpen :: (MonadTCM tcm, Raise a) => Open a -> tcm aSource
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)Source
Produced by Haddock version 2.4.2