Agda.TypeChecking.Monad.Env

Documentation

currentModule :: MonadTCEnv m => m ModuleName

Get the name of the current module, if any.

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

Set the name of the current module.

getCurrentPath :: MonadTCEnv m => m AbsolutePath

Get the path of the currently checked file

getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat

Get the number of variables bound by anonymous modules.

withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a

Add variables bound by an anonymous module.

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

Set the current environment to the given

getEnv :: TCM TCEnv

Get the current environment

withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a

Set highlighting level

doExpandLast :: TCM a -> TCM a

Restore setting for ExpandLast to default.

dontExpandLast :: TCM a -> TCM a

reallyDontExpandLast :: TCM a -> TCM a

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

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

performedSimplification' :: MonadTCEnv m => Simplification -> m a -> m a

getSimplification :: MonadTCEnv m => m Simplification

Controlling reduction.

updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv

Lens for AllowedReductions.

modifyAllowedReductions :: MonadTCEnv m => (AllowedReductions -> AllowedReductions) -> m a -> m a

putAllowedReductions :: MonadTCEnv m => AllowedReductions -> m a -> m a

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

Reduce Def f vs only if f is a projection.

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

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

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

Allow all reductions including non-terminating functions.

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

Allow all reductions when reducing types. Otherwise only allow inlined functions to be unfolded.

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

Update allowed reductions when working on types

Concerning envInsideDotPattern

insideDotPattern :: TCM a -> TCM a

isInsideDotPattern :: TCM Bool

callByName :: TCM a -> TCM a

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