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

Synopsis

Writes a TypeCheckAction to the current log, using the current PostScopeState

Reads the next entry in the cached type check log, if present.

Empties the "to read" CachedState. To be used when it gets invalid.

Caches the current type check log. Discardes the old cache. Does nothing if caching is inactive.

# Activating/deactivating

Makes sure that the stLoadedFileCache is Just, with a clean current log. Crashes is stLoadedFileCache is already active with a dirty log. Should be called when we start typechecking the current file.

To be called before any write or restore calls.

withoutCache :: TCM a -> TCM a Source #

Runs the action without cache and restores the current cache at the end of it.