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.6.0