| waitok | Agda.Auto.NarrowingSearch |
| wakeConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| wakeConstraints' | Agda.TypeChecking.Constraints |
| wakeConstraintsTCM | Agda.TypeChecking.Constraints |
| 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.TypeChecking.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.TypeChecking.SizedTypes.WarshallSolver |
| 2 (Type/Class) | Agda.Utils.Warshall |
| 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 |
| 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.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 |
| 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 |
| 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 |
| withReduced | Agda.TypeChecking.Reduce |
| WithRHS | 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.List |
| 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 |
| 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 |