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

Synopsis

# Documentation

Get the name of the current module, if any.

withCurrentModule :: MonadTCEnv m => ModuleName -> m a -> m a Source #

Set the name of the current module.

Get the path of the currently checked file

Get the number of variables bound by anonymous modules.

Add variables bound by an anonymous module.

withEnv :: MonadTCEnv m => TCEnv -> m a -> m a Source #

Set the current environment to the given

Get the current environment

Increases the module nesting level by one in the given computation.

Set highlighting level

doExpandLast :: TCM a -> TCM a Source #

Restore setting for ExpandLast to default.

performedSimplification :: MonadTCEnv m => m a -> m a Source #

If the reduced did a proper match (constructor or literal pattern), then record this as simplification step.

# Controlling reduction.

Lens for AllowedReductions.

onlyReduceProjections :: MonadTCEnv m => m a -> m a Source #

Reduce Def f vs only if f is a projection.

allowAllReductions :: MonadTCEnv m => m a -> m a Source #

Allow all reductions except for non-terminating functions (default).

allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a Source #

Allow all reductions including non-terminating functions.

onlyReduceTypes :: MonadTCEnv m => m a -> m a Source #

Allow all reductions when reducing types

typeLevelReductions :: MonadTCEnv m => m a -> m a Source #

Update allowed reductions when working on types

# Concerning envInsideDotPattern

callByName :: TCM a -> TCM a Source #

Don't use call-by-need evaluation for the given computation.