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 |