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.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
wakeConstraints'	Agda.TypeChecking.Constraints
wakeConstraintsTCM	Agda.TypeChecking.Constraints
wakeIrrelevantVars	Agda.TypeChecking.Irrelevance
wakeupConstraints	Agda.TypeChecking.Constraints
wakeupConstraints_	Agda.TypeChecking.Constraints
wakeupListener	Agda.TypeChecking.MetaVars
walkSatisfying	Agda.Utils.Graph.AdjacencyMap.Unidirectional
warn2Error	Agda.Interaction.Options.Warnings
Warning	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
warningModeUpdate	Agda.Interaction.Options.Warnings
WarningName	Agda.Interaction.Options.Warnings
warningName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warningName2String	Agda.Interaction.Options.Warnings
WarningOnImport	Agda.Syntax.Concrete
WarningOnUsage	Agda.Syntax.Concrete
warnings	Agda.TypeChecking.Warnings
WarningsAndNonFatalErrors	Agda.TypeChecking.Warnings, Agda.Interaction.Response
warningSet	Agda.Interaction.Options.Warnings
warningSets	Agda.Interaction.Options.Warnings
warning_	Agda.TypeChecking.Warnings
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.TypeChecking.SizedTypes.WarshallSolver
2 (Type/Class)	Agda.Utils.Warshall
wfAfterTel	Agda.TypeChecking.Rules.Def
wfBeforeTel	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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
Where	Agda.TypeChecking.Positivity.Occurrence
WhereClause	Agda.Syntax.Concrete
WhereClause'	Agda.Syntax.Concrete
WhereDeclarations	Agda.Syntax.Abstract
WhereDecls	Agda.Syntax.Abstract
whereDecls	Agda.Syntax.Abstract
whereModule	Agda.Syntax.Abstract
whHiding	Agda.Syntax.Common
WhichWarnings	Agda.TypeChecking.Warnings
whileLeft	Agda.Utils.Either
whThing	Agda.Syntax.Common
WhyInScope	Agda.Syntax.Scope.Base
whyInScope
1 (Function)	Agda.Interaction.BasicOps
2 (Function)	Agda.Interaction.InteractionTop
WildHole	Agda.Syntax.Common
WildP
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
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
withCheckNoShadowing	Agda.Syntax.Scope.Monad
WithClausePatternMismatch	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withClosure	Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withContextPrecedence	Agda.Syntax.Scope.Monad
withCurrentFile
1 (Function)	Agda.Interaction.CommandLine
2 (Function)	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
withDisplayForm	Agda.TypeChecking.With
withEnv	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithExpr	Agda.Syntax.Concrete
withExtendedOccEnv	Agda.TypeChecking.Positivity
withExtendedOccEnv'	Agda.TypeChecking.Positivity
withFileAndLine	Agda.Utils.Impossible
withFileAndLine'	Agda.Utils.Impossible
WithForce	Agda.Interaction.Base
withFreezeMetas	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withFreshName	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withFreshName_	Agda.TypeChecking.Monad.Context, 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
withImportPath	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withIncreasedModuleNestingLevel	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withInteractionId	Agda.Interaction.BasicOps
withInterval	Agda.Syntax.Parser.LexActions
withInterval'	Agda.Syntax.Parser.LexActions
withInterval_	Agda.Syntax.Parser.LexActions
withLayout	Agda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout
withLocalVars	Agda.Syntax.Scope.Monad
withMetaId	Agda.Interaction.BasicOps
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
WithNode
1 (Type/Class)	Agda.TypeChecking.Pretty
2 (Data Constructor)	Agda.TypeChecking.Pretty
WithOnFreeVariable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
withoutOptionsChecking	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithP
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
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
WithRHS	Agda.Syntax.Abstract
withScope
1 (Function)	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)	Agda.Syntax.Translation.AbstractToConcrete
withScope_	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WithSeenUIds
1 (Type/Class)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Auto.Syntax
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
withTCState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withTopLevelModule	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withUsableVars	Agda.Termination.Monad
withVarOcc	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
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.List
workOnTypes	Agda.TypeChecking.Irrelevance
workOnTypes'	Agda.TypeChecking.Irrelevance
woThing	Agda.Syntax.Common
writeFile	Agda.Utils.IO.UTF8
writeInterface	Agda.Interaction.Imports
writeIORef	Agda.Utils.IORef
writeModule
1 (Function)	Agda.Compiler.MAlonzo.Compiler
2 (Function)	Agda.Compiler.JS.Compiler
writeTextToFile	Agda.Utils.IO.UTF8
writeToCurrentLog	Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
writeToTempFile	Agda.Utils.IO.TempFile
WrongCohesionInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongContentBlock	Agda.Syntax.Concrete.Definitions
WrongDefinition	Agda.Syntax.Concrete.Definitions
WrongHidingInApplication	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongHidingInLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
WrongNamedArgument	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongNumberOfConstructorArguments	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongQuantityInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WSM	Agda.Syntax.Scope.Monad