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
abstractToConcrete	Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteCtx	Agda.Syntax.Translation.AbstractToConcrete
abstractToConcrete_	Agda.Syntax.Translation.AbstractToConcrete
Absurd	Agda.Syntax.Concrete
AbsurdLam
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
AbsurdLambda	Agda.Auto.Syntax
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
actOnMeta	Agda.Interaction.CommandLine.CommandLine
actualConstructor	Agda.TypeChecking.Rules.Def
acyclic	Agda.Utils.Graph
add
1 (Function)	Agda.Termination.Semiring
2 (Function)	Agda.Termination.Matrix
3 (Function)	Agda.Termination.SparseMatrix
addAwakeConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
addblk	Agda.Auto.Typecheck
addColumn
1 (Function)	Agda.Termination.Matrix
2 (Function)	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
addCtx	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxs	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxString	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxString_	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxTel	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addDecl	Agda.Interaction.BasicOps
addDefName	Agda.Compiler.Epic.CompileState
addDisplayForm	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addDisplayForms	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEdge	Agda.Utils.Warshall
addend	Agda.Auto.Typecheck
addEpicCode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEquality	Agda.TypeChecking.Rules.LHS.Unify
addEqualityHH	Agda.TypeChecking.Rules.LHS.Unify
addExtLambdaTele	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
AddExtraRef	Agda.Auto.NarrowingSearch
addFinalNewLine	Agda.Utils.String
addFlex	Agda.Utils.Warshall
addForcingAnnotations	Agda.TypeChecking.Forcing
addHaskellCode	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
addInteractionPoint	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
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
1 (Function)	Agda.Termination.Matrix
2 (Function)	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	Agda.Utils.HashMap
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
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
allowedVar	Agda.TypeChecking.MetaVars.Occurs
allPaths	Agda.Utils.Graph
allRight	Agda.Utils.Either
allThingsInScope	Agda.Syntax.Scope.Base
allVars	Agda.TypeChecking.Free
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.Internal, Agda.Syntax.Abstract
AmbiguousTopLevelModuleName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbQ	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
amodName	Agda.Syntax.Scope.Base
anameKind	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
APatName	Agda.Syntax.Translation.ConcreteToAbstract
App
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Compiler.Epic.AuxAST
4 (Data Constructor)	Agda.Syntax.Abstract
5 (Data Constructor)	Agda.TypeChecking.EtaContract
app	Agda.Syntax.Abstract
appBrackets	Agda.Syntax.Fixity
appDef	Agda.TypeChecking.Reduce
appDef'	Agda.TypeChecking.Reduce
Application	Agda.Syntax.Abstract.Views
Apply
1 (Data Constructor)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Syntax.Internal
3 (Data Constructor)	Agda.Syntax.Abstract
4 (Type/Class)	Agda.TypeChecking.Substitute
apply
1 (Function)	Agda.Compiler.JS.Substitution
2 (Function)	Agda.TypeChecking.Substitute
applyDroppingParameters	Agda.TypeChecking.InstanceArguments
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
AppP	Agda.Syntax.Concrete
appP	Agda.Syntax.Concrete.Operators.Parser
apps	Agda.Compiler.Epic.AuxAST
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
argFromDom	Agda.Syntax.Common
argH	Agda.TypeChecking.Primitive
argHiding	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
argRelevance	Agda.Syntax.Common
Args
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
3 (Type/Class)	Agda.Syntax.Internal
args	Agda.Compiler.JS.Compiler
ArgumentCtx	Agda.Syntax.Fixity
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	Agda.Interaction.BasicOps
assign	Agda.TypeChecking.MetaVars
assignConstrTag	Agda.Compiler.Epic.CompileState
assignConstrTag'	Agda.Compiler.Epic.CompileState
assignTerm	Agda.TypeChecking.MetaVars
assignTerm'	Agda.TypeChecking.MetaVars
assignV	Agda.TypeChecking.MetaVars
associative	Agda.Utils.TestHelpers
asView	Agda.TypeChecking.Rules.LHS.Split
atomP	Agda.Syntax.Concrete.Operators.Parser
atTopLevel	Agda.Interaction.BasicOps
auto	Agda.Auto.Auto
Axiom
1 (Data Constructor)	Agda.Syntax.Abstract
2 (Data Constructor)	Agda.Syntax.Concrete.Definitions
3 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
axiomName	Agda.Syntax.Abstract