Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Monad.State
Synopsis
resetState :: MonadTCM tcm => tcm ()
setScope :: MonadTCM tcm => ScopeInfo -> tcm ()
getScope :: MonadTCM tcm => tcm ScopeInfo
modifyScope :: MonadTCM tcm => (ScopeInfo -> ScopeInfo) -> tcm ()
withScope :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm (a, ScopeInfo)
withScope_ :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm a
localScope :: MonadTCM tcm => tcm a -> tcm a
setTopLevelModule :: MonadTCM tcm => QName -> tcm ()
withTopLevelModule :: MonadTCM tcm => QName -> tcm a -> tcm a
addHaskellImport :: MonadTCM tcm => String -> tcm ()
getHaskellImports :: MonadTCM tcm => tcm (Set String)
Documentation
resetState :: MonadTCM tcm => tcm ()Source
Resets the type checking state. The persistent command line options are preserved.
setScope :: MonadTCM tcm => ScopeInfo -> tcm ()Source
Set the current scope.
getScope :: MonadTCM tcm => tcm ScopeInfoSource
Get the current scope.
modifyScope :: MonadTCM tcm => (ScopeInfo -> ScopeInfo) -> tcm ()Source
Modify the current scope.
withScope :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm (a, ScopeInfo)Source
Run a computation in a local scope.
withScope_ :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm aSource
Same as withScope, but discard the scope from the computation.
localScope :: MonadTCM tcm => tcm a -> tcm aSource
Discard any changes to the scope by a computation.
setTopLevelModule :: MonadTCM tcm => QName -> tcm ()Source
Set the top-level module. This affects the global module id of freshly generated names.
withTopLevelModule :: MonadTCM tcm => QName -> tcm a -> tcm aSource
Use a different top-level module for a computation. Used when generating names for imported modules.
addHaskellImport :: MonadTCM tcm => String -> tcm ()Source
Tell the compiler to import the given Haskell module.
getHaskellImports :: MonadTCM tcm => tcm (Set String)Source
Get the Haskell imports.
Produced by Haddock version 2.4.2