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
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
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
warningName2String	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
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
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
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
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
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.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
withCallerCallStack	Agda.Utils.CallStack
withCatchallPragma	Agda.Syntax.Concrete.Definitions.Monad
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
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
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
withImportPath	Agda.TypeChecking.Monad.Imports, 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
withObject	Agda.Interaction.JSON
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
WithoutK	Agda.Syntax.Common
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
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
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
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
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
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
writeFile	Agda.Utils.IO.UTF8
writeIORef	Agda.Utils.IORef
writeModule	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
writeUnifyLog	Agda.TypeChecking.Rules.LHS.Unify.Types
WrongArgInfoForPrimitive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongCohesionInLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
WrongContentBlock	Agda.Syntax.Concrete.Definitions.Errors
WrongDefinition	Agda.Syntax.Concrete.Definitions.Errors
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
WrongHidingInProjection	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