Safe Haskell | None |
---|
- currentModule :: TCM ModuleName
- withCurrentModule :: ModuleName -> TCM a -> TCM a
- getAnonymousVariables :: ModuleName -> TCM Nat
- withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a
- withEnv :: TCEnv -> TCM a -> TCM a
- getEnv :: TCM TCEnv
- withIncreasedModuleNestingLevel :: TCM a -> TCM a
- withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a
- doExpandLast :: TCM a -> TCM a
- dontExpandLast :: TCM a -> TCM a
- performedSimplification :: MonadReader TCEnv m => m a -> m a
- performedSimplification' :: MonadReader TCEnv m => Simplification -> m a -> m a
- getSimplification :: MonadReader TCEnv m => m Simplification
- onlyReduceProjections :: TCM a -> TCM a
- dontReduceProjections :: TCM a -> TCM a
- dontReduceLevels :: TCM a -> TCM a
- allowAllReductions :: TCM a -> TCM a
- allowNonTerminatingReductions :: TCM a -> TCM a
- insideDotPattern :: TCM a -> TCM a
- isInsideDotPattern :: TCM Bool
- isReifyingUnquoted :: TCM Bool
- nowReifyingUnquoted :: TCM a -> TCM a
Documentation
currentModule :: TCM ModuleNameSource
Get the name of the current module, if any.
withCurrentModule :: ModuleName -> TCM a -> TCM aSource
Set the name of the current module.
getAnonymousVariables :: ModuleName -> TCM NatSource
Get the number of variables bound by anonymous modules.
withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM aSource
Add variables bound by an anonymous module.
withIncreasedModuleNestingLevel :: TCM a -> TCM aSource
Increases the module nesting level by one in the given computation.
withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM aSource
Set highlighting level
doExpandLast :: TCM a -> TCM aSource
Restore setting for ExpandLast
to default.
dontExpandLast :: TCM a -> TCM aSource
performedSimplification :: MonadReader TCEnv m => m a -> m aSource
If the reduced did a proper match (constructor or literal pattern), then record this as simplification step.
performedSimplification' :: MonadReader TCEnv m => Simplification -> m a -> m aSource
onlyReduceProjections :: TCM a -> TCM aSource
Reduce Def f vs
only if f
is a projection.
dontReduceProjections :: TCM a -> TCM aSource
dontReduceLevels :: TCM a -> TCM aSource
allowAllReductions :: TCM a -> TCM aSource
allowNonTerminatingReductions :: TCM a -> TCM aSource
insideDotPattern :: TCM a -> TCM aSource
isInsideDotPattern :: TCM BoolSource
isReifyingUnquoted :: TCM BoolSource
nowReifyingUnquoted :: TCM a -> TCM aSource