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




resetState :: TCM ()Source

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

resetAllState :: TCM ()Source

Resets all of the type checking state.

setScope :: ScopeInfo -> TCM ()Source

Set the current scope.

getScope :: TCM ScopeInfoSource

Get the current scope.

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

Sets stExtLambdaTele .

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

Get stExtLambdaTele.

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

Modify the current scope.

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

Run a computation in a local scope.

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

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

localScope :: TCM a -> TCM aSource

Discard any changes to the scope by a computation.

setTopLevelModule :: QName -> TCM ()Source

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

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

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

addHaskellImport :: String -> TCM ()Source

Tell the compiler to import the given Haskell module.

getHaskellImports :: TCM (Set String)Source

Get the Haskell imports.