Agda.TypeChecking.Monad.State

Documentation

resetState :: TCM ()

Resets the non-persistent part of the type checking state.

resetAllState :: TCM ()

Resets all of the type checking state.

setScope :: ScopeInfo -> TCM ()

Set the current scope.

getScope :: TCM ScopeInfo

Get the current scope.

setExtLambdaTele :: Map QName (Int, Int) -> TCM ()

Sets stExtLambdaTele .

getExtLambdaTele :: TCM (Map QName (Int, Int))

Get stExtLambdaTele.

addExtLambdaTele :: QName -> (Int, Int) -> TCM ()

modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()

Modify the current scope.

withScope :: ScopeInfo -> TCM a -> TCM (a, ScopeInfo)

Run a computation in a local scope.

withScope_ :: ScopeInfo -> TCM a -> TCM a

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

localScope :: TCM a -> TCM a

Discard any changes to the scope by a computation.

setTopLevelModule :: QName -> TCM ()

Set the top-level module. This affects the global module id of freshly generated names.

withTopLevelModule :: QName -> TCM a -> TCM a

Use a different top-level module for a computation. Used when generating names for imported modules.

addHaskellImport :: String -> TCM ()

Tell the compiler to import the given Haskell module.

getHaskellImports :: TCM (Set String)

Get the Haskell imports.