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

waitok	Agda.Auto.NarrowingSearch
wakeConstraints	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
wakeConstraints'	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
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.Irrelevance
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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
Warning	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
warning	Agda.TypeChecking.Warnings
warning'	Agda.TypeChecking.Warnings
warning'_	Agda.TypeChecking.Warnings
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.Compiler.Backend, Agda.TypeChecking.Monad
warningName2String	Agda.Interaction.Options.Warnings
WarningOnImport	Agda.Syntax.Concrete
WarningOnUsage	Agda.Syntax.Concrete
warnings
1 (Function)	Agda.Interaction.Library.Base
2 (Function)	Agda.TypeChecking.Warnings
warnings'	Agda.Interaction.Library.Base
WarningsAndNonFatalErrors	Agda.TypeChecking.Warnings, Agda.Interaction.Response
warningSet	Agda.Interaction.Options.Warnings
warningSets	Agda.Interaction.Options.Warnings
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
warshall	Agda.Utils.Warshall
warshallG	Agda.Utils.Warshall
Weak	Agda.Auto.Syntax
weak	Agda.Auto.Syntax
weak'	Agda.Auto.Syntax
Weakening	Agda.Auto.Syntax
weakly	Agda.TypeChecking.MetaVars.Occurs
WeaklyRigid	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
Weight
1 (Type/Class)	Agda.Utils.Warshall
2 (Type/Class)	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
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
whatInduction	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
when	Agda.Utils.Monad
whenAbstractFreezeMetasAfter	Agda.TypeChecking.Rules.Decl
whenConstraints	Agda.TypeChecking.Constraints
whenExactVerbosity	Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
Where	Agda.TypeChecking.Positivity.Occurrence
whereAnywhere	Agda.Syntax.Abstract
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.Compiler.Backend, Agda.TypeChecking.Monad
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
whyInScopeDataFromAmbiguousNameReason	Agda.Syntax.Scope.Base
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
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
withCallerCallStack	Agda.Utils.CallStack
withCatchallPragma	Agda.Syntax.Concrete.Definitions.Monad
withCheckNoShadowing	Agda.Syntax.Scope.Monad
WithClausePatternMismatch	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withClosure	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Closure
withCompilerFlag	Agda.Compiler.MAlonzo.Compiler
withConstraint	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
withContextPrecedence	Agda.Syntax.Scope.Monad
withCoverageCheckPragma	Agda.Syntax.Concrete.Definitions.Monad
withCurrentCallStack	Agda.Utils.CallStack
withCurrentFile	Agda.Interaction.InteractionTop
withCurrentModule
1 (Function)	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
2 (Function)	Agda.Syntax.Scope.Monad
withCurrentModule'	Agda.Syntax.Scope.Monad
WithDefault	Agda.Utils.WithDefault
withDisplayForm	Agda.TypeChecking.With
withEmbeddedJSON	Agda.Interaction.JSON
withEnv	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
withFreshName_	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
withFrozenMetas	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
withImportPath	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
withInteractionId	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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, Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
withMetaInfo	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
withMetaInfo'	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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
withObject	Agda.Interaction.JSON
WithOnFreeVariable	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WithOrigin
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
withoutCache	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
WithoutForce	Agda.Interaction.Base
WithoutK	Agda.Syntax.Common
WithoutKFlagPrimEraseEquality	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WithoutKFlagPrimEraseEquality_	Agda.Interaction.Options.Warnings
withoutKOption	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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
WithRHS	Agda.Syntax.Abstract
WithRHSS	Agda.Syntax.Abstract
withScientific	Agda.Interaction.JSON
withScope
1 (Function)	Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Function)	Agda.Syntax.Translation.AbstractToConcrete
withScope_	Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WithSeenUIds
1 (Type/Class)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Auto.Syntax
withShadowingNameTCM	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
withShowAllArguments	Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withShowAllArguments'	Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withSignature	Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withSome	Agda.Utils.IndexedList
withTCState	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
withTerminationCheckPragma	Agda.Syntax.Concrete.Definitions.Monad
withText	Agda.Interaction.JSON
withTopLevelModule	Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
wordsBy	Agda.Utils.List1
workOnTypes	Agda.TypeChecking.Irrelevance
workOnTypes'	Agda.TypeChecking.Irrelevance
woThing	Agda.Syntax.Common
writeFile	Agda.Utils.IO.UTF8
writeIORef	Agda.Utils.IORef
writeModule
1 (Function)	Agda.Compiler.MAlonzo.Compiler
2 (Function)	Agda.Compiler.JS.Compiler
writeTextToFile	Agda.Utils.IO.UTF8
writeToCurrentLog	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
writeToTempFile	Agda.Utils.IO.TempFile
writeUnifyLog	Agda.TypeChecking.Rules.LHS.Unify.Types
WrongCohesionInLambda	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongContentBlock	Agda.Syntax.Concrete.Definitions.Errors
WrongDefinition	Agda.Syntax.Concrete.Definitions.Errors
WrongHidingInApplication	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongHidingInLambda	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongHidingInLHS	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongInstanceDeclaration	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongInstanceDeclaration_	Agda.Interaction.Options.Warnings
WrongIrrelevanceInLambda	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongModalityForPrimitive	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongNamedArgument	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongNumberOfConstructorArguments	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WrongQuantityInLambda	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
WSM	Agda.Syntax.Scope.Monad