Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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.

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

Don't fold let bindings when printing. This is a bit crude since it disables any folding of let bindings at all. In many cases it's better to use removeLetBinding before printing to drop the let bindings that should not be folded.