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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- $
- %
- +
- .
- /
- <
- =
- >
- ^
- -
- _
- All

Index - A

A | Agda.Interaction.EmacsCommand
aArity | Agda.Syntax.Treeless, Agda.Compiler.Backend
aBody | Agda.Syntax.Treeless, Agda.Compiler.Backend
Abort | Agda.TypeChecking.Injectivity
abort |
1 (Function) | Agda.TypeChecking.MetaVars.Occurs
2 (Function) | Agda.Interaction.InteractionTop
above | Agda.Utils.IntSet.Infinite
Abs |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
3 (Type/Class) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Reflected
5 (Type/Class) | Agda.Syntax.Internal
6 (Data Constructor) | Agda.Syntax.Internal
absApp | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
absBody | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
abslamvarname | Agda.Auto.Convert
AbsModule | Agda.Syntax.Scope.Base
AbsName | Agda.Syntax.Scope.Base
absName | Agda.Syntax.Internal
absolute | Agda.Utils.FileName
AbsolutePath |
1 (Type/Class) | Agda.Utils.FileName
2 (Data Constructor) | Agda.Utils.FileName
absPathD | Agda.TypeChecking.Serialise.Base
abspatvarname | Agda.Auto.CaseSplit
AbsTerm | Agda.TypeChecking.Abstract
absTerm | Agda.TypeChecking.Abstract
AbsToCon | Agda.Syntax.Translation.AbstractToConcrete
Abstract |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
abstract | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
abstractArgs | Agda.TypeChecking.Substitute
AbstractConstructorNotInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbstractDef | Agda.Syntax.Common
AbstractDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbstractMode |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbstractModule | Agda.Syntax.Scope.Base
AbstractName | Agda.Syntax.Scope.Base
AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract
abstractTerm | Agda.TypeChecking.Abstract
abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteHiding | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteScope | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete
abstractType | Agda.TypeChecking.Abstract
Absurd |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem
absurd | Agda.Utils.Empty
absurdBody | Agda.Syntax.Internal
AbsurdClause | Agda.Syntax.Reflected
AbsurdLam |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
AbsurdLambda | Agda.Auto.Syntax
absurdLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbsurdMatch | Agda.Syntax.Internal
AbsurdP |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
absurdP | Agda.Syntax.Internal
AbsurdPattern | Agda.TypeChecking.Rules.LHS.Problem
absurdPatternName | Agda.Syntax.Internal
AbsurdPatternRequiresNoRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbsurdPatternRequiresNoRHS_ | Agda.Interaction.Options.Warnings
AbsurdRHS |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
acceptableFileExts | Agda.Syntax.Parser
Access | Agda.Syntax.Common
Account |
1 (Type/Class) | Agda.Utils.Benchmark
2 (Type/Class) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
aCon | Agda.Syntax.Treeless, Agda.Compiler.Backend
Action |
1 (Type/Class) | Agda.TypeChecking.CheckInternal
2 (Data Constructor) | Agda.TypeChecking.CheckInternal
activateLoadedFileCache | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
actOnMeta | Agda.Interaction.CommandLine
acyclic | Agda.Utils.Graph.AdjacencyMap.Unidirectional
add |
1 (Function) | Agda.Termination.Semiring
2 (Function) | Agda.Termination.SparseMatrix
addAwakeConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addblk | Agda.Auto.Typecheck
addClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addCoercions | Agda.Compiler.MAlonzo.Coerce
addColumn | Agda.Termination.SparseMatrix
addCompilerPragma | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addCompositionForRecord | Agda.TypeChecking.Rules.Record
addConnection | Agda.Interaction.Highlighting.Dot
addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addConstraint |
1 (Function) | Agda.Utils.Warshall
2 (Function) | Agda.TypeChecking.Constraints
addConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addConstraintTo | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AddContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addCPUTime | Agda.Utils.Benchmark
addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addCtxTel | Agda.TypeChecking.Reduce.Monad
addDataCons | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addDefaultLibraries | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addEdge |
1 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Function) | Agda.Utils.Warshall
addend | Agda.Auto.Typecheck
AddExtraRef | Agda.Auto.NarrowingSearch
addFinalNewLine | Agda.Utils.String
addFlex | Agda.Utils.Warshall
addForeignCode | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addImport | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addImportCycleCheck | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addImportedInstances | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addImportedThings | Agda.Interaction.Imports
addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addLetBinding' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addModule | Agda.Interaction.Highlighting.Dot
addModuleToScope | Agda.Syntax.Scope.Base
addNamedInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addNamesToScope | Agda.Syntax.Scope.Base
addNameToScope | Agda.Syntax.Scope.Base
addNode | Agda.Utils.Warshall
addPragma | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addRecordNameContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addRewriteRule | Agda.TypeChecking.Rewriting
addRewriteRules | Agda.TypeChecking.Rewriting
addRewriteRulesFor | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addRow | Agda.Termination.SparseMatrix
addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addSuffix | Agda.Utils.Suffix
addtrailingargs | Agda.Auto.Syntax
addTypedInstance | Agda.TypeChecking.Telescope
addUnknownInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addVarToBind | Agda.Syntax.Scope.Monad
ADef | Agda.TypeChecking.Positivity
aDefToMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AdjList | Agda.Utils.Warshall
adjust |
1 (Function) | Agda.Utils.HashMap
2 (Function) | Agda.Utils.Trie
AffineHole | Agda.Utils.AffineHole
AgdaFileType | Agda.Syntax.Common
AgdaLib | Agda.Interaction.Library.Base
AgdaLibFile | Agda.Interaction.Library.Base
agdaTermType | Agda.TypeChecking.Unquote
agdaTypeType | Agda.TypeChecking.Unquote
aGuard | Agda.Syntax.Treeless, Agda.Compiler.Backend
AHMModule | Agda.Auto.Options
AHMNone | Agda.Auto.Options
ALConPar | Agda.Auto.Syntax
ALCons | Agda.Auto.Syntax
AlexEOF | Agda.Syntax.Parser.Lexer
AlexError | Agda.Syntax.Parser.Lexer
alexGetByte | Agda.Syntax.Parser.Alex
alexGetChar | Agda.Syntax.Parser.Alex
AlexInput |
1 (Type/Class) | Agda.Syntax.Parser.Alex
2 (Data Constructor) | Agda.Syntax.Parser.Alex
alexInputPrevChar | Agda.Syntax.Parser.Alex
AlexReturn | Agda.Syntax.Parser.Lexer
alexScanUser | Agda.Syntax.Parser.Lexer
AlexSkip | Agda.Syntax.Parser.Lexer
AlexToken | Agda.Syntax.Parser.Lexer
align | Agda.Utils.Pretty
aLit | Agda.Syntax.Treeless, Agda.Compiler.Backend
All |
1 (Type/Class) | Agda.Utils.IndexedList
2 (Type/Class) | Agda.Utils.TypeLevel
allApplyElims | Agda.Syntax.Internal
allEqual | Agda.Utils.List
allFlexVars | Agda.TypeChecking.Rules.LHS.Problem
allFreeVars | Agda.TypeChecking.Free
allFreeVarsWithOcc | Agda.TypeChecking.Free
allHelpTopics | Agda.Interaction.Options.Help
allIndices | Agda.Utils.IndexedList
allJustM | Agda.Utils.Maybe
allKindsOfNames | Agda.Syntax.Scope.Base
allLeft | Agda.Utils.Either
allM | Agda.Utils.Monad
allMetaKinds | Agda.TypeChecking.MetaVars
allMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
allMetasList | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AllNames | Agda.Syntax.Abstract
allNames | Agda.Syntax.Abstract
allNamesInScope | Agda.Syntax.Scope.Base
allNamesInScope' | Agda.Syntax.Scope.Base
allNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
allowAllReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AllowAmbiguousNames | Agda.Syntax.Scope.Base
AllowedReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AllowedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
allowedVar | Agda.TypeChecking.MetaVars.Occurs
allowNonTerminatingReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
allProjElims | Agda.Syntax.Internal
allReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
allRelevances | Agda.Syntax.Common
allRelevantVars | Agda.TypeChecking.Free
allRelevantVarsIgnoring | Agda.TypeChecking.Free
allRight | Agda.Utils.Either
allThingsInScope | Agda.Syntax.Scope.Base
allVars |
1 (Function) | Agda.TypeChecking.Free
2 (Function) | Agda.TypeChecking.Free.Old
AllWarnings | Agda.TypeChecking.Warnings
allWarnings | Agda.Interaction.Options.Warnings
allWithKey | Agda.Utils.Map
ALNil | Agda.Auto.Syntax
ALProj | Agda.Auto.Syntax
alreadyVisited | Agda.Interaction.Imports
Alt |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
alt | Agda.Compiler.MAlonzo.Compiler
alter | Agda.Utils.HashMap
alterF | Agda.Utils.HashMap
altM1 | Agda.Utils.Monad
Ambiguous | Agda.Interaction.FindFile
AmbiguousAnything | Agda.Syntax.Scope.Base
AmbiguousConProjs | Agda.Syntax.Scope.Base
AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions
AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousNothing | Agda.Syntax.Scope.Base
AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
aModeToDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
amodLineage | Agda.Syntax.Scope.Base
amodName | Agda.Syntax.Scope.Base
anameKind | Agda.Syntax.Scope.Base
anameLineage | Agda.Syntax.Scope.Base
anameMetadata | Agda.Syntax.Scope.Base
anameName | Agda.Syntax.Scope.Base
AnArg | Agda.TypeChecking.Positivity
And | Agda.Auto.NarrowingSearch
and2M | Agda.Utils.Monad
andM | Agda.Utils.Monad
annotate | Agda.Utils.Parser.MemoisedCPS
antiUnify | Agda.TypeChecking.Conversion
antiUnifyElims | Agda.TypeChecking.Conversion
antiUnifyType | Agda.TypeChecking.Conversion
AnyAbstract | Agda.Syntax.Abstract
anyAbstract | Agda.Syntax.Abstract
anyDefs | Agda.Termination.RecCheck
anyM | Agda.Utils.Monad
AnyWhere | Agda.Syntax.Concrete
aoHintMode | Agda.Auto.Options
aoHints | Agda.Auto.Options
aoMode | Agda.Auto.Options
aoPick | Agda.Auto.Options
aoTimeOut | Agda.Auto.Options
APatName | Agda.Syntax.Translation.ConcreteToAbstract
APatternLike | Agda.Syntax.Abstract.Pattern
App |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
3 (Data Constructor) | Agda.Syntax.Concrete
4 (Data Constructor) | Agda.Syntax.Abstract
5 (Data Constructor) | Agda.TypeChecking.EtaContract
app | Agda.Syntax.Abstract
appBrackets | Agda.Syntax.Fixity
appBrackets' | Agda.Syntax.Fixity
appDef | Agda.TypeChecking.Reduce
appDef' | Agda.TypeChecking.Reduce
appDefE | Agda.TypeChecking.Reduce
appDefE' | Agda.TypeChecking.Reduce
appDefE_ | Agda.TypeChecking.Reduce
appDef_ | Agda.TypeChecking.Reduce
appElims | Agda.Auto.Syntax
appendArgNames | Agda.Syntax.Internal
appHead | Agda.Auto.Syntax
AppInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
appInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AppK | Agda.Syntax.Concrete.Operators.Parser.Monad
Application | Agda.Syntax.Abstract.Views
Applied | Agda.Syntax.Scope.Base
Apply |
1 (Data Constructor) | Agda.Compiler.JS.Syntax
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Internal
4 (Type/Class) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
5 (Data Constructor) | Agda.Syntax.Abstract
6 (Type/Class) | Agda.Utils.TypeLevel
apply |
1 (Function) | Agda.Compiler.JS.Substitution
2 (Function) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
apply1 | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyE | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyFlagsToMaybeWarnings | Agda.Interaction.Imports
applyFlagsToTCWarnings | Agda.TypeChecking.Errors
applyFlagsToTCWarnings' | Agda.TypeChecking.Errors
applyImportDirective | Agda.Syntax.Scope.Base
applyImportDirectiveM | Agda.Syntax.Scope.Monad
applyModality | Agda.Syntax.Common
applyModalityToContext | Agda.TypeChecking.Irrelevance
applyModalityToContextFunBody | Agda.TypeChecking.Irrelevance
applyModalityToContextOnly | Agda.TypeChecking.Irrelevance
applyModalityToJudgementOnly | Agda.TypeChecking.Irrelevance
applyNLPatSubst | Agda.TypeChecking.Substitute
ApplyOrIApply | Agda.TypeChecking.Coverage.Match
applyPatSubst | Agda.TypeChecking.Substitute
applyperm | Agda.Auto.CaseSplit
applyQuantity | Agda.Syntax.Common
applyQuantityToContext | Agda.TypeChecking.Irrelevance
applyQuantityToContextOnly | Agda.TypeChecking.Irrelevance
applyQuantityToJudgementOnly | Agda.TypeChecking.Irrelevance
applyRelevance | Agda.Syntax.Common
applyRelevanceToContext | Agda.TypeChecking.Irrelevance
applyRelevanceToContextFunBody | Agda.TypeChecking.Irrelevance
applyRelevanceToContextOnly | Agda.TypeChecking.Irrelevance
applyRelevanceToJudgementOnly | Agda.TypeChecking.Irrelevance
applys | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applySection' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applySplitPSubst | Agda.TypeChecking.Coverage.Match
applySubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyUnless | Agda.Utils.Function
applyUnlessM | Agda.Utils.Function
applyWarningMode | Agda.TypeChecking.Warnings
applyWhen | Agda.Utils.Function
applyWhenM | Agda.Utils.Function
applyWhenVerboseS | Agda.TypeChecking.Reduce.Monad
appOK | Agda.Auto.Syntax
appOrigin | Agda.Syntax.Info
AppP | Agda.Syntax.Concrete
appP | Agda.Syntax.Concrete.Operators.Parser
appParens | Agda.Syntax.Info
appRange | Agda.Syntax.Info
appUId | Agda.Auto.Syntax
AppV | Agda.Syntax.Concrete.Operators.Parser
AppView |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract.Views
appView |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Views
AppView' | Agda.Syntax.Abstract.Views
appView' | Agda.Syntax.Abstract.Views
apReduce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
apTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Arc | Agda.Utils.Warshall
areWeCaching | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Arg |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
ArgDescr | Agda.Interaction.Options
argFromDom | Agda.Syntax.Common
argH | Agda.TypeChecking.Primitive
ArgInfo |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
argInfo | Agda.Syntax.Common
argInfoFreeVariables | Agda.Syntax.Common
argInfoHiding | Agda.Syntax.Common
argInfoModality | Agda.Syntax.Common
argInfoOrigin | Agda.Syntax.Common
ArgList | Agda.Auto.Syntax
argN | Agda.TypeChecking.Primitive
ArgName | Agda.Syntax.Internal
argNameToString | Agda.Syntax.Internal
ArgNode | Agda.TypeChecking.Positivity
Args |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Type/Class) | Agda.Syntax.Reflected
3 (Type/Class) | Agda.Syntax.Internal
4 (Type/Class) | Agda.Syntax.Abstract
argsFromElims | Agda.Syntax.Internal
argsP | Agda.Syntax.Concrete.Operators.Parser
argsToElims | Agda.Syntax.Reflected
ArgT | Agda.TypeChecking.Records
argToDontCare | Agda.TypeChecking.Substitute
Argument | Agda.Interaction.Highlighting.Precise
ArgumentCtx | Agda.Syntax.Fixity
argumentCtx_ | Agda.Syntax.Fixity
ArgumentIndex | Agda.Termination.CallMatrix
Arity | Agda.Syntax.Common
arity |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.TypeChecking.CompiledClause
arrow | Agda.Syntax.Concrete.Pretty
Arrows | Agda.Utils.TypeLevel
As | Agda.Syntax.Concrete
AsB | Agda.TypeChecking.Rules.LHS.Problem
AsBinding | Agda.TypeChecking.Rules.LHS.Problem
AsciiOnly | Agda.Interaction.Options.IORefs
AsIs | Agda.Interaction.BasicOps
askName | Agda.Syntax.Translation.ReflectedToAbstract
askR | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend
asksTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
askTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AsName |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
asName | Agda.Syntax.Concrete
AsName' | Agda.Syntax.Concrete
AsP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Aspect | Agda.Interaction.Highlighting.Precise
aspect | Agda.Interaction.Highlighting.Precise
Aspects |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
asRange | Agda.Syntax.Concrete
assertCurrentModule | Agda.TypeChecking.Rules.Decl
Assign |
1 (Type/Class) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Interaction.BasicOps
assign | Agda.TypeChecking.MetaVars
assignE | Agda.TypeChecking.Conversion
Assignments | Agda.Auto.CaseSplit
assignMeta | Agda.TypeChecking.MetaVars
assignMeta' | Agda.TypeChecking.MetaVars
Assigns | Agda.Syntax.Abstract
assignTerm | Agda.TypeChecking.MetaVars
assignTerm' | Agda.TypeChecking.MetaVars
assignV | Agda.TypeChecking.MetaVars
assignWrapper | Agda.TypeChecking.MetaVars
Associativity | Agda.Syntax.Fixity
AssocList | Agda.Utils.AssocList
asView | Agda.Syntax.Abstract.Views
atClause | Agda.TypeChecking.Rules.Def
atLeastTwoParts | Agda.Syntax.Concrete.Operators.Parser
atomicModifyIORef | Agda.Utils.IORef
atomicModifyIORef' | Agda.Utils.IORef
atomicWriteIORef | Agda.Utils.IORef
atomizeLayers | Agda.Syntax.Parser.Literate
atomP |
1 (Function) | Agda.Utils.Parser.MemoisedCPS
2 (Function) | Agda.Syntax.Concrete.Operators.Parser
atTopLevel | Agda.Interaction.BasicOps
Attribute | Agda.Syntax.Concrete.Attribute
attributesMap | Agda.Syntax.Concrete.Attribute
augCallInfo | Agda.Termination.CallMatrix
augCallMatrix | Agda.Termination.CallMatrix
auto | Agda.Auto.Auto
AutoHintMode | Agda.Auto.Options
autoHintMode | Agda.Auto.Options
autoHints | Agda.Auto.Options
autoInline | Agda.TypeChecking.Inlining
autoMessage | Agda.Auto.Auto
autoMode | Agda.Auto.Options
AutoOptions |
1 (Type/Class) | Agda.Auto.Options
2 (Data Constructor) | Agda.Auto.Options
autoPick | Agda.Auto.Options
AutoProgress | Agda.Auto.Auto
autoProgress | Agda.Auto.Auto
AutoResult |
1 (Type/Class) | Agda.Auto.Auto
2 (Data Constructor) | Agda.Auto.Auto
autoTimeOut | Agda.Auto.Options
AutoToken | Agda.Auto.Options
autoTokens | Agda.Auto.Options
AwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Axiom |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.Syntax.Concrete.Definitions
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
axiomName | Agda.Syntax.Abstract