| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 ScopeInfo | Source

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 a | Source

Same as `withScope`, but discard the scope from the computation.

localScope :: MonadTCM tcm => tcm a -> tcm a | Source

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 a | Source

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