| V | Agda.Compiler.MAlonzo.Misc |
| ValidOffset | Agda.TypeChecking.SizedTypes.Syntax |
| validOffset | Agda.TypeChecking.SizedTypes.Syntax |
| validProfileOptionStrings | Agda.Utils.ProfileOptions |
| VALU | Agda.TypeChecking.Serialise.Base |
| Value | |
| 1 (Data Constructor) | Agda.Utils.WithDefault |
| 2 (Type/Class) | Agda.Interaction.JSON |
| value | Agda.TypeChecking.Serialise.Base |
| valueArgs | Agda.TypeChecking.Serialise.Base |
| valueAt | Agda.Utils.Trie |
| ValueCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ValueCmpOnFace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| valueN | Agda.TypeChecking.Serialise.Base |
| valuN | Agda.TypeChecking.Serialise.Base |
| valuN' | Agda.TypeChecking.Serialise.Base |
| Var | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Reflected |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| 5 (Type/Class) | Agda.TypeChecking.Names |
| var | Agda.Syntax.Internal |
| VarArg | Agda.TypeChecking.Positivity.Occurrence |
| varCount | Agda.TypeChecking.Rules.LHS.Unify.Types |
| VarCounts | |
| 1 (Type/Class) | Agda.TypeChecking.Free |
| 2 (Data Constructor) | Agda.TypeChecking.Free |
| varCounts | Agda.TypeChecking.Free |
| varDependencies | Agda.TypeChecking.Telescope |
| varDependents | Agda.TypeChecking.Telescope |
| varFlexRig | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| VarHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Variable | Agda.TypeChecking.Free.Lazy |
| variable | Agda.TypeChecking.Free.Lazy |
| variableCheck | Agda.TypeChecking.MetaVars.Occurs |
| VariableIsErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| VariableIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| VariableIsOfUnusableCohesion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| VariableKind | Agda.Compiler.MAlonzo.Misc |
| variableName | Agda.Compiler.JS.Pretty |
| VariablesBoundMoreThanOnce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| VariablesNotBoundByLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| VarK | Agda.Compiler.MAlonzo.Misc |
| varM | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| VarMap | |
| 1 (Type/Class) | Agda.TypeChecking.Free.Lazy |
| 2 (Data Constructor) | Agda.TypeChecking.Free.Lazy |
| VarMap' | Agda.TypeChecking.Free.Lazy |
| varModality | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| VarName | Agda.Syntax.Scope.Base |
| varNumber | Agda.Syntax.Common |
| VarOcc | |
| 1 (Type/Class) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| 2 (Data Constructor) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| VarOcc' | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| varOccurrenceIn | Agda.TypeChecking.Free |
| VarP | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| varP | Agda.Syntax.Internal |
| VarPart | Agda.Syntax.Common |
| Vars | |
| 1 (Type/Class) | Agda.Syntax.Translation.ReflectedToAbstract |
| 2 (Type/Class) | Agda.TypeChecking.Names |
| vars | Agda.TypeChecking.Positivity |
| Vars1 | Agda.TypeChecking.Names |
| VarSet | Agda.Utils.VarSet |
| varSort | Agda.Syntax.Internal |
| varTel | Agda.TypeChecking.Rules.LHS.Unify.Types |
| vcase | Agda.TypeChecking.Serialise.Base |
| vcat | |
| 1 (Function) | Agda.Syntax.Common.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| 3 (Function) | Agda.TypeChecking.Pretty |
| Verbalize | Agda.TypeChecking.Errors |
| verbalize | Agda.TypeChecking.Errors |
| verboseBracket | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| VerboseKey | Agda.Interaction.Options, Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| VerboseLevel | Agda.Interaction.Options, Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| verboseS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Verbosity | Agda.Interaction.Options, Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| verifyBuiltinRewrite | Agda.TypeChecking.Rewriting |
| verifyImportDirective | Agda.Syntax.Scope.Monad |
| verifySolution | Agda.TypeChecking.SizedTypes.WarshallSolver |
| version | Agda.Version |
| VersionView | |
| 1 (Type/Class) | Agda.Interaction.Library |
| 2 (Data Constructor) | Agda.Interaction.Library |
| versionView | Agda.Interaction.Library |
| versionWithCommitInfo | Agda.VersionCommit |
| view | Agda.Utils.Lens |
| viewProjectedVar | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| viewTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| vimFile | Agda.Interaction.Highlighting.Vim |
| vine | Agda.Compiler.JS.Substitution |
| visible | Agda.Syntax.Common |
| VisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| visitModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| visitorName | Agda.Compiler.JS.Compiler |
| vsep | |
| 1 (Function) | Agda.Syntax.Common.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| 3 (Function) | Agda.TypeChecking.Pretty |
| vvBase | Agda.Interaction.Library |
| vvNumbers | Agda.Interaction.Library |