Agda-2.2.6: A dependently typed functional programming language and proof assistant




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.