| 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 | Agda.TypeChecking.Free |
| weaklyRigidVars | Agda.TypeChecking.Free |
| Weight | Agda.Utils.Warshall |
| wellFormedIndices | Agda.TypeChecking.Rules.LHS.Split |
| whatInduction | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| whenConstraints | Agda.TypeChecking.Constraints |
| whenFail | Agda.Utils.QuickCheck |
| whenFail' | Agda.Utils.QuickCheck |
| whenJust | Agda.Utils.Monad |
| whenJustM | Agda.Utils.Monad |
| whenM | Agda.Utils.Monad |
| when_ | Agda.Utils.Monad |
| WhereClause | Agda.Syntax.Concrete |
| WildMP | Agda.TypeChecking.Coverage.Match |
| WildP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| WildV | Agda.Syntax.Concrete.Operators.Parser |
| 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 |
| withConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| withContextPrecedence | Agda.Syntax.Scope.Monad |
| withCurrentModule | |
| 1 (Function) | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Syntax.Scope.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 |
| withFresh | Agda.Utils.Fresh |
| WithFunction | Agda.TypeChecking.Rules.Def |
| WithFunctionProblem | Agda.TypeChecking.Rules.Def |
| withFunctionType | Agda.TypeChecking.With |
| WithFunCtx | Agda.Syntax.Fixity |
| 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 |
| withRangeOf | Agda.Syntax.Position |
| withRangesOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| withRangesOfQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract |
| 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.Signature, Agda.TypeChecking.Monad |
| withTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| withTypesFrom | Agda.TypeChecking.Rules.LHS.Split |
| Wk | Agda.TypeChecking.Substitute |
| wkS | Agda.TypeChecking.Substitute |
| wordBoundary | Agda.Compiler.JS.Parser |
| 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 |
| writeModule | |
| 1 (Function) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Function) | Agda.Compiler.JS.Compiler |
| 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 |
| WrongNumberOfConstructorArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongParameters | Agda.Syntax.Concrete.Definitions |
| WSM | Agda.Syntax.Scope.Monad |