A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
#
$
%
&
+
.
/
<
=
>
?
@
\
^
|
-
_
All

Index - W

wakeConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeConstraints'	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeConstraintsTCM	Agda.TypeChecking.Constraints
wakeIfBlockedOnDef	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIfBlockedOnMeta	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIfBlockedOnProblem	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeIrrelevantVars	Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WakeUp
1 (Type/Class)	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeupConstraints	Agda.TypeChecking.Constraints
wakeupConstraints_	Agda.TypeChecking.Constraints
wakeupListener	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeUpWhen	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
wakeUpWhen_	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
walkSatisfying	Agda.Utils.Graph.AdjacencyMap.Unidirectional
warn2Error	Agda.Interaction.Options.Warnings
warnEmptyPolarityPragma	Agda.Syntax.Concrete.Fixity
warnForPlentyInHardCompileTimeMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Warning	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warning	Agda.TypeChecking.Warnings
warning'	Agda.TypeChecking.Warnings
warning'_	Agda.TypeChecking.Warnings
warningArg	Agda.Interaction.Options.Arguments
warningHighlighting	Agda.Interaction.Highlighting.Generate
WarningMode
1 (Type/Class)	Agda.Interaction.Options.Warnings, Agda.Interaction.Options
2 (Data Constructor)	Agda.Interaction.Options.Warnings, Agda.Interaction.Options
WarningModeError	Agda.Interaction.Options.Warnings
warningModeUpdate	Agda.Interaction.Options.Warnings
WarningName	Agda.Interaction.Options.Warnings
warningName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warningNameToString	Agda.Interaction.Options.Warnings
WarningOnImport	Agda.Syntax.Concrete
WarningOnUsage	Agda.Syntax.Concrete
WarningProblem	Agda.Interaction.Options
WarningProblem_	Agda.Interaction.Options.Warnings
warnings
1 (Function)	Agda.Interaction.Library.Base
2 (Function)	Agda.TypeChecking.Warnings
warnings'	Agda.Interaction.Library.Base
WarningsAndNonFatalErrors
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Warnings, Agda.Interaction.Response, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warningSet	Agda.Interaction.Options.Warnings
warningSets	Agda.Interaction.Options.Warnings
warningValues	Agda.Interaction.Options.Arguments
warning_	Agda.TypeChecking.Warnings
warnOnRecordFieldWarnings	Agda.TypeChecking.Records
warnPolarityPragmasButNotPostulates	Agda.Syntax.Concrete.Fixity
warnRange	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
warnUnknownFixityInMixfixDecl	Agda.Syntax.Concrete.Fixity
warnUnknownNamesInFixityDecl	Agda.Syntax.Concrete.Fixity
warnUnknownNamesInPolarityPragmas	Agda.Syntax.Concrete.Fixity
weaken	Agda.Utils.VarSet
weakly	Agda.TypeChecking.MetaVars.Occurs
WeaklyRigid	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
Weight	Agda.TypeChecking.SizedTypes.WarshallSolver
wfAfterTel	Agda.TypeChecking.Rules.Def
wfBeforeTel	Agda.TypeChecking.Rules.Def
wfCallSubst	Agda.TypeChecking.Rules.Def
wfClauses	Agda.TypeChecking.Rules.Def
wfExprs	Agda.TypeChecking.Rules.Def
wfLetBindings	Agda.TypeChecking.Rules.Def
wfName	Agda.TypeChecking.Rules.Def
wfParentName	Agda.TypeChecking.Rules.Def
wfParentParams	Agda.TypeChecking.Rules.Def
wfParentPats	Agda.TypeChecking.Rules.Def
wfParentTel	Agda.TypeChecking.Rules.Def
wfParentType	Agda.TypeChecking.Rules.Def
wfPermFinal	Agda.TypeChecking.Rules.Def
wfPermParent	Agda.TypeChecking.Rules.Def
wfPermSplit	Agda.TypeChecking.Rules.Def
wfRHSType	Agda.TypeChecking.Rules.Def
when	Agda.Utils.Monad
whenAbstractFreezeMetasAfter	Agda.TypeChecking.Rules.Decl
whenConstraints	Agda.TypeChecking.Constraints
whenExactVerbosity	Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
whenJust
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
whenJustM
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
whenM	Agda.Utils.Monad
whenNothing	Agda.Utils.Maybe
whenNothingM	Agda.Utils.Maybe
whenNull	Agda.Utils.Null
whenNullM	Agda.Utils.Null
whenProfile	Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Where	Agda.TypeChecking.Positivity.Occurrence
whereAnywhere	Agda.Syntax.Abstract
WhereClause	Agda.Syntax.Concrete
WhereClause'	Agda.Syntax.Concrete
WhereClausesNotAllowed	Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WhereClause_	Agda.Syntax.Concrete
whereClause_	Agda.Syntax.Concrete
WhereDeclarations	Agda.Syntax.Abstract
WhereDeclarationsSpine	Agda.Syntax.Abstract
whereDeclarationsSpine	Agda.Syntax.Abstract
WhereDecls	Agda.Syntax.Abstract
whereDecls	Agda.Syntax.Abstract
WhereDeclsS	Agda.Syntax.Abstract
whereModule	Agda.Syntax.Abstract
whHiding	Agda.Syntax.Common
WhichWarnings	Agda.TypeChecking.Warnings
whileLeft	Agda.Utils.Either
whThing	Agda.Syntax.Common
WhyCheckModality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WhyInScope	Agda.Syntax.Scope.Base
whyInScope
1 (Function)	Agda.Interaction.BasicOps
2 (Function)	Agda.Interaction.InteractionTop
WhyInScopeData
1 (Type/Class)	Agda.Syntax.Scope.Base
2 (Data Constructor)	Agda.Syntax.Scope.Base
whyInScopeDataFromAbstractName	Agda.Syntax.Scope.Base
whyInScopeDataFromAmbiguousNameReason	Agda.Syntax.Scope.Base
WhyInvalidInstanceType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WhyNotAHaskellType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WildP
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
WildPart	Agda.Syntax.Common
WildV	Agda.Syntax.Concrete.Operators.Parser
With	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
withAnonymousModule	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithApp
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
withAppBrackets	Agda.Syntax.Fixity
WithArgCtx	Agda.Syntax.Fixity
withArgsFrom	Agda.Syntax.Common
withArguments	Agda.TypeChecking.With
WithArity
1 (Type/Class)	Agda.TypeChecking.CompiledClause
2 (Data Constructor)	Agda.TypeChecking.CompiledClause
withArray	Agda.Interaction.JSON
withBool	Agda.Interaction.JSON
WithBound	Agda.Syntax.Scope.Base
withBranchAndGoal	Agda.Mimer.Monad
withBranchState	Agda.Mimer.Monad
withCallerCallStack	Agda.Utils.CallStack
withCatchallPragma	Agda.Syntax.Concrete.Definitions.Monad
withCheckNoShadowing	Agda.Syntax.Scope.Monad
withClausePattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithClausePatternMismatch	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithClausePatternMismatch_	Agda.Interaction.Options.Errors
WithClauseProjectionFixityMismatch	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithClauseProjectionFixityMismatch_	Agda.Interaction.Options.Warnings
withClauseProjectionOrigin	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withClosure	Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withComputeIgnoreAbstract	Agda.Interaction.BasicOps
withConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withContextPrecedence	Agda.Syntax.Scope.Monad
withCoverageCheckPragma	Agda.Syntax.Concrete.Definitions.Monad
withCurrentCallStack	Agda.Utils.CallStack
withCurrentFile	Agda.Interaction.InteractionTop
withCurrentModule
1 (Function)	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)	Agda.Syntax.Scope.Monad
withCurrentModule'	Agda.Syntax.Scope.Monad
WithDefault	Agda.Utils.WithDefault
WithDefault'	Agda.Utils.WithDefault
withDisplayForm	Agda.TypeChecking.With
withEmbeddedJSON	Agda.Interaction.JSON
withEnv	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withError	Agda.Utils.Monad
WithExpr
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
WithExpr'	Agda.Syntax.Abstract
withExtendedOccEnv	Agda.TypeChecking.Positivity
withExtendedOccEnv'	Agda.TypeChecking.Positivity
WithForce	Agda.Interaction.Base
withFreshName	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withFreshName_	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withFrozenMetas	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithFunction	Agda.TypeChecking.Rules.Def
WithFunctionProblem	Agda.TypeChecking.Rules.Def
withFunctionType	Agda.TypeChecking.With
WithFunCtx	Agda.Syntax.Fixity
WithHiding
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
withHiding	Agda.Syntax.Concrete.Pretty
withHighlightingLevel	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withInteractionId	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withInterval	Agda.Syntax.Parser.LexActions
withInterval'	Agda.Syntax.Parser.LexActions
withInterval_	Agda.Syntax.Parser.LexActions
WithK	Agda.Syntax.Common
WithKEnabled	Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
WithKind
1 (Type/Class)	Agda.Syntax.Scope.Base
2 (Data Constructor)	Agda.Syntax.Scope.Base
withLayout	Agda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout
withLocalVars	Agda.Syntax.Scope.Monad
withMetaId	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withMetaInfo	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withMetaInfo'	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withName	Agda.Syntax.Translation.ReflectedToAbstract
withNamedArgsFrom	Agda.Syntax.Common
withNames	Agda.Syntax.Translation.ReflectedToAbstract
withNBackCallStack	Agda.Utils.CallStack
WithNode
1 (Type/Class)	Agda.TypeChecking.Pretty
2 (Data Constructor)	Agda.TypeChecking.Pretty
withNonEmpty
1 (Function)	Agda.Utils.Map1
2 (Function)	Agda.Utils.Set1
withObject	Agda.Interaction.JSON
WithOnFreeVariable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithOnFreeVariable_	Agda.Interaction.Options.Errors
WithOrigin
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
withoutCache	Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithoutForce	Agda.Interaction.Base
WithoutK	Agda.Syntax.Common
withoutKeys	Agda.Utils.Map1
WithoutKFlagPrimEraseEquality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithoutKFlagPrimEraseEquality_	Agda.Interaction.Options.Warnings
withoutKOption	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withoutModuleCheckpoints	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withoutPrintingGeneralization	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withoutPrivates	Agda.Syntax.Scope.Base
WithP
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
withPositivityCheckPragma	Agda.Syntax.Concrete.Definitions.Monad
withPragmaOptions	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withRangeOf	Agda.Syntax.Position
withRangesOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
withRangesOfQ	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
withReduced	Agda.TypeChecking.Constraints
WithRHS	Agda.Syntax.Abstract
WithRHSS	Agda.Syntax.Abstract
withScientific	Agda.Interaction.JSON
withScope	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShadowingNameTCM	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShowAllArguments	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withShowAllArguments'	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withSignature	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withSome	Agda.Utils.IndexedList
withStandardLock	Agda.Syntax.Common
withTCState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withTerminationCheckPragma	Agda.Syntax.Concrete.Definitions.Monad
withText	Agda.Interaction.JSON
withTopLevelModule	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithUniqueInt
1 (Type/Class)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Data Constructor)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
withUniverseCheckPragma	Agda.Syntax.Concrete.Definitions.Monad
withUsableVars	Agda.Termination.Monad
withVar	Agda.Syntax.Translation.ReflectedToAbstract
withVarOcc	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
withVars	Agda.Syntax.Translation.ReflectedToAbstract
Wk	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
wkS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
woOrigin	Agda.Syntax.Common
word64View	Agda.Syntax.Treeless, Agda.Compiler.Backend
wordBounded	Agda.Interaction.Highlighting.Vim
wordFoldlBits#	Agda.Utils.Word
wordFoldlBitsOffset#	Agda.Utils.Word
wordFoldlBitsOffsetStrict#	Agda.Utils.Word
wordFoldlBitsStrict#	Agda.Utils.Word
wordFoldrBits#	Agda.Utils.Word
wordFoldrBitsOffset#	Agda.Utils.Word
wordFoldrBitsOffsetStrict#	Agda.Utils.Word
wordFoldrBitsStrict#	Agda.Utils.Word
wordsBy	Agda.Utils.List1
workOnTypes	Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
workOnTypes'	Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
woThing	Agda.Syntax.Common
write
1 (Function)	Agda.Utils.MinimalArray.MutablePrim
2 (Function)	Agda.Utils.MinimalArray.MutableLifted
writeFile	Agda.Utils.IO.UTF8
writeIORef
1 (Function)	Agda.Utils.IORef
2 (Function)	Agda.Utils.IORef.Strict
writeModule	Agda.Compiler.JS.Compiler
writeTextToFile	Agda.Utils.IO.UTF8
writeTime	Agda.Mimer.Monad
writeToCurrentLog	Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
writeToTempFile	Agda.Utils.IO.TempFile
writeUnifyLog	Agda.TypeChecking.Rules.LHS.Unify.Types
WrongAnnotationInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongAnnotationInLambda_	Agda.Interaction.Options.Errors
WrongArgInfoForPrimitive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongArgInfoForPrimitive_	Agda.Interaction.Options.Errors
WrongCohesionInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongCohesionInLambda_	Agda.Interaction.Options.Errors
WrongContentBlock	Agda.Syntax.Concrete.Definitions.Errors
WrongContentBlock_	Agda.Interaction.Options.Errors
WrongDefinition	Agda.Syntax.Concrete.Definitions.Errors
WrongDefinition_	Agda.Interaction.Options.Errors
WrongHidingInApplication	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInApplication_	Agda.Interaction.Options.Errors
WrongHidingInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInLambda_	Agda.Interaction.Options.Errors
WrongHidingInLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInLHS_	Agda.Interaction.Options.Errors
WrongHidingInProjection	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInProjection_	Agda.Interaction.Options.Errors
WrongInstanceDeclaration	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongInstanceDeclaration_	Agda.Interaction.Options.Warnings
WrongIrrelevanceInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongIrrelevanceInLambda_	Agda.Interaction.Options.Errors
WrongNamedArgument	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongNamedArgument_	Agda.Interaction.Options.Errors
WrongNumberOfConstructorArguments	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongNumberOfConstructorArguments_	Agda.Interaction.Options.Errors
WrongPolarityInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongPolarityInLambda_	Agda.Interaction.Options.Errors
WrongPragmaFor	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongPragmaFor_	Agda.Interaction.Options.Errors
WrongQuantityInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongQuantityInLambda_	Agda.Interaction.Options.Errors
WrongSharpArity	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongSharpArity_	Agda.Interaction.Options.Errors
WrongTypeOfMain	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongTypeOfMain_	Agda.Interaction.Options.Errors
WSM	Agda.Syntax.Scope.Monad