Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Monad.Env

Synopsis

Documentation

currentModule :: MonadTCEnv m => m ModuleName Source #

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.

getCurrentPath :: MonadTCEnv m => m AbsolutePath Source #

Get the path of the currently checked file

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

Get the number of variables bound by anonymous modules.

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

Add variables bound by an anonymous module.

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

Set the current environment to the given

getEnv :: TCM TCEnv Source #

Get the current environment

withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a Source #

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.

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. Otherwise only allow inlined functions to be unfolded.

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.