Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant

Index - V

VAgda.Compiler.MAlonzo.Misc
ValidOffsetAgda.TypeChecking.SizedTypes.Syntax
validOffsetAgda.TypeChecking.SizedTypes.Syntax
VALUAgda.TypeChecking.Serialise.Base
Value 
1 (Data Constructor)Agda.Utils.WithDefault
2 (Type/Class)Agda.Interaction.JSON
valueAgda.TypeChecking.Serialise.Base
valueArgsAgda.TypeChecking.Serialise.Base
valueAtAgda.Utils.Trie
ValueCmpAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ValueCmpOnFaceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
valueNAgda.TypeChecking.Serialise.Base
valuNAgda.TypeChecking.Serialise.Base
valuN'Agda.TypeChecking.Serialise.Base
Var 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Auto.Syntax
3 (Data Constructor)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Reflected
5 (Data Constructor)Agda.Syntax.Abstract
varAgda.Syntax.Internal
VarArgAgda.TypeChecking.Positivity.Occurrence
VarCounts 
1 (Type/Class)Agda.TypeChecking.Free
2 (Data Constructor)Agda.TypeChecking.Free
varCountsAgda.TypeChecking.Free
varDependenciesAgda.TypeChecking.Telescope
varDependentsAgda.TypeChecking.Telescope
varFlexRigAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
VarHeadAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
VariableAgda.TypeChecking.Free.Lazy
variableAgda.TypeChecking.Free.Lazy
variableCheckAgda.TypeChecking.MetaVars.Occurs
VariableIsErasedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
VariableIsIrrelevantAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
VariableIsOfUnusableCohesionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
VariableKindAgda.Compiler.MAlonzo.Misc
variableNameAgda.Compiler.JS.Pretty
VarKAgda.Compiler.MAlonzo.Misc
varMAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
VarMap 
1 (Type/Class)Agda.TypeChecking.Free.Lazy
2 (Data Constructor)Agda.TypeChecking.Free.Lazy
VarMap'Agda.TypeChecking.Free.Lazy
varModalityAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
VarNameAgda.Syntax.Scope.Base
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
varOccurrenceInAgda.TypeChecking.Free
VarP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Reflected
3 (Data Constructor)Agda.Syntax.Abstract
varPAgda.Syntax.Internal
VarsAgda.Syntax.Translation.ReflectedToAbstract
varsAgda.TypeChecking.Positivity
VarSetAgda.Utils.VarSet
varSortAgda.Syntax.Internal
vcaseAgda.TypeChecking.Serialise.Base
vcat 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
verboseBracketAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
VerboseKeyAgda.Interaction.Options, Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
VerboseLevelAgda.Interaction.Options, Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
verboseSAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
VerbosityAgda.Interaction.Options, Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
verbosityAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
verifyBuiltinRewriteAgda.TypeChecking.Rewriting
verifyImportDirectiveAgda.Syntax.Scope.Monad
verifySolutionAgda.TypeChecking.SizedTypes.WarshallSolver
versionAgda.Version
VersionView 
1 (Type/Class)Agda.Interaction.Library
2 (Data Constructor)Agda.Interaction.Library
versionViewAgda.Interaction.Library
versionWithCommitInfoAgda.VersionCommit
viewAgda.Utils.Lens
viewProjectedVarAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
viewTCAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
vimFileAgda.Interaction.Highlighting.Vim
vineAgda.Compiler.JS.Substitution
visibleAgda.Syntax.Common
VisitedModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
visitModuleAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
visitorNameAgda.Compiler.JS.Compiler
vsepAgda.Compiler.JS.Pretty
vvBaseAgda.Interaction.Library
vvNumbersAgda.Interaction.Library