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
abort	Agda.TypeChecking.MetaVars.Occurs
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
absApp	Agda.TypeChecking.Substitute
absAppHH	Agda.TypeChecking.Rules.LHS.Unify
absBody	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	Agda.Utils.FileName
abspatvarname	Agda.Auto.CaseSplit
AbsToCon	Agda.Syntax.Translation.AbstractToConcrete
Abstract
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.TypeChecking.Substitute
abstract	Agda.TypeChecking.Substitute
abstractArgs	Agda.TypeChecking.Substitute
AbstractDef	Agda.Syntax.Common
AbstractMode
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AbstractModule	Agda.Syntax.Scope.Base
AbstractName	Agda.Syntax.Scope.Base
AbstractRHS	Agda.Syntax.Translation.ConcreteToAbstract
AbstractTerm	Agda.TypeChecking.Abstract
abstractTerm	Agda.TypeChecking.Abstract
abstractToConcreteCtx	Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteEnv	Agda.Syntax.Translation.AbstractToConcrete
abstractToConcrete_	Agda.Syntax.Translation.AbstractToConcrete
Absurd	Agda.Syntax.Concrete
absurdBody	Agda.Syntax.Internal
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
AbsurdP
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
AbsurdPatternRequiresNoRHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AbsurdRHS
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
Access	Agda.Syntax.Common
Account	Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
actOnMeta	Agda.Interaction.CommandLine.CommandLine
acyclic
1 (Function)	Agda.Utils.Graph.AdjacencyMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
add
1 (Function)	Agda.Termination.Semiring
2 (Function)	Agda.Termination.SparseMatrix
addAwakeConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
addblk	Agda.Auto.Typecheck
addClauses	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addColumn	Agda.Termination.SparseMatrix
addConnection	Agda.Interaction.Highlighting.Dot
addConstant	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addConstraint
1 (Function)	Agda.Utils.Warshall
2 (Function)	Agda.TypeChecking.Constraints
3 (Function)	Agda.Compiler.Epic.Injection
addConstraint'	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
AddContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCPUTime	Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
addCtx	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxs	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxString	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxStrings_	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxString_	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxTel	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addDefName	Agda.Compiler.Epic.CompileState
addDisplayForm	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addDisplayForms	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEdge
1 (Function)	Agda.Utils.Warshall
2 (Function)	Agda.TypeChecking.SizedTypes.WarshallSolver
addend	Agda.Auto.Typecheck
addEpicCode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEquality	Agda.TypeChecking.Rules.LHS.Unify
addEqualityHH	Agda.TypeChecking.Rules.LHS.Unify
AddExtraRef	Agda.Auto.NarrowingSearch
addFinalNewLine	Agda.Utils.String
addFlex	Agda.Utils.Warshall
addForcingAnnotations	Agda.TypeChecking.Forcing
addHaskellCode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addHaskellExport	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addHaskellImport	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
addHaskellType	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addImport	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
addImportCycleCheck	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
addImportedThings	Agda.Interaction.Imports
addJSCode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addLetBinding	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addModule	Agda.Interaction.Highlighting.Dot
addModuleToScope	Agda.Syntax.Scope.Base
addNamesToScope	Agda.Syntax.Scope.Base
addNameToScope	Agda.Syntax.Scope.Base
addNode	Agda.Utils.Warshall
addRow	Agda.Termination.SparseMatrix
addSection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addSuffix	Agda.Utils.Suffix
addtrailingargs	Agda.Auto.Syntax
ADef	Agda.TypeChecking.Positivity
AdjList	Agda.Utils.Warshall
adjust
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Trie
agdaTermType	Agda.TypeChecking.Quote
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
allApplyElims	Agda.Syntax.Internal
allEqual	Agda.Utils.List
allHoles	Agda.Syntax.Internal.Pattern
allHolesWithContents	Agda.Syntax.Internal.Pattern
allKindsOfNames	Agda.Syntax.Scope.Base
allMetaKinds	Agda.TypeChecking.MetaVars
allMetas	Agda.TypeChecking.MetaVars
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
AllowedReduction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AllowedReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
allowedVar	Agda.TypeChecking.MetaVars.Occurs
allPaths
1 (Function)	Agda.Utils.Graph.AdjacencyMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
allReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
allRight	Agda.Utils.Either
allThingsInScope	Agda.Syntax.Scope.Base
allVars	Agda.TypeChecking.Free
allWithKey	Agda.Utils.Map
ALNil	Agda.Auto.Syntax
ALProj	Agda.Auto.Syntax
alreadyVisited	Agda.Interaction.Imports
altM1	Agda.Utils.Monad
Ambiguous	Agda.Interaction.FindFile
AmbiguousFunClauses	Agda.Syntax.Concrete.Definitions
AmbiguousModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousParseForApplication	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousParseForLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousQName	Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
AmbiguousTopLevelModuleName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbQ	Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
amodLineage	Agda.Syntax.Scope.Base
amodName	Agda.Syntax.Scope.Base
anameKind	Agda.Syntax.Scope.Base
anameLineage	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
AnyAbstract	Agda.Syntax.Abstract
anyAbstract	Agda.Syntax.Abstract
AnyWhere	Agda.Syntax.Concrete
ap	Agda.Utils.Monad
APatName	Agda.Syntax.Translation.ConcreteToAbstract
App
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Syntax.Abstract
4 (Data Constructor)	Agda.Compiler.Epic.AuxAST
5 (Data Constructor)	Agda.TypeChecking.EtaContract
app	Agda.Syntax.Abstract
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
appHead	Agda.Auto.Syntax
appInteractionOutputCallback	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
Application	Agda.Syntax.Abstract.Views
Applied	Agda.Syntax.Scope.Base
Apply
1 (Data Constructor)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Syntax.Internal
4 (Type/Class)	Agda.TypeChecking.Substitute
apply
1 (Function)	Agda.Compiler.JS.Substitution
2 (Function)	Agda.TypeChecking.Substitute
applyDef	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
applyDroppingParameters	Agda.TypeChecking.InstanceArguments
applyE	Agda.TypeChecking.Substitute
applyFreq	Agda.TypeChecking.Test.Generators
ApplyHH	Agda.TypeChecking.Rules.LHS.Unify
applyHH	Agda.TypeChecking.Rules.LHS.Unify
applyImportDirective	Agda.Syntax.Scope.Base
applyImportDirectiveM	Agda.Syntax.Scope.Monad
applyperm	Agda.Auto.CaseSplit
applyRelevance	Agda.TypeChecking.Irrelevance
applyRelevanceToContext	Agda.TypeChecking.Irrelevance
applySection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
applySubst	Agda.TypeChecking.Substitute
applyUnless	Agda.Utils.Function
applyWhen	Agda.Utils.Function
appOK	Agda.Auto.Syntax
AppP	Agda.Syntax.Concrete
appP	Agda.Syntax.Concrete.Operators.Parser
apps	Agda.Compiler.Epic.AuxAST
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
apTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Arbitrary	Agda.Utils.QuickCheck
arbitrary	Agda.Utils.QuickCheck
arbitraryBoundedEnum	Agda.Utils.QuickCheck
arbitraryBoundedIntegral	Agda.Utils.QuickCheck
arbitraryBoundedRandom	Agda.Utils.QuickCheck
arbitrarySizedBoundedIntegral	Agda.Utils.QuickCheck
arbitrarySizedFractional	Agda.Utils.QuickCheck
arbitrarySizedIntegral	Agda.Utils.QuickCheck
Arc	Agda.Utils.Warshall
Arg
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
3 (Type/Class)	Agda.Syntax.Concrete
4 (Type/Class)	Agda.Syntax.Abstract
5 (Type/Class)	Agda.Syntax.Internal
argColors	Agda.Syntax.Common
argFromDom	Agda.Syntax.Common
argFromElim	Agda.Syntax.Internal
argH	Agda.TypeChecking.Primitive
ArgInfo
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
3 (Type/Class)	Agda.Syntax.Concrete
4 (Type/Class)	Agda.Syntax.Abstract
5 (Type/Class)	Agda.Syntax.Internal
argInfo	Agda.Syntax.Common
argInfoColors	Agda.Syntax.Common
argInfoHiding	Agda.Syntax.Common
argInfoRelevance	Agda.Syntax.Common
argIsDef	Agda.Compiler.Epic.NatDetection
ArgList	Agda.Auto.Syntax
argN	Agda.TypeChecking.Primitive
argName	Agda.Syntax.Internal
ArgNode	Agda.TypeChecking.Positivity
argpatts	Agda.Compiler.MAlonzo.Compiler
Args
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
3 (Type/Class)	Agda.Syntax.Abstract
4 (Type/Class)	Agda.Syntax.Internal
args	Agda.Compiler.JS.Compiler
argsFromElims	Agda.Syntax.Internal
ArgsHH	Agda.TypeChecking.Rules.LHS.Unify
argToDontCare	Agda.TypeChecking.Substitute
Argument	Agda.Interaction.Highlighting.Precise
ArgumentCtx	Agda.Syntax.Fixity
ArgumentIndex	Agda.Termination.CallMatrix
ArgumentTo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Arity	Agda.Syntax.Common
arity
1 (Function)	Agda.Syntax.Internal
2 (Function)	Agda.TypeChecking.CompiledClause
arrow	Agda.Syntax.Concrete.Pretty
As	Agda.Syntax.Concrete
AsB	Agda.TypeChecking.Rules.LHS.Problem
AsBinding	Agda.TypeChecking.Rules.LHS.Problem
AsIs	Agda.Interaction.BasicOps
askPostpone	Agda.TypeChecking.Rules.LHS.Unify
AsName
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	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
asRange	Agda.Syntax.Concrete
Assign
1 (Type/Class)	Agda.Syntax.Abstract
2 (Data Constructor)	Agda.Interaction.BasicOps
assign	Agda.TypeChecking.MetaVars
assignConstrTag	Agda.Compiler.Epic.CompileState
assignConstrTag'	Agda.Compiler.Epic.CompileState
assignE	Agda.TypeChecking.Conversion
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
associative	Agda.Utils.TestHelpers
asView	Agda.Syntax.Abstract.Views
AsWeightRelation	Agda.TypeChecking.SizedTypes.Tests
atomP	Agda.Syntax.Concrete.Operators.Parser
atTopLevel	Agda.Interaction.BasicOps
augCallInfo	Agda.Termination.CallMatrix
augCallMatrix	Agda.Termination.CallMatrix
auto	Agda.Auto.Auto
Axiom
1 (Data Constructor)	Agda.Syntax.Abstract
2 (Type/Class)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Syntax.Concrete.Definitions
4 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
axiomName	Agda.Syntax.Abstract