Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x8fef28d2026-11-02Search packagesCtrl K

Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 8fef28d · 2026-11-02

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Monad.Env

Contents

Controlling reduction.
Concerning envInsideDotPattern

Synopsis

value currentModule
value withCurrentModule
value getCurrentPath
value getAnonymousVariables
value withAnonymousModule
value withEnv
value getEnv
value withHighlightingLevel
value doExpandLast
value dontExpandLast
value reallyDontExpandLast
value performedSimplification
value performedSimplification'
value getSimplification
value updateAllowedReductions
value modifyAllowedReductions
value putAllowedReductions
value onlyReduceProjections
value allowAllReductions
value allowNonTerminatingReductions
value onlyReduceTypes
value typeLevelReductions
value insideDotPattern
value isInsideDotPattern
value callByName
value dontFoldLetBindings

PackageAgda-2.8.0.2
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, MonadFileId 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.

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

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.