Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
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
a
Source
Create an open term which is closed.
getOpen
:: (
MonadTCM
tcm,
Raise
a) =>
Open
a -> tcm 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
:: (
MonadTCM
tcm,
Raise
a) =>
Open
a -> tcm (
Maybe
a)
Source
Produced by
Haddock
version 2.6.0