Skip to content

HORIZON HASKELL Docs lts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Monad.Env

26 values

PackageAgda-2.7.0.1
Exports26
LanguageHaskell2010
LicenceMIT
SourceEnv.hs

valuecurrentModule :: MonadTCEnv m => m ModuleName

Get the name of the current module, if any.

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

Set the name of the current module.

valuegetCurrentPath :: MonadTCEnv m => m AbsolutePath

Get the path of the currently checked file

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

Get the number of variables bound by anonymous modules.

valuewithAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a

Add variables bound by an anonymous module.

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

Set the current environment to the given

valuegetEnv :: TCM TCEnv

Get the current environment

valuewithHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a

Set highlighting level

valuedoExpandLast :: TCM a -> TCM a

Restore setting for ExpandLast to default.

valuedontExpandLast :: TCM a -> TCM a

valuereallyDontExpandLast :: TCM a -> TCM a

valueperformedSimplification :: MonadTCEnv m => m a -> m a

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

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

valuegetSimplification :: MonadTCEnv m => m Simplification

Controlling reduction.

8 declarations

valueupdateAllowedReductions

:: AllowedReductions -> AllowedReductions
-> TCEnv
-> TCEnv

Lens for AllowedReductions.

valuemodifyAllowedReductions

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

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

valueonlyReduceProjections :: MonadTCEnv m => m a -> m a

Reduce Def f vs only if f is a projection.

valueallowAllReductions :: MonadTCEnv m => m a -> m a

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

valueallowNonTerminatingReductions :: MonadTCEnv m => m a -> m a

Allow all reductions including non-terminating functions.

valueonlyReduceTypes :: MonadTCEnv m => m a -> m a

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

valuetypeLevelReductions :: MonadTCEnv m => m a -> m a

Update allowed reductions when working on types

Concerning envInsideDotPattern

4 declarations

valueinsideDotPattern :: TCM a -> TCM a

valueisInsideDotPattern :: TCM Bool

valuecallByName :: TCM a -> TCM a

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

valuedontFoldLetBindings :: MonadTCEnv m => m a -> m a

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.