| waitok | Agda.Auto.NarrowingSearch |
| wakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| wakeIrrelevantVars | Agda.TypeChecking.Irrelevance |
| wakeupConstraints | Agda.TypeChecking.Constraints |
| wakeupConstraints_ | Agda.TypeChecking.Constraints |
| wakeupListener | Agda.TypeChecking.MetaVars |
| Warnings | |
| 1 (Type/Class) | Agda.TypeChecking.Errors |
| 2 (Data Constructor) | Agda.TypeChecking.Errors |
| warningsToError | Agda.TypeChecking.Errors |
| warshall | Agda.Utils.Warshall |
| warshallG | Agda.Utils.Warshall |
| Weak | Agda.Auto.Syntax |
| weak | Agda.Auto.Syntax |
| weakarglist | Agda.Auto.Syntax |
| weakelr | Agda.Auto.Syntax |
| weaken | Agda.Auto.Convert |
| weakens | Agda.Auto.Convert |
| weaki | Agda.Auto.Syntax |
| 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 |
| wfParentPats | 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 |
| when | Agda.Utils.Monad |
| whenConstraints | Agda.TypeChecking.Constraints |
| whenFail | Agda.Utils.QuickCheck |
| whenFail' | Agda.Utils.QuickCheck |
| 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 |
| when_ | Agda.Utils.Monad |
| WhereClause | Agda.Syntax.Concrete |
| WhereClause' | Agda.Syntax.Concrete |
| whileLeft | Agda.Utils.Either |
| WhyInScope | Agda.Syntax.Scope.Base |
| whyInScope | |
| 1 (Function) | Agda.Interaction.BasicOps |
| 2 (Function) | Agda.Interaction.InteractionTop |
| WildMP | Agda.TypeChecking.Coverage.Match |
| 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 |
| 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 |
| WithArity | |
| 1 (Type/Class) | Agda.TypeChecking.CompiledClause |
| 2 (Data Constructor) | Agda.TypeChecking.CompiledClause |
| WithClausePatternMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WithColors | Agda.Syntax.Concrete |
| withConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| withContextPrecedence | Agda.Syntax.Scope.Monad |
| withCurrentFile | |
| 1 (Function) | Agda.Interaction.CommandLine |
| 2 (Function) | Agda.Interaction.InteractionTop |
| withCurrentModule | |
| 1 (Function) | Agda.Syntax.Scope.Monad |
| 2 (Function) | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| withCurrentModule' | Agda.Syntax.Scope.Monad |
| withDisplayForm | Agda.TypeChecking.With |
| withEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| WithExpr | Agda.Syntax.Concrete |
| withExtendedOccEnv | Agda.TypeChecking.Positivity |
| withFreezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| 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 |
| withImportPath | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| within | Agda.Utils.QuickCheck |
| withIncreasedModuleNestingLevel | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| 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 |
| withMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| 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 |
| WithoutKError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WithoutKException | Agda.TypeChecking.Rules.LHS.Unify |
| withRangeOf | Agda.Syntax.Position |
| withRangesOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| withRangesOfQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| WithRHS | Agda.Syntax.Abstract |
| withScope | |
| 1 (Function) | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Syntax.Translation.AbstractToConcrete |
| withScope_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| withShowAllArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| withSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| withTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| withUsableVars | Agda.Termination.Monad |
| Wk | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| wkS | Agda.TypeChecking.Substitute |
| wordBoundary | Agda.Compiler.JS.Parser |
| wordBounded | Agda.Interaction.Highlighting.Vim |
| wordsBy | Agda.Utils.List |
| workOnTypes | Agda.TypeChecking.Irrelevance |
| workOnTypes' | Agda.TypeChecking.Irrelevance |
| Wrap | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Pretty |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Pretty |
| writeFile | Agda.Utils.IO.UTF8 |
| writeInterface | Agda.Interaction.Imports |
| writeIORef | Agda.Utils.IORef |
| writeModule | |
| 1 (Function) | Agda.Compiler.JS.Compiler |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| WrongContentPostulateBlock | Agda.Syntax.Concrete.Definitions |
| WrongDefinition | Agda.Syntax.Concrete.Definitions |
| WrongHidingInApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongHidingInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongHidingInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongIrrelevanceInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongNamedArgument | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongNumberOfConstructorArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongParameters | Agda.Syntax.Concrete.Definitions |
| WSM | Agda.Syntax.Scope.Monad |