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
wakeIrrelevantVars	Agda.TypeChecking.Irrelevance
wakeupConstraints	Agda.TypeChecking.Constraints
wakeupConstraints_	Agda.TypeChecking.Constraints
wakeupListener	Agda.TypeChecking.MetaVars
walkSatisfying	Agda.Utils.Graph.AdjacencyMap.Unidirectional
Warning	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
warning	Agda.TypeChecking.Warnings
WarningMode	Agda.Interaction.Options
warning_	Agda.TypeChecking.Warnings
warnRange	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
warshall	Agda.Utils.Warshall
warshallG	Agda.Utils.Warshall
Weak	Agda.Auto.Syntax
weak	Agda.Auto.Syntax
weak'	Agda.Auto.Syntax
Weakening	Agda.Auto.Syntax
weakenModuleParameters	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
weakly	Agda.TypeChecking.MetaVars.Occurs
WeaklyRigid
1 (Data Constructor)	Agda.TypeChecking.Free.Lazy
2 (Data Constructor)	Agda.TypeChecking.Free
3 (Data Constructor)	Agda.TypeChecking.Free.Old
weaklyRigidVars
1 (Function)	Agda.TypeChecking.Free
2 (Function)	Agda.TypeChecking.Free.Old
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
wfExprTypes	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.Options, 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
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.Notation
wildOrUnqualifiedName	Agda.Syntax.Concrete.Operators.Parser
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
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
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
WithForce	Agda.Interaction.BasicOps
withFreezeMetas	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
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
withModuleParameters	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
withName	Agda.Syntax.Translation.ReflectedToAbstract
withNamedArgsFrom	Agda.Syntax.Common
WithNames	Agda.Syntax.Translation.ReflectedToAbstract
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
WithoutForce	Agda.Interaction.BasicOps
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
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
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
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
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
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
WrongParameters	Agda.Syntax.Concrete.Definitions
WSM	Agda.Syntax.Scope.Monad