Agda-2.6.2.2: 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 |
1 (Data Constructor) | Agda.Interaction.EmacsCommand
2 (Data Constructor) | Agda.Compiler.MAlonzo.Misc
aArity | Agda.Syntax.Treeless, Agda.Compiler.Backend
aBody | Agda.Syntax.Treeless, Agda.Compiler.Backend
abort |
1 (Function) | Agda.Interaction.Base
2 (Function) | Agda.TypeChecking.MetaVars.Occurs
abortIfBlocked | Agda.TypeChecking.Reduce
Above | Agda.Compiler.JS.Pretty
above | Agda.Utils.IntSet.Infinite
Abs |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
3 (Type/Class) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Internal
5 (Type/Class) | Agda.Syntax.Reflected
6 (Data Constructor) | Agda.Syntax.Reflected
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
AbsNameWithFixity |
1 (Type/Class) | Agda.TypeChecking.Serialise.Instances.Abstract
2 (Data Constructor) | Agda.TypeChecking.Serialise.Instances.Abstract
AbsOfCon | Agda.Syntax.Translation.ConcreteToAbstract
AbsOfRef | Agda.Syntax.Translation.ReflectedToAbstract
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.Compiler.Backend, Agda.TypeChecking.Monad
AbstractDef | Agda.Syntax.Common
AbstractDefn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AbstractMode |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
AbsurdMatch | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
AbsurdP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Reflected
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.Compiler.Backend, Agda.TypeChecking.Monad
AbsurdPatternRequiresNoRHS_ | Agda.Interaction.Options.Warnings
absurdPatterns | Agda.TypeChecking.Rules.LHS.Problem
AbsurdRHS |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
acceptableFileExts | Agda.Syntax.Parser
Access | Agda.Syntax.Common
acConstraints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Account |
1 (Type/Class) | Agda.Utils.Benchmark
2 (Type/Class) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
acData | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
acElims | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
aCon | Agda.Syntax.Treeless, Agda.Compiler.Backend
acRanges | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ACState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Action |
1 (Type/Class) | Agda.TypeChecking.CheckInternal
2 (Data Constructor) | Agda.TypeChecking.CheckInternal
activateLoadedFileCache | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
activeBackend | Agda.Compiler.Backend
activeBackendMayEraseType | Agda.Compiler.Backend
acType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
acyclic | Agda.Utils.Graph.AdjacencyMap.Unidirectional
add |
1 (Function) | Agda.Termination.Semiring
2 (Function) | Agda.Termination.SparseMatrix
addAndUnblocker | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addAwakeConstraint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addAwakeConstraint' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addblk | Agda.Auto.Typecheck
addClauses | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addCoercions | Agda.Compiler.MAlonzo.Coerce
addCohesion | Agda.Syntax.Common
addColumn | Agda.Termination.SparseMatrix
addCompilerPragma | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addCompositionForRecord | Agda.TypeChecking.Rules.Record
addConstant | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addConstant' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addConstraint |
1 (Function) | Agda.Utils.Warshall
2 (Function) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addConstraint' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addConstraintTCM | Agda.TypeChecking.Constraints
addConstraintTo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
AddContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addCPUTime | Agda.Utils.Benchmark
addCtx | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addDataCons | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addDefaultLibraries | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addDisplayForm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addDisplayForms | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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
addFlexRig | Agda.TypeChecking.Free.Lazy
addForeignCode | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addImport | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
addImportCycleCheck | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
addImportedInstances | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addLetBinding | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addLetBinding' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addLoneSig | Agda.Syntax.Concrete.Definitions.Monad
addModality | Agda.Syntax.Common
addModuleToScope | Agda.Syntax.Scope.Base
addNamedInstance | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addNameToScope | Agda.Syntax.Scope.Base
addNode | Agda.Utils.Warshall
addOrUnblocker | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addPragma | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addQuantity | Agda.Syntax.Common
addRecordNameContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addRelevance | Agda.Syntax.Common
addRewriteRules | Agda.TypeChecking.Rewriting
addRewriteRulesFor | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addRow | Agda.Termination.SparseMatrix
addSection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addSuffix | Agda.Utils.Suffix
addtrailingargs | Agda.Auto.Syntax
addTrustedExecutables | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addTypedInstance | Agda.TypeChecking.Telescope
addTypedPatterns | Agda.TypeChecking.Rules.Term
addUniqueInts | Agda.Utils.Graph.AdjacencyMap.Unidirectional
addUnknownInstance | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addVarToBind | Agda.Syntax.Scope.Monad
addWarning | Agda.TypeChecking.Warnings
ADef | Agda.TypeChecking.Positivity
aDefToMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AdjList | Agda.Utils.Warshall
adjust |
1 (Function) | Agda.Utils.Trie
2 (Function) | Agda.Utils.BiMap
adjustM | Agda.Utils.Map
adjustM' | Agda.Utils.Map
adjustPrecondition | Agda.Utils.BiMap
ADotT | Agda.Syntax.Abstract.Pattern
AffineHole | Agda.Utils.AffineHole
AgdaError | Agda.Interaction.ExitCode
agdaErrorFromInt | Agda.Interaction.ExitCode
agdaErrorToInt | Agda.Interaction.ExitCode
AgdaFileType | Agda.Syntax.Common
AgdaLibFile |
1 (Type/Class) | Agda.Interaction.Library.Base, Agda.Interaction.Library
2 (Data Constructor) | Agda.Interaction.Library.Base, Agda.Interaction.Library
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.Elim, Agda.Syntax.Internal
allBlockingMetas | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
allBlockingProblems | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
allCohesions | Agda.Syntax.Common
allDuplicates | Agda.Utils.List
allEqual |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.List1
allFlexVars | Agda.TypeChecking.Rules.LHS.Problem
allFreeVars | Agda.TypeChecking.Free
allHelpTopics | Agda.Interaction.Options.Help
allIndices | Agda.Utils.IndexedList
allJustM | Agda.Utils.Maybe
AllKindsOfNames | Agda.Syntax.Scope.Base
allKindsOfNames | Agda.Syntax.Scope.Base
allLeft | Agda.Utils.Either
allListT | Agda.Utils.ListT
allM | Agda.Utils.Monad
allMetaKinds | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
AllMetas | Agda.Syntax.Internal.MetaVars
allMetas | Agda.Syntax.Internal.MetaVars
allMetas' | Agda.Syntax.Internal.MetaVars
allMetasList | Agda.Syntax.Internal.MetaVars
allNamesInScope | Agda.Syntax.Scope.Base
allNamesInScope' | Agda.Syntax.Scope.Base
allNameSpaces | Agda.Syntax.Scope.Base
allNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
allNullaryToStringTag | Agda.Interaction.JSON
allowAllReductions | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
AllowAmbiguousNames | Agda.Syntax.Scope.Base
AllowedReduction | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AllowedReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AllowedVar | Agda.TypeChecking.MetaVars.Occurs
allowedVars | Agda.TypeChecking.MetaVars.Occurs
allowNonTerminatingReductions | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
allProjElims | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
allReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
allRelevances | Agda.Syntax.Common
allRelevantVars | Agda.TypeChecking.Free
allRelevantVarsIgnoring | Agda.TypeChecking.Free
allRight | Agda.Utils.Either
allThingsInScope | Agda.Syntax.Scope.Base
allVars | Agda.TypeChecking.Free
AllWarnings | Agda.TypeChecking.Warnings
allWarnings | Agda.Interaction.Options.Warnings
ALNil | Agda.Auto.Syntax
ALProj | Agda.Auto.Syntax
Alt |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
alt | Agda.Compiler.MAlonzo.Compiler
alter | Agda.Utils.BiMap
alterM | Agda.Utils.BiMap
alterPrecondition | Agda.Utils.BiMap
altM1 | Agda.Utils.Monad
alwaysUnblock | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
Ambiguous | Agda.Interaction.FindFile
AmbiguousAnything | Agda.Syntax.Scope.Base
AmbiguousConProjs | Agda.Syntax.Scope.Base
AmbiguousConstructor | Agda.Syntax.Concrete.Definitions.Errors
AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions.Errors
AmbiguousLib | Agda.Interaction.Library.Base
AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbiguousNothing | Agda.Syntax.Scope.Base
AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbiguousQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
aModeToDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
andThen | Agda.Syntax.Parser.LexActions
Ann |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem
annLock | Agda.Syntax.Common
annotate | Agda.Utils.Parser.MemoisedCPS
annotateDecls | Agda.Syntax.Scope.Monad
annotateExpr | Agda.Syntax.Scope.Monad
annotatePattern | Agda.Syntax.Translation.ReflectedToAbstract
Annotation |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
AnnotationPattern | Agda.TypeChecking.Rules.LHS.Problem
AnnP | Agda.Syntax.Abstract
antiUnify | Agda.TypeChecking.Conversion
antiUnifyArgs | Agda.TypeChecking.Conversion
antiUnifyElims | Agda.TypeChecking.Conversion
antiUnifyType | Agda.TypeChecking.Conversion
AnyAbstract | Agda.Syntax.Abstract
anyAbstract | Agda.Syntax.Abstract
anyDefs | Agda.Termination.RecCheck
anyEllipsisVar | Agda.Interaction.MakeCase
AnyIsAbstract | Agda.Syntax.Common
anyIsAbstract | Agda.Syntax.Common
anyListT | Agda.Utils.ListT
anyM | Agda.Utils.Monad
AnyRigid | Agda.TypeChecking.MetaVars.Occurs
anyRigid | Agda.TypeChecking.MetaVars.Occurs
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.Common
appendList | Agda.Utils.List1
appHead | Agda.Auto.Syntax
AppInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
appInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Internal.Elim, Agda.Syntax.Internal
3 (Type/Class) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
4 (Data Constructor) | Agda.Syntax.Reflected
5 (Data Constructor) | Agda.Syntax.Abstract
6 (Type/Class) | Agda.Utils.TypeLevel
apply |
1 (Function) | Agda.Compiler.JS.Substitution
2 (Function) | Agda.Utils.AssocList
3 (Function) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
apply1 | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyCohesion | Agda.Syntax.Common
applyCohesionToContext | Agda.TypeChecking.Irrelevance
applyCohesionToContextOnly | Agda.TypeChecking.Irrelevance
applyDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
applyE | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyFlagsToTCWarnings | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
applyFlagsToTCWarningsPreserving | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
applyImportDirective | Agda.Syntax.Scope.Base
applyImportDirectiveM | Agda.Syntax.Scope.Monad
applyImportDirective_ | Agda.Syntax.Scope.Base
applyModality | Agda.Syntax.Common
applyModalityToContext | Agda.TypeChecking.Irrelevance
applyModalityToContextFunBody | Agda.TypeChecking.Irrelevance
applyModalityToContextOnly | Agda.TypeChecking.Irrelevance
applyModalityToJudgementOnly | Agda.TypeChecking.Irrelevance
applyNLPatSubst | Agda.TypeChecking.Substitute
applyNLSubstToDom | Agda.TypeChecking.Substitute
ApplyOrIApply | Agda.TypeChecking.Coverage.Match
applyPatSubst | Agda.TypeChecking.Substitute
applyperm | Agda.Auto.CaseSplit
applyQuantity | Agda.Syntax.Common
applyQuantityToContext | 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
applySection' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
applySplitPSubst | Agda.TypeChecking.Coverage.Match
applySubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applySubstTerm | Agda.TypeChecking.Substitute
applyTermE | Agda.TypeChecking.Substitute
applyUnless | Agda.Utils.Function
applyUnlessM | Agda.Utils.Function
applyWhen | Agda.Utils.Function
applyWhenM | Agda.Utils.Function
applyWhenVerboseS | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Reduce.Monad, Agda.TypeChecking.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
approxConInduction | Agda.Syntax.Scope.Base
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.Compiler.Backend, Agda.TypeChecking.Monad
apTCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Arc | Agda.Utils.Warshall
areWeCaching | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
Arg |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
ArgDescr | Agda.Interaction.Options
argFromDom | Agda.Syntax.Internal
argH | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
ArgInfo |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
argInfo | Agda.Syntax.Common
argInfoAnnotation | 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, Agda.TypeChecking.Primitive.Base
ArgName | Agda.Syntax.Common
argNameToString | Agda.Syntax.Common
ArgNode | Agda.TypeChecking.Positivity
Args |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Type/Class) | Agda.Syntax.Internal
3 (Type/Class) | Agda.Syntax.Reflected
4 (Type/Class) | Agda.Syntax.Abstract
ArgsCheckState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
argsFromElims | Agda.Syntax.Internal.Elim, 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
ArgUnused | Agda.Syntax.Treeless, Agda.Compiler.Backend
ArgUsage | Agda.Syntax.Treeless, Agda.Compiler.Backend
ArgUsed | Agda.Syntax.Treeless, Agda.Compiler.Backend
Arity | Agda.Syntax.Common
arity |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.TypeChecking.CompiledClause
arityPiPath | Agda.TypeChecking.Telescope.Path
Array |
1 (Data Constructor) | Agda.Compiler.JS.Syntax
2 (Type/Class) | Agda.Interaction.JSON
3 (Data Constructor) | Agda.Interaction.JSON
arrow | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
Arrows | Agda.Utils.TypeLevel
As | Agda.Syntax.Concrete
AsB | Agda.TypeChecking.Rules.LHS.Problem
AsBinding | Agda.TypeChecking.Rules.LHS.Problem
AsciiCounter | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
AsciiOnly | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options
asFinite | Agda.Utils.Float
AsIs | Agda.Interaction.Base
askGHCEnv | Agda.Compiler.MAlonzo.Misc
askGHCModuleEnv | Agda.Compiler.MAlonzo.Misc
askGhcOpts | Agda.Compiler.MAlonzo.Compiler
askHsModuleEnv | Agda.Compiler.MAlonzo.Misc
askName | Agda.Syntax.Translation.ReflectedToAbstract
askR | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Reduce.Monad, Agda.TypeChecking.Monad
asksTC | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
askTC | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
askVar | Agda.Syntax.Translation.ReflectedToAbstract
asMainFunctionDef | Agda.Compiler.MAlonzo.Primitives
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
asPatterns | Agda.TypeChecking.Rules.LHS.Problem
AsPatternShadowsConstructorOrPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AsPatternShadowsConstructorOrPatternSynonym_ | Agda.Interaction.Options.Warnings
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
asQuantity | Agda.Syntax.Common
asRange | Agda.Syntax.Concrete
Assign |
1 (Type/Class) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Interaction.Base
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
assignTermTCM' | Agda.TypeChecking.MetaVars
assignV | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
assignWrapper | Agda.TypeChecking.MetaVars
AsSizes | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Associativity | Agda.Syntax.Common
AssocList | Agda.Utils.AssocList
AsTermsOf | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AsTypes | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
asView | Agda.Syntax.Abstract.Views
atClause | Agda.TypeChecking.Rules.Def
atLeastTwoParts | Agda.Syntax.Concrete.Operators.Parser
atomicLevel | Agda.Syntax.Internal
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 |
1 (Function) | Agda.Interaction.BasicOps
2 (Function) | Agda.Interaction.InteractionTop
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
Axiom |
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
axiomConstTransp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AxiomName | Agda.Syntax.Scope.Base
axiomName | Agda.Syntax.Abstract