Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Lenses for TCState and more.



resetState :: TCM () Source

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

resetAllState :: TCM () Source

Resets all of the type checking state.

Keep only Benchmark information.

localTCState :: TCM a -> TCM a Source

Restore TCState after performing subcomputation.

In contrast to localState, the Benchmark info from the subcomputation is saved.

localTCStateSaving :: TCM a -> TCM (a, TCState) Source

Same as localTCState but also returns the state in which we were just before reverting it.

Lens for persistent states and its fields


getScope :: TCM ScopeInfo Source

Get the current scope.

setScope :: ScopeInfo -> TCM () Source

Set the current scope.

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

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

localScope :: TCM a -> TCM a Source

Discard any changes to the scope by a computation.

notInScope :: QName -> TCM a Source

Scope error.

printScope :: String -> Int -> String -> TCM () Source

Debug print the scope.


Lens for stSignature and stImports

withSignature :: Signature -> TCM a -> TCM a Source

Run some computation in a different signature, restore original signature.

Modifiers for rewrite rules

Modifiers for parts of the signature

Top level module

setTopLevelModule :: QName -> TCM () Source

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

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

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

Haskell imports

addHaskellImport :: String -> TCM () Source

Tell the compiler to import the given Haskell module.

getHaskellImports :: TCM (Set String) Source

Get the Haskell imports.

Interaction output callback

Pattern synonyms


getBenchmark :: TCM Benchmark Source

Lens getter for Benchmark from TCM.

modifyBenchmark :: (Benchmark -> Benchmark) -> TCM () Source

Lens modify for Benchmark.

freshTCM :: TCM a -> TCM (Either TCErr a) Source

Run a fresh instance of the TCM (with initial state). Benchmark info is preserved.

Instance definitions

addSignatureInstances :: Signature -> TCM () Source

Look through the signature and reconstruct the instance table.

clearAnonInstanceDefs :: TCM () Source

Remove all instances whose type is still unresolved.

addUnknownInstance :: QName -> TCM () Source

Add an instance whose type is still unresolved.

addNamedInstance Source


:: QName

Name of the instance.

-> QName

Name of the class.

-> TCM () 

Add instance to some `class'.