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

Index

!!! 
1 (Function)Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
2 (Function)Agda.Compiler.Epic.Injection
$!!Agda.Syntax.Strict
$$ 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
$$$Agda.Syntax.Concrete.Operators.Parser
$+$Agda.Utils.Pretty
&&-Agda.Compiler.Epic.Erasure
+++ 
1 (Function)Agda.Utils.ReadP
2 (Function)Agda.Compiler.Epic.Smashing
-*-Agda.Utils.Tuple
-->Agda.TypeChecking.Primitive
.&&. 
1 (Function)Agda.Utils.QuickCheck
2 (Function)Agda.Syntax.Parser.Alex
.&.Agda.Utils.QuickCheck
.*.Agda.Termination.CallGraph
.||. 
1 (Function)Agda.Utils.QuickCheck
2 (Function)Agda.Syntax.Parser.Alex
/\ 
1 (Function)Agda.Utils.Tuple
2 (Function)Agda.TypeChecking.Polarity
:->Agda.TypeChecking.CompiledClause
<#>Agda.TypeChecking.Primitive
<$>Agda.Utils.Monad
<*>Agda.Utils.Monad
<++Agda.Utils.ReadP
<+> 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
<.>Agda.Utils.Monad
<:Agda.Compiler.Epic.Injection
<> 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
<@>Agda.TypeChecking.Primitive
===Agda.Utils.FileName
==>Agda.Utils.QuickCheck
>*< 
1 (Function)Agda.Termination.CallGraph
2 (Function)Agda.TypeChecking.Positivity
>+<Agda.TypeChecking.Positivity
><Agda.Utils.QuickCheck
AAgda.Interaction.EmacsCommand
abortAgda.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
absAppAgda.TypeChecking.Substitute
absAppHHAgda.TypeChecking.Rules.LHS.Unify
absBodyAgda.TypeChecking.Substitute
abslamvarnameAgda.Auto.Convert
AbsModuleAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
AbsNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
absNameAgda.Syntax.Internal
absoluteAgda.Utils.FileName
AbsolutePathAgda.Utils.FileName
abspatvarnameAgda.Auto.CaseSplit
AbsToConAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
Abstract 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Type/Class)Agda.TypeChecking.Substitute
abstractAgda.TypeChecking.Substitute
abstractArgsAgda.TypeChecking.Substitute
AbstractDefAgda.Syntax.Common
AbstractMode 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AbstractModuleAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
AbstractNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
AbstractRHSAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
AbstractTermAgda.TypeChecking.Abstract
abstractTermAgda.TypeChecking.Abstract
abstractToConcreteAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
abstractToConcreteCtxAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
abstractToConcrete_Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
AbsurdAgda.Syntax.Concrete
AbsurdLam 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
AbsurdLambdaAgda.Auto.Syntax
AbsurdP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
AbsurdPatternRequiresNoRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AbsurdRHS 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
AccessAgda.Syntax.Common
actOnMetaAgda.Interaction.CommandLine.CommandLine
actualConstructorAgda.TypeChecking.Rules.Def
add 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.SparseMatrix
3 (Function)Agda.Termination.Matrix
addAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
addblkAgda.Auto.Typecheck
addColumn 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
addConnectionAgda.Interaction.Highlighting.Dot
addConstantAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addConstraint 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.Compiler.Epic.Injection
3 (Function)Agda.TypeChecking.Constraints
addConstraint'Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
addContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxsAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxStringAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxTelAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addDeclAgda.Interaction.BasicOps
addDefNameAgda.Compiler.Epic.CompileState
addDisplayFormAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addDisplayFormsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEdgeAgda.Utils.Warshall
addendAgda.Auto.Typecheck
addEpicCodeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEqualityAgda.TypeChecking.Rules.LHS.Unify
addEqualityHHAgda.TypeChecking.Rules.LHS.Unify
addExtLambdaTeleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
AddExtraRefAgda.Auto.NarrowingSearch
addFinalNewLineAgda.Utils.String
addFlexAgda.Utils.Warshall
addForcingAnnotationsAgda.TypeChecking.Forcing
addHaskellCodeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addHaskellImportAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
addHaskellTypeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addImportAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
addImportCycleCheckAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
addImportedThingsAgda.Interaction.Imports
addInteractionPointAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
addJSCodeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addLetBindingAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addModuleAgda.Interaction.Highlighting.Dot
addModuleToScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
addNamesToScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
addNameToScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
addNodeAgda.Utils.Warshall
addRow 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
addSectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addSuffixAgda.Utils.Suffix
addtrailingargsAgda.Auto.Syntax
ADefAgda.TypeChecking.Positivity
AdjListAgda.Utils.Warshall
agdaTermTypeAgda.TypeChecking.Quote
ALConParAgda.Auto.Syntax
ALConsAgda.Auto.Syntax
AlexEOFAgda.Syntax.Parser.Lexer
AlexErrorAgda.Syntax.Parser.Lexer
alexGetByteAgda.Syntax.Parser.Alex
alexGetCharAgda.Syntax.Parser.Alex
AlexInput 
1 (Type/Class)Agda.Syntax.Parser.Alex
2 (Data Constructor)Agda.Syntax.Parser.Alex
alexInputPrevCharAgda.Syntax.Parser.Alex
AlexReturnAgda.Syntax.Parser.Lexer
alexScanUserAgda.Syntax.Parser.Lexer
AlexSkipAgda.Syntax.Parser.Lexer
AlexTokenAgda.Syntax.Parser.Lexer
alignAgda.Utils.Pretty
allEqualAgda.Utils.List
allHolesAgda.Syntax.Internal.Pattern
allHolesWithContentsAgda.Syntax.Internal.Pattern
allMetaKindsAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
allNamesAgda.Syntax.Abstract
allNamesInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
allNamesInScope'Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
allocAgda.Utils.Pointer
allowedVarAgda.TypeChecking.MetaVars.Occurs
allPathsAgda.Utils.Graph
allRightAgda.Utils.Either
allThingsInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
allVarOrIrrelevantAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
allVarsAgda.TypeChecking.Free
ALNilAgda.Auto.Syntax
ALProjAgda.Auto.Syntax
alreadyVisitedAgda.Interaction.Imports
AmbiguousAgda.Interaction.FindFile
AmbiguousFunClausesAgda.Syntax.Concrete.Definitions
AmbiguousModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousParseForApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousParseForLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousQNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
AmbiguousTopLevelModuleNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
amodNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
anameKindAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
anameNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
AnArgAgda.TypeChecking.Positivity
AndAgda.Auto.NarrowingSearch
AnyAbstractAgda.Syntax.Abstract
anyAbstractAgda.Syntax.Abstract
AnyWhereAgda.Syntax.Concrete
APatNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
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
appBracketsAgda.Syntax.Fixity
ApplicationAgda.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
ApplyHHAgda.TypeChecking.Rules.LHS.Unify
applyHHAgda.TypeChecking.Rules.LHS.Unify
applyImportDirectiveAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
applyImportDirectiveMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
applypermAgda.Auto.CaseSplit
applyRelevanceAgda.TypeChecking.Irrelevance
applyRelevanceToContextAgda.TypeChecking.Irrelevance
applySectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
AppPAgda.Syntax.Concrete
appPAgda.Syntax.Concrete.Operators.Parser
apps 
1 (Function)Agda.Compiler.Epic.AuxAST
2 (Function)Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
AppVAgda.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
ArbitraryAgda.Utils.QuickCheck
arbitraryAgda.Utils.QuickCheck
arbitraryBoundedIntegralAgda.Utils.QuickCheck
arbitraryBoundedRandomAgda.Utils.QuickCheck
arbitrarySizedBoundedIntegralAgda.Utils.QuickCheck
arbitrarySizedFractionalAgda.Utils.QuickCheck
arbitrarySizedIntegralAgda.Utils.QuickCheck
ArcAgda.Utils.Warshall
Arg 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
argHAgda.TypeChecking.Primitive
argHidingAgda.Syntax.Common
argIsDefAgda.Compiler.Epic.NatDetection
ArgListAgda.Auto.Syntax
argNAgda.TypeChecking.Primitive
argNameAgda.Syntax.Internal
ArgNodeAgda.TypeChecking.Positivity
argpattsAgda.Compiler.MAlonzo.Compiler
argRelevanceAgda.Syntax.Common
Args 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
3 (Type/Class)Agda.Syntax.Internal
argsAgda.Compiler.JS.Compiler
ArgumentCtxAgda.Syntax.Fixity
ArgumentToAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ArityAgda.Syntax.Common
arityAgda.Syntax.Internal
arrowAgda.Syntax.Concrete.Pretty
AsAgda.Syntax.Concrete
AsBAgda.TypeChecking.Rules.LHS
AsBindingAgda.TypeChecking.Rules.LHS
AsIsAgda.Interaction.BasicOps
askPostponeAgda.TypeChecking.Rules.LHS.Unify
AsName 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
asNameAgda.Syntax.Concrete
AsP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
AspectAgda.Interaction.Highlighting.Precise
aspectAgda.Interaction.Highlighting.Precise
asRangeAgda.Syntax.Concrete
AssignAgda.Interaction.BasicOps
assignAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
assignConstrTagAgda.Compiler.Epic.CompileState
assignConstrTag'Agda.Compiler.Epic.CompileState
assignTermAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
assignVAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
associativeAgda.Utils.TestHelpers
asViewAgda.TypeChecking.Rules.LHS.Split
atomPAgda.Syntax.Concrete.Operators.Parser
atTopLevelAgda.Interaction.BasicOps
autoAgda.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
axiomNameAgda.Syntax.Abstract
BAgda.Utils.Map
BackendAgda.Interaction.GhciTop
backupPosAgda.Syntax.Position, Agda.Interaction.GhciTop
BadImplicitsAgda.TypeChecking.Implicit
beginAgda.Syntax.Parser.LexActions
beginningOfAgda.Syntax.Position, Agda.Interaction.GhciTop
beginningOfFileAgda.Syntax.Position, Agda.Interaction.GhciTop
begin_Agda.Syntax.Parser.LexActions
betareduceAgda.Auto.CaseSplit
betweenAgda.Utils.ReadP
BinAppViewAgda.TypeChecking.EtaContract
binAppViewAgda.TypeChecking.EtaContract
BindAgda.Syntax.Internal
bindAsPatternsAgda.TypeChecking.Rules.LHS
bindBuiltinAgda.TypeChecking.Rules.Builtin
bindBuiltinFlatAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinInfAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinNameAgda.TypeChecking.Monad.Builtin
bindBuiltinSharpAgda.TypeChecking.Rules.Builtin.Coinduction
bindExprAgda.Compiler.Epic.CompileState
BindHoleAgda.Syntax.Notation
bindLHSVarsAgda.TypeChecking.Rules.LHS
bindModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindNameAgda.Syntax.Scope.Monad
bindParametersAgda.TypeChecking.Rules.Data
bindPostulatedNameAgda.TypeChecking.Rules.Builtin
bindPrimitiveAgda.TypeChecking.Monad.Builtin
bindQModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindToConcreteAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
bindVariableAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
BinOpAgda.Compiler.JS.Syntax
binop 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Concrete.Operators.Parser
Blind 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
BlkInfoAgda.Auto.NarrowingSearch
BlockAgda.TypeChecking.Coverage.Match
blockAgda.Compiler.JS.Pretty
block'Agda.Compiler.JS.Pretty
Blocked 
1 (Data Constructor)Agda.Auto.NarrowingSearch
2 (Type/Class)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Internal
blockedAgda.Syntax.Internal
BlockedConstAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BlockedLevelAgda.Syntax.Internal
blockingMetaAgda.Syntax.Internal
blockOfLinesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
blockTermAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
blockTermOnProblemAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
bltQualAgda.Compiler.MAlonzo.Misc
bltQual'Agda.Compiler.MAlonzo.Primitives
BNameAgda.Syntax.Concrete
bnameFixityAgda.Syntax.Concrete
BodyAgda.Syntax.Internal
body 
1 (Function)Agda.Compiler.JS.Case
2 (Function)Agda.Compiler.JS.Compiler
bolAgda.Syntax.Parser.Lexer
boolPrimTFAgda.Compiler.Epic.Primitive
boolSemiringAgda.Termination.Semiring
BothWithAndRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BoundAgda.Interaction.Highlighting.Precise
BoundNameAgda.Syntax.Concrete
boundNameAgda.Syntax.Concrete
brAgda.Compiler.JS.Pretty
bracedAgda.Compiler.JS.Parser
bracedBlockAgda.Compiler.JS.Parser
braces 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
braces'Agda.Syntax.Concrete.Pretty
bracketAgda.Utils.Monad
bracketedAgda.Compiler.JS.Parser
brackets 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
Branch 
1 (Type/Class)Agda.Compiler.Epic.AuxAST
2 (Data Constructor)Agda.Compiler.Epic.AuxAST
BranchesAgda.TypeChecking.CompiledClause
brExprAgda.Compiler.Epic.AuxAST
BrIntAgda.Compiler.Epic.AuxAST
brIntAgda.Compiler.Epic.AuxAST
brNameAgda.Compiler.Epic.AuxAST
brTagAgda.Compiler.Epic.AuxAST
brVarsAgda.Compiler.Epic.AuxAST
buildClosureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
buildConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
buildGraphAgda.Utils.Warshall
buildInterfaceAgda.Interaction.Imports
buildLambdaAgda.Compiler.Epic.Smashing
buildListAgda.TypeChecking.Primitive
buildMPatternsAgda.TypeChecking.Coverage.Match
buildOccurrenceGraphAgda.TypeChecking.Positivity
buildProblemConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
buildTermAgda.Compiler.Epic.Forcing
buildWithFunctionAgda.TypeChecking.With
Builtin 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinAgdaDataDefAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionDataConstructorAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionDataDefAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionFunDefAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionPostulateAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionPrimitiveAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionRecordDefAgda.TypeChecking.Monad.Builtin
builtinAgdaFunDefAgda.TypeChecking.Monad.Builtin
builtinAgdaRecordDefAgda.TypeChecking.Monad.Builtin
builtinAgdaSortAgda.TypeChecking.Monad.Builtin
builtinAgdaSortLitAgda.TypeChecking.Monad.Builtin
builtinAgdaSortSetAgda.TypeChecking.Monad.Builtin
builtinAgdaSortUnsupportedAgda.TypeChecking.Monad.Builtin
builtinAgdaTermAgda.TypeChecking.Monad.Builtin
builtinAgdaTermConAgda.TypeChecking.Monad.Builtin
builtinAgdaTermDefAgda.TypeChecking.Monad.Builtin
builtinAgdaTermLamAgda.TypeChecking.Monad.Builtin
builtinAgdaTermPiAgda.TypeChecking.Monad.Builtin
builtinAgdaTermSortAgda.TypeChecking.Monad.Builtin
builtinAgdaTermUnsupportedAgda.TypeChecking.Monad.Builtin
builtinAgdaTermVarAgda.TypeChecking.Monad.Builtin
builtinAgdaTypeAgda.TypeChecking.Monad.Builtin
builtinAgdaTypeElAgda.TypeChecking.Monad.Builtin
builtinArgAgda.TypeChecking.Monad.Builtin
builtinArgArgAgda.TypeChecking.Monad.Builtin
builtinBoolAgda.TypeChecking.Monad.Builtin
builtinCharAgda.TypeChecking.Monad.Builtin
builtinConsAgda.TypeChecking.Monad.Builtin
BuiltinDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinDataConsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinDescAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinDescriptorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinEqualityAgda.TypeChecking.Monad.Builtin
builtinFalseAgda.TypeChecking.Monad.Builtin
builtinFlatAgda.TypeChecking.Monad.Builtin
builtinFloatAgda.TypeChecking.Monad.Builtin
builtinHiddenAgda.TypeChecking.Monad.Builtin
builtinHidingAgda.TypeChecking.Monad.Builtin
builtinInfAgda.TypeChecking.Monad.Builtin
BuiltinInfo 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinInParameterisedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinInstanceAgda.TypeChecking.Monad.Builtin
builtinIntegerAgda.TypeChecking.Monad.Builtin
builtinIOAgda.TypeChecking.Monad.Builtin
builtinIrrelevantAgda.TypeChecking.Monad.Builtin
builtinLevelAgda.TypeChecking.Monad.Builtin
builtinLevelKitAgda.TypeChecking.Level
builtinLevelMaxAgda.TypeChecking.Monad.Builtin
builtinLevelSucAgda.TypeChecking.Monad.Builtin
builtinLevelZeroAgda.TypeChecking.Monad.Builtin
builtinListAgda.TypeChecking.Monad.Builtin
BuiltinMustBeConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinNatAgda.TypeChecking.Monad.Builtin
builtinNatDivSucAuxAgda.TypeChecking.Monad.Builtin
builtinNatEqualsAgda.TypeChecking.Monad.Builtin
builtinNatLessAgda.TypeChecking.Monad.Builtin
builtinNatMinusAgda.TypeChecking.Monad.Builtin
builtinNatModSucAuxAgda.TypeChecking.Monad.Builtin
builtinNatPlusAgda.TypeChecking.Monad.Builtin
builtinNatTimesAgda.TypeChecking.Monad.Builtin
builtinNilAgda.TypeChecking.Monad.Builtin
BuiltinPostulateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
BuiltinPrimAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinQNameAgda.TypeChecking.Monad.Builtin
builtinReflAgda.TypeChecking.Monad.Builtin
builtinRelevanceAgda.TypeChecking.Monad.Builtin
builtinRelevantAgda.TypeChecking.Monad.Builtin
builtinSharpAgda.TypeChecking.Monad.Builtin
builtinSizeAgda.TypeChecking.Monad.Builtin
builtinSizeInfAgda.TypeChecking.Monad.Builtin
builtinSizeSucAgda.TypeChecking.Monad.Builtin
builtinStringAgda.TypeChecking.Monad.Builtin
builtinSucAgda.TypeChecking.Monad.Builtin
BuiltinThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinTrueAgda.TypeChecking.Monad.Builtin
BuiltinUnknownAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinVisibleAgda.TypeChecking.Monad.Builtin
builtinZeroAgda.TypeChecking.Monad.Builtin
CActionAgda.Auto.Syntax
calcAgda.Auto.NarrowingSearch
calcEqRStateAgda.Auto.Typecheck
CALConcatAgda.Auto.Syntax
Call 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.Termination.CallGraph
3 (Data Constructor)Agda.Termination.CallGraph
callGHCAgda.Compiler.MAlonzo.Compiler
CallGraphAgda.Termination.CallGraph
callGraphInvariantAgda.Termination.CallGraph
CallInfo 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInfoCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInfoRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInvariantAgda.Termination.CallGraph
CallMatrix 
1 (Type/Class)Agda.Termination.CallGraph
2 (Data Constructor)Agda.Termination.CallGraph
callMatrixInvariantAgda.Termination.CallGraph
callsAgda.Termination.Lexicographic
CALNilAgda.Auto.Syntax
canonicalNameAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
CantSplitAgda.TypeChecking.Coverage
Case 
1 (Type/Class)Agda.Compiler.JS.Case
2 (Data Constructor)Agda.Compiler.JS.Case
3 (Data Constructor)Agda.Compiler.Epic.AuxAST
4 (Data Constructor)Agda.TypeChecking.CompiledClause
5 (Type/Class)Agda.TypeChecking.CompiledClause
CaseContextAgda.Interaction.MakeCase
caseeAgda.Compiler.Epic.AuxAST
caseOptsAgda.Compiler.Epic.CaseOpts
caseOptsExprAgda.Compiler.Epic.CaseOpts
caseSplitSearchAgda.Auto.CaseSplit
caseSplitSearch'Agda.Auto.CaseSplit
catAgda.Utils.Pretty
catchAllAgda.TypeChecking.CompiledClause
catchAllBranchAgda.TypeChecking.CompiledClause
catchConstraintAgda.TypeChecking.Constraints
catchError_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
catchExceptionAgda.TypeChecking.Monad.Exception
catchImpossibleAgda.Utils.Impossible
categorizedeclAgda.Auto.Syntax
catMaybesAgda.Utils.Maybe
cdcontAgda.Auto.Syntax
cddeffreevarsAgda.Auto.Syntax
cdeclAgda.Compiler.MAlonzo.Compiler
cdnameAgda.Auto.Syntax
cdoriginAgda.Auto.Syntax
cdtypeAgda.Auto.Syntax
CExpAgda.Auto.Syntax
chainlAgda.Utils.ReadP
chainl1Agda.Utils.ReadP
chainl1'Agda.Syntax.Concrete.Operators.Parser
chainrAgda.Utils.ReadP
chainr1Agda.Utils.ReadP
chainr1'Agda.Syntax.Concrete.Operators.Parser
CharAgda.Compiler.JS.Syntax
char 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Utils.ReadP
chattyAgda.Utils.QuickCheck
checkAllVarsAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
CheckArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkArgumentsAgda.TypeChecking.Rules.Term
checkArguments'Agda.TypeChecking.Rules.Term
checkArguments_Agda.TypeChecking.Rules.Term
checkAxiomAgda.TypeChecking.Rules.Decl
CheckClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkClauseAgda.TypeChecking.Rules.Def
CheckConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkConstructorAgda.TypeChecking.Rules.Data
checkConstructorApplicationAgda.TypeChecking.Rules.Term
checkConstructorTypeAgda.Compiler.MAlonzo.Compiler
checkCoverAgda.Compiler.MAlonzo.Compiler
checkCoverageAgda.TypeChecking.Coverage
CheckDataDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkDataDefAgda.TypeChecking.Rules.Data
checkDeclAgda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop
checkDeclsAgda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop
CheckDotPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkDotPatternAgda.TypeChecking.Rules.LHS
checkeliminandAgda.Auto.Typecheck
checkEqualitiesAgda.TypeChecking.Rules.LHS.Unify
checkEqualityAgda.TypeChecking.Rules.LHS.Unify
checkEqualityHHAgda.TypeChecking.Rules.LHS.Unify
CheckExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkExprAgda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop
checkForImportCycleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
CheckFunDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkFunDefAgda.TypeChecking.Rules.Def
checkFunDef'Agda.TypeChecking.Rules.Def
checkHeadApplicationAgda.TypeChecking.Rules.Term
checkImportAgda.TypeChecking.Rules.Decl
checkInjectivityAgda.TypeChecking.Injectivity
CheckIsEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkLambdaAgda.TypeChecking.Rules.Term
checkLeftHandSideAgda.TypeChecking.Rules.LHS
CheckLetBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkLetBindingAgda.TypeChecking.Rules.Term
checkLetBindingsAgda.TypeChecking.Rules.Term
checkLiteralAgda.TypeChecking.Rules.Term
checkMetaAgda.TypeChecking.Rules.Term
checkModuleArityAgda.TypeChecking.Rules.Decl
checkModuleNameAgda.Interaction.FindFile
checkMutualAgda.TypeChecking.Rules.Decl
checkOptsAgda.Interaction.Options
CheckPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckPatternShadowingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckPragmaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkPragmaAgda.TypeChecking.Rules.Decl
CheckPrimitiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkPrimitiveAgda.TypeChecking.Rules.Decl
CheckRecDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkRecDefAgda.TypeChecking.Rules.Record
checkRecordProjectionsAgda.TypeChecking.Rules.Record
checkSectionAgda.TypeChecking.Rules.Decl
CheckSectionApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkSectionApplicationAgda.TypeChecking.Rules.Decl
checkSectionApplication'Agda.TypeChecking.Rules.Decl
checkSizeIndexAgda.TypeChecking.Polarity
checkStrictlyPositiveAgda.TypeChecking.Positivity
checkTelescope_Agda.TypeChecking.Rules.Term
checkTermAgda.TypeChecking.Rules.Term
checkTypedBindingAgda.TypeChecking.Rules.Term
checkTypedBindingsAgda.TypeChecking.Rules.Term
checkTypedBindings_Agda.TypeChecking.Rules.Term
checkTypeOfMainAgda.Compiler.MAlonzo.Primitives
checkTypeSignatureAgda.TypeChecking.Rules.Decl
checkWhereAgda.TypeChecking.Rules.Def
checkWithFunctionAgda.TypeChecking.Rules.Def
CheckWithFunctionTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ChoiceAgda.Auto.NarrowingSearch
choice 
1 (Function)Agda.Utils.ReadP
2 (Function)Agda.TypeChecking.Coverage.Match
3 (Function)Agda.TypeChecking.Quote
choose 
1 (Function)Agda.Utils.QuickCheck
2 (Function)Agda.Auto.NarrowingSearch
choosePrioMetaAgda.Auto.NarrowingSearch
chopAgda.Utils.List
ChrAgda.Utils.Pretty
ClAgda.TypeChecking.CompiledClause.Compile
ClashingDefinitionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingFileNamesForAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingModuleImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
classifyAgda.Utils.QuickCheck
Clause 
1 (Type/Class)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Internal
4 (Type/Class)Agda.Syntax.Abstract
5 (Data Constructor)Agda.Syntax.Abstract
6 (Type/Class)Agda.Syntax.Concrete.Definitions
7 (Data Constructor)Agda.Syntax.Concrete.Definitions
clause 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
ClauseBodyAgda.Syntax.Internal
clauseBodyAgda.Syntax.Internal
clausebodyAgda.Compiler.MAlonzo.Compiler
clausePatsAgda.Syntax.Internal
clausePermAgda.Syntax.Internal
clauseRangeAgda.Syntax.Internal
clauseTelAgda.Syntax.Internal
clearMetaListenersAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
clEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Clos 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
closeBraceAgda.Syntax.Parser.Layout
ClosedLevelAgda.Syntax.Internal
closifyAgda.Auto.Syntax
Closure 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClsAgda.TypeChecking.CompiledClause.Compile
clScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clValueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
cmAgda.Termination.CallGraph
cmd_autoAgda.Interaction.GhciTop
cmd_compileAgda.Interaction.GhciTop
cmd_computeAgda.Interaction.GhciTop
cmd_compute_toplevelAgda.Interaction.GhciTop
cmd_constraintsAgda.Interaction.GhciTop
cmd_contextAgda.Interaction.GhciTop
cmd_giveAgda.Interaction.GhciTop
cmd_goal_typeAgda.Interaction.GhciTop
cmd_goal_type_contextAgda.Interaction.GhciTop
cmd_goal_type_context_andAgda.Interaction.GhciTop
cmd_goal_type_context_inferAgda.Interaction.GhciTop
cmd_inferAgda.Interaction.GhciTop
cmd_infer_toplevelAgda.Interaction.GhciTop
cmd_introAgda.Interaction.GhciTop
cmd_loadAgda.Interaction.GhciTop
cmd_load'Agda.Interaction.GhciTop
cmd_make_caseAgda.Interaction.GhciTop
cmd_metasAgda.Interaction.GhciTop
cmd_refineAgda.Interaction.GhciTop
cmd_refine_or_introAgda.Interaction.GhciTop
cmd_show_module_contentsAgda.Interaction.GhciTop
cmd_show_module_contents_toplevelAgda.Interaction.GhciTop
cmd_solveAllAgda.Interaction.GhciTop
cmd_write_highlighting_infoAgda.Interaction.GhciTop
CMFBlockedAgda.Auto.Typecheck
CMFFlexAgda.Auto.Typecheck
CMFlex 
1 (Type/Class)Agda.Auto.Typecheck
2 (Data Constructor)Agda.Auto.Typecheck
CMFSemiAgda.Auto.Typecheck
CModeAgda.Auto.Typecheck
CmpElimAgda.Interaction.BasicOps
CmpEqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CmpInTypeAgda.Interaction.BasicOps
CmpLeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CmpLevelsAgda.Interaction.BasicOps
CmpSortsAgda.Interaction.BasicOps
CmpTelesAgda.Interaction.BasicOps
CmpTypesAgda.Interaction.BasicOps
CMRigidAgda.Auto.Typecheck
cnvhAgda.Auto.Convert
CoArbitraryAgda.Utils.QuickCheck
coarbitraryAgda.Utils.QuickCheck
coarbitraryIntegralAgda.Utils.QuickCheck
coarbitraryRealAgda.Utils.QuickCheck
coarbitraryShowAgda.Utils.QuickCheck
CodataAgda.Syntax.Concrete.Definitions
codeAgda.Syntax.Parser.Lexer
CoinductionKit 
1 (Type/Class)Agda.TypeChecking.Rules.Builtin.Coinduction
2 (Data Constructor)Agda.TypeChecking.Rules.Builtin.Coinduction
coinductionKitAgda.TypeChecking.Rules.Builtin.Coinduction
CoInductiveAgda.Syntax.Common
CoinductiveDatatypeAgda.TypeChecking.Coverage
col 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
coldescrAgda.Utils.Warshall
collectAgda.Utils.QuickCheck
colonAgda.Utils.Pretty
cols 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
ColumnAgda.Termination.Lexicographic
columnsAgda.Termination.Lexicographic
comma 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
CommandAgda.Interaction.CommandLine.CommandLine
commandAgda.Interaction.GhciTop
CommandLineOptionsAgda.Interaction.Options
commandLineOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Comment 
1 (Type/Class)Agda.Compiler.Epic.AuxAST
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
commutativeAgda.Utils.TestHelpers
commuteMAgda.Utils.Monad
comp'Agda.Auto.Typecheck
compactPAgda.Utils.Permutation
compareArgsAgda.TypeChecking.Conversion
compareAtomAgda.TypeChecking.Conversion
compareElimsAgda.TypeChecking.Conversion
compareLevelAgda.TypeChecking.UniversePolymorphism
compareSizesAgda.TypeChecking.SizedTypes
compareSortAgda.TypeChecking.Conversion
compareTelAgda.TypeChecking.Conversion
compareTermAgda.TypeChecking.Conversion
compareTerm'Agda.TypeChecking.Conversion
compareTypeAgda.TypeChecking.Conversion
ComparisonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompilationErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompileAgda.Compiler.Epic.CompileState
compile 
1 (Function)Agda.TypeChecking.CompiledClause.Compile
2 (Function)Agda.Compiler.MAlonzo.Compiler
3 (Function)Agda.Compiler.JS.Compiler
compileClauses 
1 (Function)Agda.TypeChecking.CompiledClause.Compile
2 (Function)Agda.Compiler.Epic.FromAgda
CompiledClausesAgda.TypeChecking.CompiledClause
CompiledDataPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compiledEpicAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledEpicPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compiledHaskellAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
compileDir 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
compiledJSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledJSPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compiledModulesAgda.Compiler.Epic.CompileState
CompiledPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
CompiledRepAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledRepresentationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledTypePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compilerMain 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.Epic.Compiler
3 (Function)Agda.Compiler.JS.Compiler
CompileState 
1 (Type/Class)Agda.Compiler.Epic.CompileState
2 (Data Constructor)Agda.Compiler.Epic.CompileState
completeAgda.Termination.CallGraph
composePAgda.Utils.Permutation
composePolAgda.TypeChecking.Polarity
composeRelevanceAgda.TypeChecking.Irrelevance
compressAgda.Interaction.Highlighting.Precise
CompressedFileAgda.Interaction.Highlighting.Precise
computeEdgeAgda.TypeChecking.Positivity
computeNeighbourhoodAgda.TypeChecking.Coverage
ComputeOccurrencesAgda.TypeChecking.Positivity
computeOccurrencesAgda.TypeChecking.Positivity
computePolarityAgda.TypeChecking.Polarity
computeSizeConstraintAgda.TypeChecking.SizedTypes
Con 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Compiler.Epic.AuxAST
3 (Data Constructor)Agda.Syntax.Abstract
conAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConArgTypeAgda.TypeChecking.Positivity
conArityAgda.Compiler.Epic.Interface
conArityAndParsAgda.Compiler.MAlonzo.Compiler
conBranchesAgda.TypeChecking.CompiledClause
conCaseAgda.TypeChecking.CompiledClause
concatargsAgda.Auto.CaseSplit
concatMapMAgda.Utils.Monad
concatOccursAgda.TypeChecking.Positivity
ConcreteDefAgda.Syntax.Common
ConcreteModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
concreteToAbstractAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
concreteToAbstract_Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
conDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
condeclAgda.Compiler.MAlonzo.Compiler
ConElimAgda.TypeChecking.Eliminators
conFreqAgda.TypeChecking.Test.Generators
ConHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
conhqnAgda.Compiler.MAlonzo.Misc
conIndAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
conjoinAgda.Utils.QuickCheck
ConMPAgda.TypeChecking.Coverage.Match
ConName 
1 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Type/Class)Agda.TypeChecking.Test.Generators
3 (Data Constructor)Agda.TypeChecking.Test.Generators
ConnectHandleAgda.Auto.NarrowingSearch
ConP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract
conParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConsAgda.Interaction.EmacsCommand
conSrcConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Const 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
ConstDef 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
Constr 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
Constraint 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.Utils.Warshall
constraintProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Constraints 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.Utils.Warshall
ConstRefAgda.Auto.Syntax
constrGroupAgda.Compiler.Epic.Injection
constrInScopeAgda.Compiler.Epic.CompileState
constrTagsAgda.Compiler.Epic.Interface
Constructor 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Interaction.Highlighting.Precise
5 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constructorArityAgda.Compiler.Epic.CompileState
constructorFormAgda.TypeChecking.Primitive
constructorImpossibleAgda.Auto.Typecheck
ConstructorMismatchAgda.TypeChecking.Rules.LHS.Unify
constructorMismatchAgda.TypeChecking.Rules.LHS.Unify
constructorMismatchHHAgda.TypeChecking.Rules.LHS.Unify
ConstructorNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
ConstructorPatternInWrongDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constructPatsAgda.Auto.Convert
constructsAgda.TypeChecking.Rules.Data
ContAgda.Utils.Monad
containsAbsurdPatternAgda.TypeChecking.Rules.Def
contains_constructorAgda.Auto.Convert
ContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ContextEntryAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
contextOfMetaAgda.Interaction.BasicOps
ContinueAgda.Interaction.CommandLine.CommandLine
continueAfterAgda.Interaction.CommandLine.CommandLine
ContinueInAgda.Interaction.CommandLine.CommandLine
continuousAgda.Syntax.Position, Agda.Interaction.GhciTop
continuousPerLineAgda.Syntax.Position, Agda.Interaction.GhciTop
ContravariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
convertLineEndingsAgda.Utils.Unicode
copyargAgda.Auto.Typecheck
copyScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
costAbsurdLamAgda.Auto.SearchControl
costAddVarDepthAgda.Auto.CaseSplit
costAppConstructorAgda.Auto.SearchControl
costAppConstructorSingleAgda.Auto.SearchControl
costAppExtraRefAgda.Auto.SearchControl
costAppHintAgda.Auto.SearchControl
costAppHintUsedAgda.Auto.SearchControl
costAppRecCallAgda.Auto.SearchControl
costAppRecCallUsedAgda.Auto.SearchControl
costAppVarAgda.Auto.SearchControl
costAppVarUsedAgda.Auto.SearchControl
costCaseSplitHighAgda.Auto.CaseSplit
costCaseSplitLowAgda.Auto.CaseSplit
costCaseSplitVeryHighAgda.Auto.CaseSplit
costEqCongAgda.Auto.SearchControl
costEqEndAgda.Auto.SearchControl
costEqStepAgda.Auto.SearchControl
costEqSymAgda.Auto.SearchControl
costIncreaseAgda.Auto.SearchControl
costInferredTypeUnkownAgda.Auto.SearchControl
costIotaStepAgda.Auto.SearchControl
costLamAgda.Auto.SearchControl
costLamUnfoldAgda.Auto.SearchControl
costPiAgda.Auto.SearchControl
costSortAgda.Auto.SearchControl
costUnificationAgda.Auto.SearchControl
costUnificationOccursAgda.Auto.SearchControl
countAgda.Utils.ReadP
CovariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
cover 
1 (Function)Agda.Utils.QuickCheck
2 (Function)Agda.TypeChecking.Coverage
CoverageCantSplitIrrelevantTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageCantSplitOnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageCantSplitTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageFailureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoveringAgda.TypeChecking.Coverage
CoverMAgda.TypeChecking.Coverage
createInterfaceAgda.Interaction.Imports
createMetaInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
createModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
CSAbsurdAgda.Auto.CaseSplit
CSCtxAgda.Auto.CaseSplit
CSOmittedArgAgda.Auto.CaseSplit
CSPatAgda.Auto.CaseSplit
CSPatConAppAgda.Auto.CaseSplit
CSPatExpAgda.Auto.CaseSplit
CSPatIAgda.Auto.CaseSplit
CSPatVarAgda.Auto.CaseSplit
CSWithAgda.Auto.CaseSplit
cthandlesAgda.Auto.NarrowingSearch
ctparentAgda.Auto.NarrowingSearch
ctpriometaAgda.Auto.NarrowingSearch
CTree 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
ctsubAgda.Auto.NarrowingSearch
Ctx 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ctxEntryAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CtxId 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ctxIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
curDefsAgda.Compiler.MAlonzo.Misc
curFunAgda.Compiler.Epic.CompileState
curHsModAgda.Compiler.MAlonzo.Misc
curIFAgda.Compiler.MAlonzo.Misc
curMNameAgda.Compiler.MAlonzo.Misc
curModule 
1 (Function)Agda.Compiler.Epic.CompileState
2 (Function)Agda.Compiler.JS.Compiler
CurrentDirAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
CurrentInputAgda.Syntax.Parser.Alex
currentModuleAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
currentMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
currentProblemAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
curriedApplyAgda.Compiler.JS.Substitution
curriedLambdaAgda.Compiler.JS.Substitution
curSigAgda.Compiler.MAlonzo.Misc
CyclicModuleDependencyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataAgda.Syntax.Concrete
dataAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataArgOccurrencesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataConsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataDef 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Concrete.Definitions
dataInductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataInfoAgda.TypeChecking.Datatypes
dataIxsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataMustEndInSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataOrRecordTypeAgda.TypeChecking.Rules.LHS.Unify
dataOrRecordType'Agda.TypeChecking.Rules.LHS.Unify
dataOrRecordTypeHHAgda.TypeChecking.Rules.LHS.Unify
dataParametersAgda.Compiler.Epic.Forcing
dataParametersTCMAgda.Compiler.Epic.Forcing
dataParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataPolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataSig 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
dataSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Datatype 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DatatypeInfoAgda.TypeChecking.Datatypes
datatypeIxsAgda.TypeChecking.Datatypes
datatypeIxTelAgda.TypeChecking.Datatypes
datatypeNameAgda.TypeChecking.Datatypes
datatypeParsAgda.TypeChecking.Datatypes
datatypeParTelAgda.TypeChecking.Datatypes
dbraces 
1 (Function)Agda.Syntax.Concrete.Pretty
2 (Function)Agda.TypeChecking.Pretty
DConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DDotAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
deBruijnIndexAgda.Interaction.MakeCase
DeBruijnPatAgda.Termination.TermCheck
debugAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad
decDigitAgda.Utils.Char
Declaration 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
DeclarationExceptionAgda.Syntax.Concrete.Definitions
DeclarationPanicAgda.Syntax.Concrete.Definitions
DeclContAgda.Auto.Syntax
DeclInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
declNameAgda.Syntax.Info
declRangeAgda.Syntax.Info
declsForPrimAgda.Compiler.MAlonzo.Primitives
decodeAgda.TypeChecking.Serialise
DecodedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
decodeFileAgda.TypeChecking.Serialise
decompressAgda.Interaction.Highlighting.Precise
decrAgda.Termination.CallGraph
decrConfAgda.TypeChecking.Test.Generators
decreasingAgda.Termination.CallGraph
Def 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Abstract
defAbstract 
1 (Function)Agda.Syntax.Info
2 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defAccessAgda.Syntax.Info
DefArgAgda.TypeChecking.Positivity
defArgsAgda.TypeChecking.MetaVars.Occurs
DefaultAgda.Compiler.Epic.AuxAST
defaultArgAgda.Syntax.Common
defaultDisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defaultFixityAgda.Syntax.Fixity
defaultFixity'Agda.Syntax.Fixity
defaultFrequenciesAgda.TypeChecking.Test.Generators
defaultImportDirAgda.Syntax.Concrete
defaultNotationAgda.Syntax.Notation
defaultOptionsAgda.Interaction.Options
defaultParseFlagsAgda.Syntax.Parser.Monad
defaultVerbosityAgda.Interaction.Options
defClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCompiledRepAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDelayed 
1 (Function)Agda.Compiler.Epic.Interface
2 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDisplayAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefElimAgda.TypeChecking.Eliminators
defEpicDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defFixityAgda.Syntax.Info
defFreqAgda.TypeChecking.Test.Generators
DefinedNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
DefInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
defInfoAgda.Syntax.Info
DefinitelyAgda.TypeChecking.Rules.LHS.Unify
DefinitionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definition 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
DefinitionIsIrrelevantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefinitionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definitions 
1 (Function)Agda.Compiler.Epic.Interface
2 (Function)Agda.Compiler.MAlonzo.Compiler
definitionSiteAgda.Interaction.Highlighting.Precise
defIsRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defJSDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Defn 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defn 
1 (Function)Agda.Compiler.JS.Syntax
2 (Function)Agda.Compiler.JS.Compiler
DefName 
1 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Type/Class)Agda.TypeChecking.Test.Generators
3 (Data Constructor)Agda.TypeChecking.Test.Generators
defName 
1 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Function)Agda.Compiler.Epic.Primitive
DefNodeAgda.TypeChecking.Positivity
defnParsAgda.Compiler.Epic.Smashing
DefPAgda.Syntax.Abstract
defProjectionAgda.Compiler.JS.Compiler
defRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefShAgda.TypeChecking.Rules.LHS.Unify
defTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Delayed 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
deleteAgda.Utils.VarSet
DependentAgda.Interaction.GhciTop
depthofvarAgda.Auto.CaseSplit
derefAgda.Utils.Pointer
detecteliminandAgda.Auto.Syntax
detectsemiflexAgda.Auto.Syntax
diagonal 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
diffAgda.Compiler.Epic.Erasure
DifferentAritiesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
disableDisplayFormsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
disjoinAgda.Utils.QuickCheck
DisplayAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayErrorAndExitAgda.Interaction.GhciTop
DisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayFormAgda.TypeChecking.DisplayForm
displayFormsEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
displayStatusAgda.Interaction.GhciTop
DisplayTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
display_infoAgda.Interaction.GhciTop
display_info'Agda.Interaction.GhciTop
display_infoDAgda.Interaction.GhciTop
DistAgda.Utils.Warshall
DistanceAgda.Utils.Warshall
distinctAgda.Utils.List
divConfAgda.TypeChecking.Test.Generators
DLubAgda.Syntax.Internal
dLubAgda.TypeChecking.Substitute
Doc 
1 (Type/Class)Agda.Utils.Pretty
2 (Type/Class)Agda.TypeChecking.Pretty
doclosAgda.Auto.Syntax
DoesNotConstructAnElementOfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
doEtaContractImplicitAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DomainFree 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
domainFreeAgda.TypeChecking.Rules.Term
DomainFull 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
DoneAgda.TypeChecking.CompiledClause
DontCare 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Abstract
dontCareAgda.Auto.Syntax
dontEtaContractImplicitAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontExpandLastAgda.TypeChecking.Rules.Term
DontKnow 
1 (Data Constructor)Agda.TypeChecking.Patterns.Match
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Unify
DontOpenAgda.Syntax.Concrete
dontReifyInteractionPointsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontTouchMeAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
DoOpenAgda.Syntax.Concrete
DotAgda.Syntax.Concrete
DotMAgda.Interaction.Highlighting.Dot
DotP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Abstract
DotPatternCtxAgda.Syntax.Fixity
DotPatternInstAgda.TypeChecking.Rules.LHS
dotPatternInstsAgda.TypeChecking.Rules.LHS
DotState 
1 (Type/Class)Agda.Interaction.Highlighting.Dot
2 (Data Constructor)Agda.Interaction.Highlighting.Dot
DottedPatternAgda.Interaction.Highlighting.Precise
dottifyAgda.Interaction.Highlighting.Dot
DotVarsAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
dotVarsAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
DoubleAgda.Compiler.JS.Syntax
doubleAgda.Utils.Pretty
doubleblockAgda.Auto.NarrowingSearch
doubleQuotesAgda.Utils.Pretty
doWorkOnTypesAgda.TypeChecking.Irrelevance
DPIAgda.TypeChecking.Rules.LHS
dropDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
drophidAgda.Auto.CaseSplit
dropIAgda.Syntax.Position, Agda.Interaction.GhciTop
dryInstantiateAgda.Auto.NarrowingSearch
dsConnectionAgda.Interaction.Highlighting.Dot
dsModulesAgda.Interaction.Highlighting.Dot
dsNameSupplyAgda.Interaction.Highlighting.Dot
dsubnameAgda.Compiler.MAlonzo.Misc
DTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dummyAgda.Compiler.MAlonzo.Misc
dummyLambdaAgda.Compiler.JS.Compiler
DuplicateBuiltinBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateConstructorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DWithAppAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eatNextCharAgda.Syntax.Parser.LookAhead
Edge 
1 (Type/Class)Agda.TypeChecking.Positivity
2 (Data Constructor)Agda.TypeChecking.Positivity
edges 
1 (Function)Agda.Utils.Graph
2 (Function)Agda.Utils.Warshall
EEAgda.Auto.Syntax
EInterface 
1 (Type/Class)Agda.Compiler.Epic.Interface
2 (Data Constructor)Agda.Compiler.Epic.Interface
EitherOrBothAgda.Utils.Map
ElAgda.Syntax.Internal
elAgda.TypeChecking.Primitive
elementsAgda.Utils.QuickCheck
ElimAgda.Syntax.Internal
ElimCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ElimViewAgda.TypeChecking.Eliminators
elimViewAgda.TypeChecking.Eliminators
EllipsisAgda.Syntax.Concrete
ElrAgda.Auto.Syntax
ElseShAgda.TypeChecking.Rules.LHS.Unify
EmbPrjAgda.TypeChecking.Serialise
empAgda.Compiler.JS.Substitution
empty 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Pretty
3 (Function)Agda.Utils.Graph
4 (Function)Agda.Utils.Trie
5 (Function)Agda.Termination.CallGraph
6 (Function)Agda.TypeChecking.Pretty
emptyCAgda.Compiler.Epic.Injection
emptyConstraintsAgda.Utils.Warshall
emptyLayoutAgda.Syntax.Parser.Layout
emptyNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptyScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptyScopeInfoAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptySignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
emptySolutionAgda.Utils.Warshall
EmptyTelAgda.Syntax.Internal
emptyUEnvAgda.TypeChecking.Rules.LHS.Unify
emptyUOutputAgda.TypeChecking.Rules.LHS.Unify
emptyUStateAgda.TypeChecking.Rules.LHS.Unify
empty_layoutAgda.Syntax.Parser.Lexer
enableDisplayFormsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
encodeAgda.TypeChecking.Serialise
encodeFileAgda.TypeChecking.Serialise
encodeModuleNameAgda.Compiler.MAlonzo.Encode
endAgda.Syntax.Parser.LexActions
endByAgda.Utils.ReadP
endBy1Agda.Utils.ReadP
endWithAgda.Syntax.Parser.LexActions
end_Agda.Syntax.Parser.LexActions
ensureFileLoadedAgda.Interaction.GhciTop
enterClosureAgda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad
EnvAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
envAbstractModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envActiveProblemsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAnonymousModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCurrentModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envDisplayFormsEnabledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envEtaContractImplicitAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envImportPathAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envLetBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envMutualBlockAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envReifyInteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envSolvingConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envTopLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eofAgda.Syntax.Parser.LexActions
EpicAgda.Interaction.GhciTop
EpicCodeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
epicErrorAgda.Compiler.Epic.CompileState
EpicFunAgda.Compiler.Epic.AuxAST
eqelrAgda.Auto.CaseSplit
eqGroupsAgda.Compiler.Epic.Injection
eqrcBeginAgda.Auto.Syntax
eqrcCongAgda.Auto.Syntax
eqrcEndAgda.Auto.Syntax
eqrcIdAgda.Auto.Syntax
eqrcStepAgda.Auto.Syntax
eqrcSymAgda.Auto.Syntax
EqReasoningConsts 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
EqReasoningStateAgda.Auto.Syntax
EqRSChainAgda.Auto.Syntax
EqRSNoneAgda.Auto.Syntax
EqRSPrf1Agda.Auto.Syntax
EqRSPrf2Agda.Auto.Syntax
EqRSPrf3Agda.Auto.Syntax
EqualAgda.TypeChecking.Rules.LHS.Unify
equalAtomAgda.TypeChecking.Conversion
EqualityAgda.TypeChecking.Rules.LHS.Unify
equalLevelAgda.TypeChecking.Conversion
equalsAgda.Utils.Pretty
equalSortAgda.TypeChecking.Conversion
equalTermAgda.TypeChecking.Conversion
equalTypeAgda.TypeChecking.Conversion
ErasureAgda.Compiler.Epic.Erasure
erasureAgda.Compiler.Epic.Erasure
ErasureState 
1 (Type/Class)Agda.Compiler.Epic.Erasure
2 (Data Constructor)Agda.Compiler.Epic.Erasure
eriEqRStateAgda.Auto.SearchControl
eriInfTypeUnknownAgda.Auto.SearchControl
eriIotaStepAgda.Auto.SearchControl
eriIsEliminandAgda.Auto.SearchControl
eriMainAgda.Auto.SearchControl
eriPickSubsVarAgda.Auto.SearchControl
eriUnifsAgda.Auto.SearchControl
eriUsedVarsAgda.Auto.SearchControl
errErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
errHighlightingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
errInputAgda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
errMsgAgda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
Error 
1 (Data Constructor)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
errorTitleAgda.Interaction.GhciTop
errPosAgda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
errPrevTokenAgda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
escapeAgda.Interaction.Highlighting.Vim
escapeContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
escChrAgda.Compiler.JS.Parser
etaContractAgda.TypeChecking.EtaContract
etaContractBodyAgda.Auto.Convert
etaContractRecordAgda.TypeChecking.Records
EtaExpandAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
etaExpandAgda.Compiler.Epic.Static
etaExpandBlockedAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandClauseAgda.TypeChecking.Positivity
etaExpandListenersAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandMetaSafeAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandRecordAgda.TypeChecking.Records
etaOnceAgda.TypeChecking.EtaContract
EtaPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
ETel 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
evalInAgda.Interaction.CommandLine.CommandLine
evalInCurrentAgda.Interaction.BasicOps
evalInMetaAgda.Interaction.BasicOps
evalTermAgda.Interaction.CommandLine.CommandLine
evaluateCCAgda.Compiler.Epic.Static
evaluateTermAgda.Compiler.Epic.Static
everythingButAgda.Utils.Generics
everythingInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
everywhereBut'Agda.Utils.Generics
everywhereButM'Agda.Utils.Generics
ExceptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExceptionT 
1 (Type/Class)Agda.TypeChecking.Monad.Exception
2 (Data Constructor)Agda.TypeChecking.Monad.Exception
ExitCodeAgda.Interaction.CommandLine.CommandLine
Exp 
1 (Type/Class)Agda.Auto.Syntax
2 (Type/Class)Agda.Compiler.JS.Syntax
expAgda.Compiler.JS.Parser
exp0Agda.Compiler.JS.Parser
exp1Agda.Compiler.JS.Parser
exp2Agda.Compiler.JS.Parser
exp2'Agda.Compiler.JS.Parser
exp3Agda.Compiler.JS.Parser
exp3'Agda.Compiler.JS.Parser
expandbindAgda.Auto.NarrowingSearch
expandCatchAllsAgda.TypeChecking.CompiledClause.Compile
expandExpAgda.Auto.Syntax
ExpandHiddenAgda.TypeChecking.Rules.Term
ExpandLastAgda.TypeChecking.Rules.Term
expandLitPatternAgda.TypeChecking.Rules.LHS.Split
expandPAgda.Utils.Permutation
expectFailureAgda.Utils.QuickCheck
expNameAgda.Compiler.JS.Syntax
Export 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
exportedNamesInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
exports 
1 (Function)Agda.Compiler.JS.Syntax
2 (Function)Agda.Compiler.JS.Pretty
Expr 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Compiler.Epic.AuxAST
3 (Type/Class)Agda.Syntax.Abstract
ExpRefInfo 
1 (Type/Class)Agda.Auto.SearchControl
2 (Data Constructor)Agda.Auto.SearchControl
ExprHoleAgda.Syntax.Notation
ExprInfoAgda.Syntax.Info
exprInfoAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
exprParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser, Agda.Interaction.GhciTop
ExprRangeAgda.Syntax.Info
ExprSourceAgda.Syntax.Info
ExprViewAgda.Syntax.Concrete.Operators.Parser
exprViewAgda.Syntax.Concrete.Operators.Parser
extendConfAgda.TypeChecking.Test.Generators
ExtendedLam 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
ExtendedLambdaAgda.Interaction.MakeCase
extendlambdanameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
extendSolutionAgda.Utils.Warshall
ExtendTelAgda.Syntax.Internal
extendWithTelConfAgda.TypeChecking.Test.Generators
extQAgda.Utils.Generics
extractblkinfosAgda.Auto.NarrowingSearch
extractNthElementAgda.Utils.List
extractNthElement'Agda.Utils.List
extrarefAgda.Auto.SearchControl
FailAgda.TypeChecking.CompiledClause
FailedAgda.Auto.NarrowingSearch
failOnExceptionAgda.Interaction.Exceptions, Agda.Interaction.GhciTop
FailureAgda.Utils.QuickCheck
fakeDAgda.Compiler.MAlonzo.Misc
fakeDQAgda.Compiler.MAlonzo.Misc
fakeDSAgda.Compiler.MAlonzo.Misc
fakeExpAgda.Compiler.MAlonzo.Misc
fakeTypeAgda.Compiler.MAlonzo.Misc
fastDistinctAgda.Utils.List
fcatAgda.Utils.Pretty
fCtxAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Field 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Interaction.Highlighting.Precise
fieldAgda.Compiler.JS.Parser
FieldOutsideRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Fields 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FileAgda.Interaction.Highlighting.Precise
FileNotFoundAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
filePathAgda.Utils.FileName
filterKeysAgda.Utils.Map
filterScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
finallyAgda.Utils.Monad
findClauseAgda.Interaction.MakeCase
findClauseDeepAgda.Auto.Convert
FindErrorAgda.Interaction.FindFile
findErrorToTypeErrorAgda.Interaction.FindFile
findFileAgda.Interaction.FindFile
findFile'Agda.Interaction.FindFile
findFile''Agda.Interaction.FindFile
findIdxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
findInjectionAgda.Compiler.Epic.Injection
FindInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FindInScopeOFAgda.Interaction.BasicOps
findInterfaceFileAgda.Interaction.FindFile
findMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
findPathAgda.Utils.Graph
findpermAgda.Auto.CaseSplit
findPositionAgda.Compiler.Epic.Forcing
findPossibleRecordsAgda.TypeChecking.Records
FiniteAgda.Utils.Warshall
fIntegerAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fInteractionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
firstPartAgda.TypeChecking.Telescope
fitsInAgda.TypeChecking.Rules.Data
fixAgda.Compiler.JS.Substitution
Fixed 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
FixityAgda.Syntax.Fixity
Fixity' 
1 (Type/Class)Agda.Syntax.Fixity
2 (Data Constructor)Agda.Syntax.Fixity
fixityLevelAgda.Syntax.Fixity
fixSizeAgda.TypeChecking.Test.Generators
fixSizeConfAgda.TypeChecking.Test.Generators
FlagAgda.Interaction.Options
flattenSubstitutionAgda.TypeChecking.Rules.LHS.Unify
flattenTelAgda.TypeChecking.Telescope
Flex 
1 (Data Constructor)Agda.Utils.Warshall
2 (Data Constructor)Agda.TypeChecking.MetaVars.Occurs
FlexibleAgda.TypeChecking.Free
flexiblePatternsAgda.TypeChecking.Rules.LHS
flexibleVariablesAgda.TypeChecking.SizedTypes
FlexibleVarsAgda.TypeChecking.Rules.LHS.Problem
flexibleVarsAgda.TypeChecking.Free
FlexIdAgda.Utils.Warshall
flexScopeAgda.Utils.Warshall
floatAgda.Utils.Pretty
fmapMAgda.Utils.Monad
fMetaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fmExpAgda.Auto.Convert
fmExpsAgda.Auto.Convert
fmLevelAgda.Auto.Convert
FModeAgda.Auto.Syntax
fmTypeAgda.Auto.Convert
fMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Focus 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
focusConAgda.TypeChecking.Rules.LHS.Problem
focusConArgsAgda.TypeChecking.Rules.LHS.Problem
focusDatatypeAgda.TypeChecking.Rules.LHS.Problem
focusHoleIxAgda.TypeChecking.Rules.LHS.Problem
focusIndicesAgda.TypeChecking.Rules.LHS.Problem
focusOutPatAgda.TypeChecking.Rules.LHS.Problem
focusParamsAgda.TypeChecking.Rules.LHS.Problem
focusRangeAgda.TypeChecking.Rules.LHS.Problem
focusTypeAgda.TypeChecking.Rules.LHS.Problem
foldTermAgda.Syntax.Internal.Generic
followedByAgda.Syntax.Parser.LexActions
forAllAgda.Utils.QuickCheck
forAllShrinkAgda.Utils.QuickCheck
force 
1 (Function)Agda.Syntax.Strict
2 (Function)Agda.TypeChecking.Forcing
forceConstrsAgda.Compiler.Epic.ForceConstrs
Forced 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Compiler.Epic.Interface
3 (Data Constructor)Agda.Compiler.Epic.Interface
forcedAgda.Compiler.Epic.Interface
ForcedArgsAgda.Compiler.Epic.Interface
forcedArgsAgda.Compiler.Epic.Interface
forceDataAgda.TypeChecking.Rules.Data
forcedExprAgda.Compiler.Epic.Forcing
forcedVariablesAgda.TypeChecking.Forcing
forceFunAgda.Compiler.Epic.ForceConstrs
forceHomAgda.TypeChecking.Rules.LHS.Unify
forceMAgda.Utils.Monad
forgetMAgda.Utils.Monad
fProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FreeAgda.TypeChecking.Free
freeIn 
1 (Function)Agda.TypeChecking.Free
2 (Function)Agda.Auto.Convert
freeInIgnoringSortsAgda.TypeChecking.Free
FreeVarsAgda.TypeChecking.Free
freeVarsAgda.TypeChecking.Free
freevarsAgda.Auto.CaseSplit
freeVarsToApplyAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
freezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
FreqsAgda.TypeChecking.Test.Generators
FrequenciesAgda.TypeChecking.Test.Generators
frequencyAgda.Utils.QuickCheck
FreshAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
freshAgda.Utils.Fresh
freshAbstractNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshAbstractName_Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshAbstractQNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
freshNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshNoNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
freshNoName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
FreshThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fromAgda.Interaction.Highlighting.Range
fromAgdaAgda.Compiler.Epic.FromAgda
fromDiagonalsAgda.Termination.Lexicographic
fromHomAgda.TypeChecking.Rules.LHS.Unify
fromIndexList 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
fromJustAgda.Utils.Maybe
fromList 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Graph
3 (Function)Agda.Termination.CallGraph
fromLists 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
fromLiteralAgda.TypeChecking.Primitive
fromMaybeAgda.Utils.Maybe
fromMaybeMAgda.Utils.Maybe
frommyAgda.Auto.Convert
frommyClauseAgda.Auto.Convert
frommyExpAgda.Auto.Convert
frommyExpsAgda.Auto.Convert
frommyTypeAgda.Auto.Convert
fromOrdinaryAgda.Syntax.Concrete
fromReducedTermAgda.TypeChecking.Primitive
FromTermAgda.TypeChecking.Primitive
fromTermAgda.TypeChecking.Primitive
FromTermFunctionAgda.TypeChecking.Primitive
Frozen 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fsep 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
fullRenderAgda.Utils.Pretty
Fun 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Type/Class)Agda.Compiler.Epic.AuxAST
3 (Data Constructor)Agda.Compiler.Epic.AuxAST
4 (Data Constructor)Agda.Syntax.Abstract
5 (Type/Class)Agda.TypeChecking.Primitive
funAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funArgOccurrencesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funArgsAgda.Compiler.Epic.AuxAST
FunClauseAgda.Syntax.Concrete
funClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funCommentAgda.Compiler.Epic.AuxAST
funCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Function 
1 (Data Constructor)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
functionAgda.Compiler.JS.Parser
FunctionCtxAgda.Syntax.Fixity
FunctionDefAgda.Interaction.MakeCase
FunctionInverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
functionInverseAgda.TypeChecking.Injectivity
FunctionSpaceDomainCtxAgda.Syntax.Fixity
FunDef 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Concrete.Definitions
funDelayedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funEpicCodeAgda.Compiler.Epic.AuxAST
funExprAgda.Compiler.Epic.AuxAST
funFreqAgda.TypeChecking.Test.Generators
funInlineAgda.Compiler.Epic.AuxAST
funInvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funNameAgda.Compiler.Epic.AuxAST
funPolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funQNameAgda.Compiler.Epic.AuxAST
funsAgda.Compiler.Epic.Erasure
FunShAgda.TypeChecking.Rules.LHS.Unify
FunSigAgda.Syntax.Concrete.Definitions
funStaticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fuseRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
fuseRangesAgda.Syntax.Position, Agda.Interaction.GhciTop
FVAgda.TypeChecking.Free
fvAgda.Compiler.Epic.AuxAST
FVsAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
fwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
gApplyAgda.TypeChecking.Primitive
gatherAgda.Utils.ReadP
GaveUpAgda.Utils.QuickCheck
GenAgda.Utils.QuickCheck
genArgsAgda.TypeChecking.Test.Generators
GenCAgda.TypeChecking.Test.Generators
genCAgda.TypeChecking.Test.Generators
genConfAgda.TypeChecking.Test.Generators
generateDotAgda.Interaction.Highlighting.Dot
generateErrorInfoAgda.Interaction.Highlighting.Generate
generateHTMLAgda.Interaction.Highlighting.HTML
generateSyntaxInfoAgda.Interaction.Highlighting.Generate
generateVimFileAgda.Interaction.Highlighting.Vim
genericElemIndexAgda.Utils.List
GenericErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
GenericMAgda.Utils.Generics
GenericQAgda.Utils.Generics
GenericSplitErrorAgda.TypeChecking.Coverage
GenericTAgda.Utils.Generics
GenericUnifyExceptionAgda.TypeChecking.Rules.LHS.Unify
genGraphAgda.Utils.Warshall
genGraph_Agda.Utils.Warshall
GenPartAgda.Syntax.Notation
genPathAgda.Utils.Warshall
getAgda.Utils.ReadP
getAllArgsAgda.Auto.Typecheck
getAllConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
getAnonymousVariablesAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
getArgOccurrenceAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getArityAgda.TypeChecking.Polarity
getAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
getblksAgda.Auto.CaseSplit
getBrVarsAgda.Compiler.Epic.AuxAST
getBuiltinAgda.TypeChecking.Monad.Builtin
getBuiltin'Agda.TypeChecking.Monad.Builtin
getBuiltinsAgda.Compiler.Epic.Primitive
getBuiltinThingAgda.TypeChecking.Monad.Builtin
getConArityAgda.Compiler.Epic.CompileState
getConDataAgda.Compiler.Epic.CompileState
getConstAgda.Auto.Convert
getConstInfoAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getConstraintsAgda.Interaction.BasicOps
getConstraintsForProblemAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
getConstrTagAgda.Compiler.Epic.CompileState
getConstrTag'Agda.Compiler.Epic.CompileState
getConstructorDataAgda.TypeChecking.Datatypes
getContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextArgsAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextIdAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextPrecedenceAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getContextTelescopeAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextTermsAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getCurrentFileAgda.Interaction.GhciTop
getCurrentModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getCurrentRangeAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
getCurrentScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getDataConAgda.Compiler.Epic.CompileState
getDatatypeAgda.Auto.Typecheck
getDatatypeInfoAgda.TypeChecking.Datatypes
getDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getDecodedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getDefArityAgda.TypeChecking.Positivity
getDefFreeVarsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
GetDefInfoAgda.Syntax.Abstract
getDefInfoAgda.Syntax.Abstract
getDelayedAgda.Compiler.Epic.CompileState
getdfvAgda.Auto.Convert
getEnvAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
getEqsAgda.Auto.Convert
getExtLambdaTeleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getFixityAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getForcedArgsAgda.Compiler.Epic.CompileState
getHaskellImportsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getHsTypeAgda.Compiler.HaskellTypes
getHsVarAgda.Compiler.HaskellTypes
getImportedSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getImportPathAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getImportsAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getIncludeDirsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getinfoAgda.Auto.SearchControl
getInputAgda.Syntax.Parser.LookAhead
getInputFileAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getInstantiatedMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionPointsAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionScopeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInterfaceAgda.Interaction.Imports
getInterface'Agda.Interaction.Imports
getLexInputAgda.Syntax.Parser.Alex
getLexStateAgda.Syntax.Parser.Monad
getLocalVarsAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getMainAgda.Compiler.Epic.CompileState
getMetaAgda.Auto.Convert
getMetaEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaListenersAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaPriorityAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaSigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaStoreAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getModuleFreeVarsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getMutualBlocksAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
getNamedScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
getNArgsAgda.Auto.Typecheck
getNatishAgda.Compiler.Epic.NatDetection
getOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
getOpenMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getParseFlagsAgda.Syntax.Parser.Monad
getParseIntervalAgda.Syntax.Parser.Monad
getPolarityAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getPolarity'Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getPrimitiveAgda.TypeChecking.Monad.Builtin
getRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
getRangesAgda.Interaction.Highlighting.Range
getRangesAAgda.Interaction.Highlighting.Range
getRecordConstructorAgda.TypeChecking.Records
getRecordConstructorTypeAgda.TypeChecking.Records
getRecordDefAgda.TypeChecking.Records
getRecordFieldNamesAgda.TypeChecking.Records
getRecordFieldTypesAgda.TypeChecking.Records
getScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getSecFreeVarsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getsEIAgda.Compiler.Epic.CompileState
getSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getSizeConstraintsAgda.TypeChecking.SizedTypes
getSizeMetasAgda.TypeChecking.SizedTypes
getSolvedInteractionPointsAgda.Interaction.BasicOps
getSortAgda.Syntax.Internal
getStatisticsAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
getTypeAgda.Compiler.Epic.CompileState
getVarInfoAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getVerbosityAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getVisitedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getVisitedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
giveAgda.Interaction.BasicOps
giveExprAgda.Interaction.BasicOps
giveMetaAgda.Interaction.CommandLine.CommandLine
give_genAgda.Interaction.GhciTop
give_gen'Agda.Interaction.GhciTop
GlobalAgda.Compiler.JS.Syntax
globalAgda.Compiler.JS.Compiler
global'Agda.Compiler.JS.Compiler
GlobalId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
globalidAgda.Compiler.JS.Parser
GlobalsAgda.Compiler.JS.Syntax
globalsAgda.Compiler.JS.Syntax
GMAgda.Utils.Warshall
gmapMAgda.Utils.Generics
gmapQAgda.Utils.Generics
gmapTAgda.Utils.Generics
GoalCommandAgda.Interaction.GhciTop
goal_commandAgda.Interaction.GhciTop
goIrrelevantAgda.TypeChecking.MetaVars.Occurs
gpiAgda.TypeChecking.Primitive
Graph 
1 (Type/Class)Agda.Utils.Graph
2 (Data Constructor)Agda.Utils.Graph
3 (Type/Class)Agda.Utils.Warshall
4 (Data Constructor)Agda.Utils.Warshall
graphAgda.Utils.Warshall
groupBy'Agda.Utils.List
groupOnAgda.Utils.List
growGraphAgda.Utils.Graph
growingElementsAgda.Utils.QuickCheck
gshow'Agda.Compiler.MAlonzo.Misc
GuardAgda.Interaction.BasicOps
guardConstraintAgda.TypeChecking.Constraints
GuardedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
handleParseExceptionAgda.Interaction.Exceptions, Agda.Interaction.GhciTop
HandleSolAgda.Auto.NarrowingSearch
hangAgda.Utils.Pretty
hasBadRigidAgda.TypeChecking.MetaVars.Occurs
hasCompiledDataAgda.Compiler.MAlonzo.Primitives
HasFreshAgda.Utils.Fresh
hashAgda.Utils.Hash
hasInputFileAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
HaskellCodeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
HaskellKindAgda.Compiler.HaskellTypes
haskellKindAgda.Compiler.HaskellTypes
HaskellRepresentationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
HaskellTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
haskellTypeAgda.Compiler.HaskellTypes
HasPolarityAgda.TypeChecking.Polarity
HasRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
HasTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
hasUniversePolymorphismAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
hasVerbosityAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
HasZeroAgda.Termination.Semiring
haveSizedTypesAgda.TypeChecking.SizedTypes
hcatAgda.Utils.Pretty
head''Agda.Compiler.Epic.Primitive
HeadNormalAgda.Interaction.BasicOps
headSymbolAgda.TypeChecking.Injectivity
helpAgda.Interaction.CommandLine.CommandLine
hequalMetavarAgda.Auto.NarrowingSearch
HereAgda.TypeChecking.Positivity
hereAgda.TypeChecking.Positivity
HetAgda.TypeChecking.Rules.LHS.Unify
HeterogeneousEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
hexDigitAgda.Utils.Char
hGetContentsAgda.Utils.IO.Locale
HI 
1 (Type/Class)Agda.Auto.CaseSplit
2 (Data Constructor)Agda.Auto.CaseSplit
Hidden 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Common
HiddenArgAgda.Syntax.Concrete
hiddenArgumentCtxAgda.Syntax.Fixity
HiddenArgVAgda.Syntax.Concrete.Operators.Parser
hiddenFreqAgda.TypeChecking.Test.Generators
HiddenFreqs 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
hiddenFreqsAgda.TypeChecking.Test.Generators
HiddenPAgda.Syntax.Concrete
hideAgda.Syntax.Common
hideAndRelParamsAgda.TypeChecking.Irrelevance
Hiding 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Concrete
HighlightingInfoAgda.Interaction.Highlighting.Precise
highMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
HintModeAgda.Auto.Syntax
HMNormalAgda.Auto.Syntax
HMRecCallAgda.Auto.Syntax
HNALConParAgda.Auto.Syntax
HNALConsAgda.Auto.Syntax
HNALNilAgda.Auto.Syntax
HNAppAgda.Auto.Syntax
HNArgListAgda.Auto.Syntax
hnarglistAgda.Auto.Typecheck
hnbAgda.Auto.Typecheck
hncAgda.Auto.Typecheck
HNDoneAgda.Auto.Typecheck
HNExpAgda.Auto.Syntax
HNLamAgda.Auto.Syntax
HNMetaAgda.Auto.Typecheck
hnnAgda.Auto.Typecheck
hnn'Agda.Auto.Typecheck
HNNBlksAgda.Auto.Typecheck
hnn_blksAgda.Auto.Typecheck
hnn_checkstepAgda.Auto.Typecheck
HNPiAgda.Auto.Syntax
HNResAgda.Auto.Typecheck
HNSortAgda.Auto.Syntax
Hole 
1 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Internal.Pattern
holeAgda.Syntax.Parser.Comments
HoleNameAgda.Syntax.Notation
holeNameAgda.Syntax.Notation
holesAgda.Utils.List
holeTargetAgda.Syntax.Notation
HomAgda.TypeChecking.Rules.LHS.Unify
HomHetAgda.TypeChecking.Rules.LHS.Unify
hPiAgda.TypeChecking.Primitive
hPutStrAgda.Utils.IO.UTF8
hsAppAgda.Compiler.HaskellTypes
hsCastAgda.Compiler.MAlonzo.Compiler
hsCast'Agda.Compiler.MAlonzo.Compiler
hsCoerceAgda.Compiler.MAlonzo.Compiler
HsDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
hsep 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
hsForallAgda.Compiler.HaskellTypes
hsFunAgda.Compiler.HaskellTypes
hsKFunAgda.Compiler.HaskellTypes
hslitAgda.Compiler.MAlonzo.Compiler
hsStarAgda.Compiler.HaskellTypes
HsTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
hsUnitAgda.Compiler.HaskellTypes
hsVarAgda.Compiler.HaskellTypes
hsVarUQAgda.Compiler.MAlonzo.Misc
iBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ICArgListAgda.Auto.Syntax
ICExpAgda.Auto.Syntax
icnvhAgda.Auto.Convert
Id 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IdentAgda.Syntax.Concrete
identifier 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Parser.LexActions
identityAgda.Utils.TestHelpers
IdentPAgda.Syntax.Concrete
idPAgda.Utils.Permutation
IdPartAgda.Syntax.Notation
idSubAgda.TypeChecking.Substitute
iEndAgda.Syntax.Position, Agda.Interaction.GhciTop
If 
1 (Data Constructor)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.Epic.AuxAST
ifBlockAgda.Compiler.JS.Parser
ifCleanAgda.TypeChecking.Rules.LHS.Unify
ifMAgda.Utils.Monad
ifNoConstraintsAgda.TypeChecking.Constraints
ifNoConstraints_Agda.TypeChecking.Constraints
IFSNoCandidateInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IgnoreAbstractModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreAbstractModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ignoreBlockingAgda.Syntax.Internal
ignoreForced 
1 (Function)Agda.TypeChecking.Irrelevance
2 (Function)Agda.Compiler.Epic.Erasure
ignoreInterfacesAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
ignoreReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHaskellImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHighlightingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ihnameAgda.Compiler.MAlonzo.Misc
iImportedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iInsideScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IlltypedPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IMAgda.Interaction.Monad
iModuleNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ImpInsertAgda.TypeChecking.Implicit
impInsertAgda.TypeChecking.Implicit
ImplicitInsertionAgda.TypeChecking.Implicit
ImplicitPAgda.Syntax.Abstract
Import 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
ImportDirective 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
importDirRangeAgda.Syntax.Concrete
ImportedModuleAgda.Syntax.Concrete
importedModulesAgda.Compiler.Epic.CompileState
ImportedName 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
importedNameAgda.Syntax.Concrete
ImportedNSAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ImportPragmaAgda.Syntax.Concrete
importsAgda.Compiler.MAlonzo.Compiler
importsForPrimAgda.Compiler.MAlonzo.Primitives
IMPOSSIBLEAgda.Compiler.Epic.AuxAST
Impossible 
1 (Type/Class)Agda.Utils.Impossible
2 (Data Constructor)Agda.Utils.Impossible
ImpossiblePragmaAgda.Syntax.Concrete
impossibleTermAgda.Syntax.Internal
impossibleTestAgda.ImpossibleTest
imp_dirAgda.Syntax.Parser.Lexer
inAbstractModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
incAgda.Utils.Warshall
InClauseAgda.TypeChecking.Positivity
IncompletePatternAgda.Interaction.Highlighting.Precise
IncompletePatternMatchingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inConcreteModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
InDefOfAgda.TypeChecking.Positivity
indentAgda.Utils.String
IndependenceAgda.Interaction.GhciTop
independenceAgda.Interaction.GhciTop
IndependentAgda.Interaction.GhciTop
Index 
1 (Data Constructor)Agda.Utils.Suffix
2 (Type/Class)Agda.Termination.CallGraph
IndexFreeInParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndexVariablesNotDistinctAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndicesNotConstructorApplicationsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InductionAgda.Syntax.Common
InductiveAgda.Syntax.Common
InfAgda.Syntax.Internal
inferableAgda.Compiler.Epic.Smashing
inferableTermAgda.Compiler.Epic.Smashing
InferDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferDefAgda.TypeChecking.Rules.Term
InferExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferExprAgda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop
inferHeadAgda.TypeChecking.Rules.Term
inferMetaAgda.TypeChecking.Rules.Term
infertypevarAgda.Auto.CaseSplit
InferVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
infimumAgda.Termination.CallGraph
InfiniteAgda.Utils.Warshall
infiniteAgda.Utils.Warshall
InfixAgda.Syntax.Concrete
InfixDefAgda.Syntax.Common
infixlPAgda.Syntax.Concrete.Operators.Parser
infixPAgda.Syntax.Concrete.Operators.Parser
infixrPAgda.Syntax.Concrete.Operators.Parser
InfoAgda.Syntax.Info
infodeclAgda.Compiler.MAlonzo.Compiler
infoOnExceptionAgda.Interaction.GhciTop
initCompileStateAgda.Compiler.Epic.CompileState
initEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initGraphAgda.Utils.Warshall
initialDotStateAgda.Interaction.Highlighting.Dot
initialPrimsAgda.Compiler.Epic.Primitive
initialRelsAgda.Compiler.Epic.Erasure
initialTagsAgda.Compiler.Epic.Injection
initiateAgda.Compiler.Epic.Erasure
initMapSAgda.Auto.Convert
initMetaAgda.Auto.NarrowingSearch
initState 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
3 (Function)Agda.Interaction.GhciTop
injArgAgda.Compiler.Epic.Interface
injArityAgda.Compiler.Epic.Interface
InjConstraintsAgda.Compiler.Epic.Injection
InjectiveFun 
1 (Type/Class)Agda.Compiler.Epic.Interface
2 (Data Constructor)Agda.Compiler.Epic.Interface
injectiveFunsAgda.Compiler.Epic.Interface
InlineAgda.Compiler.Epic.AuxAST
inMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
inNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
InScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
InScopeTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inScopeTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
insert 
1 (Function)Agda.Utils.Graph
2 (Function)Agda.Utils.Trie
3 (Function)Agda.Termination.CallGraph
insertAfterAgda.Compiler.JS.Compiler
insertAtAgda.Compiler.Epic.Injection
insertImplicitAgda.TypeChecking.Implicit
insertImplicitPatternsAgda.TypeChecking.Rules.LHS.Implicit
insertImplicitProblemAgda.TypeChecking.Rules.LHS.Implicit
insertPatternsAgda.TypeChecking.Rules.Def
insertTeleAgda.Compiler.Epic.Forcing
insertWithKeyMAgda.Utils.Map
InsideOperandCtxAgda.Syntax.Fixity
insideScopeAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
Instance 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Common
InstanceArgAgda.Syntax.Concrete
InstanceArgVAgda.Syntax.Concrete.Operators.Parser
InstancePAgda.Syntax.Concrete
InstantiableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstantiateAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiateAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
InstantiatedAgda.Interaction.BasicOps
instantiateDefAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
InstantiateFullAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiateFullAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiatePatternAgda.TypeChecking.Rules.LHS
instantiateTelAgda.TypeChecking.Rules.LHS.Instantiate
inStateAgda.Syntax.Parser.LexActions
InstSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstVAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
intAgda.Utils.Pretty
IntegerAgda.Compiler.JS.Syntax
integerAgda.Utils.Pretty
integerSemiringAgda.Termination.Semiring
Interaction 
1 (Type/Class)Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Interaction.GhciTop
interactionAgda.Interaction.CommandLine.CommandLine
InteractionId 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interactionLoopAgda.Interaction.CommandLine.CommandLine
InteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interestingCallAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
Interface 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InternalErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
internalErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
intersectVarsAgda.TypeChecking.Conversion
intersectWithAgda.Termination.SparseMatrix
Interval 
1 (Type/Class)Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Position, Agda.Interaction.GhciTop
intervalInvariantAgda.Syntax.Position, Agda.Interaction.GhciTop
intLitAgda.Compiler.JS.Parser
intMapAgda.Utils.Warshall
introTacticAgda.Interaction.BasicOps
InvAgda.TypeChecking.Injectivity
InvalidPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InvariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inverseApplyRelevanceAgda.TypeChecking.Irrelevance
inverseComposeRelevanceAgda.TypeChecking.Irrelevance
inverseScopeLookupAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inverseScopeLookupModuleAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inverseScopeLookupNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
invertPAgda.Utils.Permutation
InvViewAgda.TypeChecking.Injectivity
ioAgda.TypeChecking.Primitive
IOExceptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iotapossmetaAgda.Auto.Typecheck
iotastepAgda.Auto.Typecheck
ioTCMAgda.Interaction.GhciTop
ioTCM_Agda.Interaction.GhciTop
iPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IrrAgda.Compiler.Epic.Interface
IrrelAgda.TypeChecking.MetaVars.Occurs
IrrelevantAgda.Syntax.Common
IrrelevantDatatypeAgda.TypeChecking.Coverage
irrelevantVarsAgda.TypeChecking.Free
irrToNonStrictAgda.TypeChecking.Irrelevance
IsAbstractAgda.Syntax.Common
isAHoleAgda.Syntax.Notation
isBelowAgda.Utils.Warshall
isBinderUsedAgda.TypeChecking.Free
isBindingHoleAgda.Syntax.Notation
isBlockedTermAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isCoinductiveAgda.TypeChecking.Rules.Data
isConAgda.TypeChecking.Quote
iScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isDataOrRecordTypeAgda.TypeChecking.Datatypes
isDatatype 
1 (Function)Agda.TypeChecking.Datatypes
2 (Function)Agda.TypeChecking.Coverage
IsEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmpty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Termination.SparseMatrix
3 (Function)Agda.Termination.Matrix
IsEmptyTypeAgda.Interaction.BasicOps
isEmptyTypeAgda.TypeChecking.Empty
isEtaExpandableAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isEtaRecordAgda.TypeChecking.Records
isEtaRecordTypeAgda.TypeChecking.Records
isEtaRecordTypeHHAgda.TypeChecking.Rules.LHS.Unify
IsExprAgda.Syntax.Concrete.Operators.Parser
isFrozenAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isGeneratedRecordConstructorAgda.TypeChecking.Records
isHaskellKindAgda.Compiler.HaskellTypes
isHiddenArgAgda.Syntax.Common
isHoleAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isHomAgda.TypeChecking.Rules.LHS.Unify
iSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isImportedAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isIndependentAgda.Interaction.GhciTop
IsInfixAgda.Syntax.Common
isInfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInjectiveAgda.Compiler.Epic.Injection
isInjectiveHereAgda.Compiler.Epic.Injection
isInModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isInstantiatedMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isInteractionMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isIrrAgda.Compiler.Epic.Erasure
isJustAgda.Utils.Maybe
isLambdaHoleAgda.Syntax.Notation
isLeftAgda.Utils.Either
isLevelConstraintAgda.TypeChecking.UniversePolymorphism
isLiterateAgda.Interaction.Options
isNatishAgda.Compiler.Epic.NatDetection
isNewerThanAgda.Interaction.Imports
isNoBodyAgda.Compiler.Epic.Injection
isNoNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNonfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNothingAgda.Utils.Maybe
isntTypeConfAgda.TypeChecking.Test.Generators
isOperator 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isPostfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPrefixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isProblemSolvedAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
isProjectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
isReallyEmptyTypeAgda.TypeChecking.Empty
isRecAgda.Compiler.Epic.NatDetection
isRecordAgda.TypeChecking.Records
isRecordConstructorAgda.TypeChecking.Records
IsReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isRelAgda.Compiler.Epic.Erasure
isRightAgda.Utils.Either
isSingleton 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Compiler.JS.Compiler
isSingletonRecordAgda.TypeChecking.Records
isSingletonRecord'Agda.TypeChecking.Records
isSingletonRecordModuloRelevanceAgda.TypeChecking.Records
isSizeNameTestAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeTypeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeTypeTestAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSolvedProblemAgda.TypeChecking.Rules.LHS
isSolvingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
IsSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isSortMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isStringAgda.Utils.Generics
isSublistOfAgda.Utils.List
isSubModuleOfAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isSubsetOfAgda.Utils.VarSet
isSuccessAgda.Utils.QuickCheck
IsTagAgda.Compiler.Epic.Injection
iStartAgda.Syntax.Position, Agda.Interaction.GhciTop
isTypeAgda.TypeChecking.Rules.Term
IsTypeCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isTypeConfAgda.TypeChecking.Test.Generators
isTypeEqualToAgda.TypeChecking.Rules.Term
IsType_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isType_Agda.TypeChecking.Rules.Term
isUnicodeIdAgda.Utils.Unicode
isVisitedAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isWellScopedAgda.TypeChecking.Test.Generators
isZeroAgda.Utils.TestHelpers
ItemAgda.TypeChecking.Positivity
iterate'Agda.Utils.Function
jMetaIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
jMetaTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
JSAgda.Interaction.GhciTop
JSCodeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
jsFileNameAgda.Compiler.JS.Compiler
jsMemberAgda.Compiler.JS.Compiler
jsModAgda.Compiler.JS.Compiler
JudgementAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
judgementInteractionIdAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
judgToOutputFormAgda.Interaction.BasicOps
JustAgda.Utils.Maybe
JustSortAgda.Interaction.BasicOps
JustTypeAgda.Interaction.BasicOps
keepCommentsAgda.Syntax.Parser.Comments
keepCommentsMAgda.Syntax.Parser.Comments
Keyword 
1 (Type/Class)Agda.Syntax.Parser.Tokens
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
keyword 
1 (Function)Agda.Syntax.Parser.LexActions
2 (Function)Agda.Interaction.Highlighting.Vim
killAbsAgda.TypeChecking.Test.Generators
killArgsAgda.TypeChecking.MetaVars.Occurs
killedTypeAgda.TypeChecking.MetaVars.Occurs
KillRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
killRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
killRange1Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange2Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange3Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange4Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange5Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange6Agda.Syntax.Position, Agda.Interaction.GhciTop
killRange7Agda.Syntax.Position, Agda.Interaction.GhciTop
KillVarAgda.TypeChecking.Test.Generators
killVarAgda.TypeChecking.Test.Generators
KindOfNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
KwAbstractAgda.Syntax.Parser.Tokens
KwBUILTINAgda.Syntax.Parser.Tokens
KwCoDataAgda.Syntax.Parser.Tokens
KwCOMPILEDAgda.Syntax.Parser.Tokens
KwCOMPILED_DATAAgda.Syntax.Parser.Tokens
KwCOMPILED_EPICAgda.Syntax.Parser.Tokens
KwCOMPILED_JSAgda.Syntax.Parser.Tokens
KwCOMPILED_TYPEAgda.Syntax.Parser.Tokens
KwConstructorAgda.Syntax.Parser.Tokens
KwDataAgda.Syntax.Parser.Tokens
KwETAAgda.Syntax.Parser.Tokens
KwFieldAgda.Syntax.Parser.Tokens
KwForallAgda.Syntax.Parser.Tokens
KwHidingAgda.Syntax.Parser.Tokens
KwIMPORTAgda.Syntax.Parser.Tokens
KwImportAgda.Syntax.Parser.Tokens
KwIMPOSSIBLEAgda.Syntax.Parser.Tokens
KwInAgda.Syntax.Parser.Tokens
KwInfixAgda.Syntax.Parser.Tokens
KwInfixLAgda.Syntax.Parser.Tokens
KwInfixRAgda.Syntax.Parser.Tokens
KwLetAgda.Syntax.Parser.Tokens
KwLINEAgda.Syntax.Parser.Tokens
KwModuleAgda.Syntax.Parser.Tokens
KwMutualAgda.Syntax.Parser.Tokens
KwOpenAgda.Syntax.Parser.Tokens
KwOPTIONSAgda.Syntax.Parser.Tokens
KwPostulateAgda.Syntax.Parser.Tokens
KwPrimitiveAgda.Syntax.Parser.Tokens
KwPrivateAgda.Syntax.Parser.Tokens
KwPropAgda.Syntax.Parser.Tokens
KwPublicAgda.Syntax.Parser.Tokens
KwQuoteAgda.Syntax.Parser.Tokens
KwQuoteGoalAgda.Syntax.Parser.Tokens
KwQuoteTermAgda.Syntax.Parser.Tokens
KwRecordAgda.Syntax.Parser.Tokens
KwRenamingAgda.Syntax.Parser.Tokens
KwRewriteAgda.Syntax.Parser.Tokens
KwSetAgda.Syntax.Parser.Tokens
KwSTATICAgda.Syntax.Parser.Tokens
KwSyntaxAgda.Syntax.Parser.Tokens
KwToAgda.Syntax.Parser.Tokens
KwUnquoteAgda.Syntax.Parser.Tokens
KwUsingAgda.Syntax.Parser.Tokens
KwWhereAgda.Syntax.Parser.Tokens
KwWithAgda.Syntax.Parser.Tokens
L 
1 (Data Constructor)Agda.Interaction.EmacsCommand
2 (Data Constructor)Agda.Utils.Map
labelAgda.Utils.QuickCheck
labelsAgda.Utils.QuickCheck
Lam 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Internal
4 (Data Constructor)Agda.Compiler.Epic.AuxAST
5 (Data Constructor)Agda.Syntax.Abstract
LambdaAgda.Compiler.JS.Syntax
lambda 
1 (Function)Agda.Compiler.JS.Case
2 (Function)Agda.Syntax.Concrete.Pretty
lambda'Agda.Compiler.JS.Case
LambdaHoleAgda.Syntax.Notation
LamBinding 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
lamBracketsAgda.Syntax.Fixity
lamFreqAgda.TypeChecking.Test.Generators
LamNotPiAgda.TypeChecking.Rules.Term
LamOrPiAgda.TypeChecking.Rules.Term
LamVAgda.Syntax.Concrete.Operators.Parser
LayoutAgda.Syntax.Parser.Monad
layoutAgda.Syntax.Parser.Lexer
LayoutContextAgda.Syntax.Parser.Monad
layoutKeywordsAgda.Syntax.Parser.Tokens
LazyAgda.Compiler.Epic.AuxAST
lazyAgda.Compiler.Epic.AuxAST
lbraceAgda.Utils.Pretty
lbrackAgda.Utils.Pretty
LCharAgda.Compiler.Epic.AuxAST
leAgda.Termination.CallGraph
leaveTopLevelAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
LeftAssocAgda.Syntax.Fixity
LeftDisjunctAgda.Auto.NarrowingSearch
leftDistributiveAgda.Utils.TestHelpers
LeftHandSideAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
leftHHAgda.TypeChecking.Rules.LHS.Unify
LeftModeAgda.Utils.Pretty
LeftOfArrowAgda.TypeChecking.Positivity
LeftOperandCtxAgda.Syntax.Fixity
LegendMatrix 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.Utils.Warshall
LeqAgda.TypeChecking.SizedTypes
leqLevelAgda.TypeChecking.Conversion
leqSortAgda.TypeChecking.Conversion
leqTypeAgda.TypeChecking.Conversion
leqType_Agda.TypeChecking.Rules.Term
Let 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Compiler.Epic.AuxAST
3 (Data Constructor)Agda.Syntax.Abstract
LetApplyAgda.Syntax.Abstract
LetBindAgda.Syntax.Abstract
LetBindingAgda.Syntax.Abstract
LetBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
LetDefAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
LetDefsAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
LetInfoAgda.Syntax.Info
LetOpenAgda.Syntax.Abstract
LetRangeAgda.Syntax.Info
lettAgda.Compiler.Epic.AuxAST
Level 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
LevelAtomAgda.Syntax.Internal
LevelCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
LevelKit 
1 (Type/Class)Agda.TypeChecking.Level
2 (Data Constructor)Agda.TypeChecking.Level
levelLubAgda.TypeChecking.Level
levelMaxAgda.TypeChecking.Substitute
LevelsAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
levelSortAgda.TypeChecking.Substitute
levelSucAgda.Syntax.Internal
levelSucFunctionAgda.TypeChecking.Level
levelTmAgda.TypeChecking.Substitute
levelViewAgda.TypeChecking.Level
LexActionAgda.Syntax.Parser.Alex
lexerAgda.Syntax.Parser.Lexer
lexErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser.LexActions
lexInputAgda.Syntax.Parser.Alex
LexOrderAgda.Termination.Lexicographic
lexOrderAgda.Termination.Lexicographic
lexPosAgda.Syntax.Parser.Alex
LexPredicateAgda.Syntax.Parser.Alex
lexPrevCharAgda.Syntax.Parser.Alex
LexStateAgda.Syntax.Parser.Monad
lexTokenAgda.Syntax.Parser.LexActions
LFloatAgda.Compiler.Epic.AuxAST
LHS 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Abstract
LHSInfoAgda.Syntax.Info
lhsOriginalPatternAgda.Syntax.Concrete
LHSRangeAgda.Syntax.Info
lhsRewriteEqnAgda.Syntax.Concrete
lhsWithExprAgda.Syntax.Concrete
lhsWithPatternAgda.Syntax.Concrete
liftAgda.Auto.CaseSplit
liftEitherAgda.Utils.Monad
liftPAgda.Syntax.Parser.LookAhead
liftTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lineLengthAgda.Utils.Pretty
LIntAgda.Compiler.Epic.AuxAST
LispAgda.Interaction.EmacsCommand
listAgda.TypeChecking.Primitive
ListenerAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
listenToMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
listOfAgda.Utils.QuickCheck
listOf1Agda.Utils.QuickCheck
listOfElementsAgda.Utils.TestHelpers
listToMaybeAgda.Utils.Maybe
Lit 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Compiler.Epic.AuxAST
4 (Type/Class)Agda.Compiler.Epic.AuxAST
5 (Data Constructor)Agda.Syntax.Abstract
litBranchesAgda.TypeChecking.CompiledClause
litCaseAgda.TypeChecking.CompiledClause
LitCharAgda.Syntax.Literal
litCharAgda.Syntax.Parser.StringLiterals
litConAgda.Compiler.Epic.Injection
LiteralAgda.Syntax.Literal
literal 
1 (Function)Agda.Syntax.Parser.LexActions
2 (Function)Agda.Compiler.MAlonzo.Compiler
3 (Function)Agda.Compiler.JS.Compiler
literateAgda.Syntax.Parser.Lexer
LitFloatAgda.Syntax.Literal
LitFocusAgda.TypeChecking.Rules.LHS.Problem
litFreqAgda.TypeChecking.Test.Generators
LitIntAgda.Syntax.Literal
LitMPAgda.TypeChecking.Coverage.Match
LitP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Abstract
LitQNameAgda.Syntax.Literal
litqnameAgda.Compiler.MAlonzo.Compiler
LitShAgda.TypeChecking.Rules.LHS.Unify
LitStringAgda.Syntax.Literal
litStringAgda.Syntax.Parser.StringLiterals
litToConAgda.Compiler.Epic.Injection
litTypeAgda.TypeChecking.Rules.Term
loadFileAgda.Interaction.CommandLine.CommandLine
LocalAgda.Compiler.JS.Syntax
LocalId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
localidAgda.Compiler.JS.Parser
localNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
localScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localStateAgda.TypeChecking.Constraints
localTerminationEnvAgda.Auto.CaseSplit
localTerminationSidecondAgda.Auto.CaseSplit
localToAbstractAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
LocalVAgda.Syntax.Concrete.Operators.Parser
LocalVarsAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
LocalVsImportedModuleClashAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lookAgda.Utils.ReadP
LookAheadAgda.Syntax.Parser.LookAhead
lookInterfaceAgda.Compiler.Epic.CompileState
LookupAgda.Compiler.JS.Syntax
lookup 
1 (Function)Agda.Utils.Graph
2 (Function)Agda.Compiler.JS.Substitution
lookupEdgeAgda.Utils.Warshall
lookupInteractionIdAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
lookupPathAgda.Utils.Trie
lookupPrimitiveFunctionAgda.TypeChecking.Primitive
lookupSectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
LowerMetaAgda.Interaction.GhciTop
lowerMetaAgda.Interaction.GhciTop
lowMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lparenAgda.Utils.Pretty
LStringAgda.Compiler.Epic.AuxAST
ltAgda.Termination.CallGraph
Lvl 
1 (Type/Class)Agda.TypeChecking.Primitive
2 (Data Constructor)Agda.TypeChecking.Primitive
lvlMaxAgda.TypeChecking.Level
lvlSucAgda.TypeChecking.Level
lvlTypeAgda.TypeChecking.Level
lvlViewAgda.TypeChecking.Substitute
lvlZeroAgda.TypeChecking.Level
mainAgda.Main
mainNameAgda.Compiler.Epic.Interface
makeAbstractAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
makeAbstractClauseAgda.Interaction.MakeCase
makeAbsurdClauseAgda.Interaction.MakeCase
makeCaseAgda.Interaction.MakeCase
makeClosedAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeConfigurationAgda.TypeChecking.Test.Generators
makeEnvAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
makeForcedArgsAgda.Compiler.Epic.ForceConstrs
makeInstanceAgda.Syntax.Common
makeOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeProjectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
makeSilentAgda.Interaction.GhciTop
makeSubstitutionAgda.TypeChecking.Rules.LHS.Unify
MAlonzoAgda.Interaction.GhciTop
manyAgda.Utils.ReadP
many1Agda.Utils.ReadP
manyTillAgda.Utils.ReadP
mapAgda.Compiler.JS.Substitution
map'Agda.Compiler.JS.Substitution
mapConAgda.Compiler.Epic.Primitive
mapFlagAgda.Interaction.Options
mapMaybeAgda.Utils.Maybe
mapMaybeMAgda.Utils.Monad
mapNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapNameSpaceMAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapNodesAgda.Utils.Warshall
mappingAgda.Compiler.JS.Compiler
mapping'Agda.Compiler.JS.Compiler
MapSAgda.Auto.Convert
mapScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScopeMAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScopeM_Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapScope_Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mapSizeAgda.Utils.QuickCheck
mapTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MArgListAgda.Auto.Syntax
markStaticAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
MatAgda.Termination.CallGraph
matAgda.Termination.CallGraph
Match 
1 (Type/Class)Agda.TypeChecking.Coverage.Match
2 (Type/Class)Agda.TypeChecking.Patterns.Match
3 (Type/Class)Agda.TypeChecking.DisplayForm
match 
1 (Function)Agda.Compiler.JS.Case
2 (Function)Agda.TypeChecking.Coverage.Match
3 (Function)Agda.Syntax.Parser.LookAhead
4 (Function)Agda.Interaction.Highlighting.Vim
5 (Function)Agda.TypeChecking.DisplayForm
6 (Function)Agda.TypeChecking.CompiledClause.Match
match' 
1 (Function)Agda.Syntax.Parser.LookAhead
2 (Function)Agda.TypeChecking.CompiledClause.Match
matchClauseAgda.TypeChecking.Coverage.Match
matchCommandAgda.Interaction.CommandLine.CommandLine
matchCompiledAgda.TypeChecking.CompiledClause.Match
matchDisplayFormAgda.TypeChecking.DisplayForm
matchesAgda.Interaction.Highlighting.Vim
MatchLitAgda.TypeChecking.Coverage.Match
matchLitsAgda.TypeChecking.Coverage.Match
matchPatAgda.TypeChecking.Coverage.Match
matchPatsAgda.TypeChecking.Coverage.Match
matchPatternAgda.TypeChecking.Patterns.Match
matchPatternsAgda.TypeChecking.Patterns.Match
matchTypeAgda.Auto.Convert
Matrix 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Type/Class)Agda.Termination.Matrix
3 (Type/Class)Agda.Utils.Warshall
matrix 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
3 (Function)Agda.Utils.Warshall
matrixInvariant 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
matrixUsingRowGen 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
MaxAgda.Syntax.Internal
maxDiscardAgda.Utils.QuickCheck
maxNameAgda.TypeChecking.Level
maxSizeAgda.Utils.QuickCheck
maxSuccessAgda.Utils.QuickCheck
MaybeAgda.Utils.Maybe
maybeAgda.Utils.Maybe
maybeCoGenAgda.Utils.TestHelpers
maybeGenAgda.Utils.TestHelpers
maybeorAgda.Auto.Typecheck
maybePrefixMatchAgda.Utils.List
maybePrimConAgda.TypeChecking.Level
maybePrimDefAgda.TypeChecking.Level
MaybeRedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MaybeReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MaybeReducedArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
maybeToListAgda.Utils.Maybe
MayNotPostponeAgda.TypeChecking.Rules.LHS.Unify
MayPostponeAgda.TypeChecking.Rules.LHS.Unify
mazBoolToHBoolAgda.Compiler.MAlonzo.Primitives
mazCharToIntegerAgda.Compiler.MAlonzo.Primitives
mazCoerceAgda.Compiler.MAlonzo.Misc
mazerrorAgda.Compiler.MAlonzo.Misc
mazHBoolToBoolAgda.Compiler.MAlonzo.Primitives
mazHListToListAgda.Compiler.MAlonzo.Primitives
mazIncompleteMatchAgda.Compiler.MAlonzo.Misc
mazIntegerToNatAgda.Compiler.MAlonzo.Primitives
mazIntToNatAgda.Compiler.MAlonzo.Primitives
mazListToHListAgda.Compiler.MAlonzo.Primitives
mazListToStringAgda.Compiler.MAlonzo.Primitives
mazModAgda.Compiler.MAlonzo.Misc
mazMod'Agda.Compiler.MAlonzo.Misc
mazNameAgda.Compiler.MAlonzo.Misc
mazNatToIntAgda.Compiler.MAlonzo.Primitives
mazNatToIntegerAgda.Compiler.MAlonzo.Primitives
mazRTEAgda.Compiler.MAlonzo.Misc
mazstrAgda.Compiler.MAlonzo.Misc
mazStringToListAgda.Compiler.MAlonzo.Primitives
MBAgda.Auto.NarrowingSearch
mbcaseAgda.Auto.NarrowingSearch
mbfailedAgda.Auto.NarrowingSearch
mbindAgda.Auto.NarrowingSearch
mbpcaseAgda.Auto.NarrowingSearch
mbretAgda.Auto.NarrowingSearch
mcompointAgda.Auto.NarrowingSearch
memberAgda.Utils.VarSet
MemberId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
MentionsMetaAgda.TypeChecking.MetaVars.Mention
mentionsMetaAgda.TypeChecking.MetaVars.Mention
mergeGroupsAgda.Compiler.Epic.Injection
mergeInterfaceAgda.Interaction.Imports
mergeNamesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mergeScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
mergeScopesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
MetaAgda.Auto.NarrowingSearch
MetaArgAgda.TypeChecking.Positivity
MetaCannotDependOnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaElimAgda.TypeChecking.Eliminators
MetaEnvAgda.Auto.NarrowingSearch
MetaId 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
MetaInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
3 (Type/Class)Agda.Interaction.Highlighting.Precise
4 (Data Constructor)Agda.Interaction.Highlighting.Precise
5 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaInstantiationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaKindAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
MetaLevelAgda.Syntax.Internal
metaliseokhAgda.Auto.Syntax
metaNumberAgda.Syntax.Info
MetaOccursInItselfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaParseExprAgda.Interaction.CommandLine.CommandLine
MetaPriority 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaRangeAgda.Syntax.Info
metaScopeAgda.Syntax.Info
MetaShAgda.TypeChecking.Rules.LHS.Unify
MetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaVAgda.Syntax.Internal
MetaVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Metavar 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
MetaVariableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
meta_not_constructorAgda.Auto.Typecheck
MExpAgda.Auto.Syntax
mextrarefsAgda.Auto.NarrowingSearch
mheadAgda.Utils.List
MIdAgda.Auto.Syntax
miInterfaceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
minfoAsNameAgda.Syntax.Info
minfoAsToAgda.Syntax.Info
minfoDirectiveAgda.Syntax.Info
minfoOpenShortAgda.Syntax.Info
minfoRangeAgda.Syntax.Info
MissingDataSignatureAgda.Syntax.Concrete.Definitions
MissingDefinitionAgda.Syntax.Concrete.Definitions
MissingTypeSignatureAgda.Syntax.Concrete.Definitions
MissingWithClausesAgda.Syntax.Concrete.Definitions
miTimeStampAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
miWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MIx 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Data Constructor)Agda.Termination.SparseMatrix
3 (Type/Class)Agda.Termination.Matrix
4 (Data Constructor)Agda.Termination.Matrix
mIxInvariant 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
mkAbsAgda.TypeChecking.Substitute
mkAbsoluteAgda.Utils.FileName, Agda.Interaction.GhciTop
mkBoundName_Agda.Syntax.Concrete
mkConAgda.Compiler.Epic.Forcing
mkContextEntryAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
mkDefInfoAgda.Syntax.Info
mkMatrixAgda.Utils.Warshall
mkNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mkName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mkNotationAgda.Syntax.Notation
mkPrimFun1Agda.TypeChecking.Primitive
mkPrimFun1TCMAgda.TypeChecking.Primitive
mkPrimFun2Agda.TypeChecking.Primitive
mkPrimFun4Agda.TypeChecking.Primitive
mkPrimLevelMaxAgda.TypeChecking.Primitive
mkPrimLevelSucAgda.TypeChecking.Primitive
mkPrimLevelZeroAgda.TypeChecking.Primitive
mkQAgda.Utils.Generics
MkStrAgda.Utils.QuickCheck
mkTypeAgda.Syntax.Internal
mlevelAgda.TypeChecking.Conversion
MMAgda.Auto.NarrowingSearch
mmAgda.Auto.CaseSplit
mmbpcaseAgda.Auto.NarrowingSearch
mmcaseAgda.Auto.NarrowingSearch
mmmcaseAgda.Auto.NarrowingSearch
mmpcaseAgda.Auto.NarrowingSearch
MNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameFromListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameToConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameToListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mnameToQNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
mobsAgda.Auto.NarrowingSearch
ModeAgda.Utils.Pretty
modeAgda.Utils.Pretty
modifyAbstractClauseAgda.Auto.Convert
modifyAbstractExprAgda.Auto.Convert
modifyArgRelevanceAgda.TypeChecking.Irrelevance
modifyContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyContextEntriesAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyContextEntryAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
modifyCurrentNameSpaceAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyCurrentScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyCurrentScopeMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyEIAgda.Compiler.Epic.CompileState
modifyImportedSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modifyMetaStoreAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
modifyNamedScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyNamedScopeMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
modifyScopeInfoAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifyScopesAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
modifySignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modNameAgda.Compiler.JS.Syntax
modnameAgda.Compiler.JS.Pretty
modSubAgda.TypeChecking.Rules.LHS.Unify
Module 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
3 (Type/Class)Agda.Syntax.Concrete
4 (Data Constructor)Agda.Syntax.Concrete
5 (Data Constructor)Agda.Interaction.Highlighting.Precise
ModuleApplication 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
ModuleArityMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moduleContentsAgda.Interaction.BasicOps
ModuleDefinedInOtherFileAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleDoesntExportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
3 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
4 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ModuleMacroAgda.Syntax.Concrete
ModuleNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
moduleNameAgda.Interaction.FindFile
moduleName'Agda.Interaction.FindFile
ModuleNameDoesntMatchFileNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moduleNamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleNameToFileNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
moduleParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser, Agda.Interaction.GhciTop
ModulesInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ModuleTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ModuleToSourceAgda.Interaction.FindFile
MonadExceptionAgda.TypeChecking.Monad.Exception
MonadTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moreRelevantAgda.Syntax.Common
movePosAgda.Syntax.Position, Agda.Interaction.GhciTop
movePosByStringAgda.Syntax.Position, Agda.Interaction.GhciTop
mparenAgda.Syntax.Concrete.Operators
mparensAgda.Utils.Pretty
MPatAgda.TypeChecking.Coverage.Match
mpretAgda.Auto.NarrowingSearch
mprincipalpresentAgda.Auto.NarrowingSearch
mul 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.SparseMatrix
3 (Function)Agda.Termination.Matrix
MultipleFixityDeclsAgda.Syntax.Concrete.Definitions
multiplyAgda.Termination.Semiring
munchAgda.Utils.ReadP
munch1Agda.Utils.ReadP
MutIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Mutual 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
MutualIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvFrozenAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvInstantiationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvJudgementAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvListenersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvPermutationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mvPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MyMBAgda.Auto.Syntax
MyPBAgda.Auto.Syntax
Name 
1 (Type/Class)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
4 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
5 (Data Constructor)Agda.Interaction.Highlighting.Precise
nameBindingSiteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nameConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
Named 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
namedAgda.Syntax.Common
NamedArgAgda.Syntax.Common
NamedClause 
1 (Type/Class)Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
namedThingAgda.Syntax.Common
nameFixityAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nameFreqAgda.TypeChecking.Test.Generators
NameFreqs 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
nameFreqsAgda.TypeChecking.Test.Generators
NameId 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
nameIdAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
NameKindAgda.Interaction.Highlighting.Precise
nameModifiersAgda.Interaction.GhciTop
nameOfAgda.Syntax.Common
nameOfBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
nameOfFlatAgda.TypeChecking.Rules.Builtin.Coinduction
nameOfInfAgda.TypeChecking.Rules.Builtin.Coinduction
nameOfSharpAgda.TypeChecking.Rules.Builtin.Coinduction
NamePartAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
namePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NamesInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
namesInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameSpace 
1 (Type/Class)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
nameSpaceAccessAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NameSpaceIdAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
nameStringPartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameSupplyAgda.Compiler.Epic.CompileState
NameTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Nat 
1 (Type/Class)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.Common
3 (Type/Class)Agda.TypeChecking.Primitive
4 (Data Constructor)Agda.TypeChecking.Primitive
natPrimTFAgda.Compiler.Epic.Primitive
naturalAgda.Utils.TestHelpers
negAgda.TypeChecking.Polarity
NegativeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
negtypeAgda.Auto.Convert
neighboursAgda.Utils.Graph
nest 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
nestedCommentAgda.Syntax.Parser.Comments
NeutralLevelAgda.Syntax.Internal
newArgsMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newArgsMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newCTreeAgda.Auto.NarrowingSearch
newEdgeAgda.Utils.Warshall
NewFlexAgda.Utils.Warshall
newIFSMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newIFSMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newLayoutContextAgda.Syntax.Parser.Layout
newMeta 
1 (Function)Agda.Auto.NarrowingSearch
2 (Function)Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
newMeta'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
NewModuleNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
NewModuleQName 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
NewNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
newNameAgda.Compiler.Epic.CompileState
NewNotationAgda.Syntax.Fixity
newOKHandleAgda.Auto.NarrowingSearch
newPlaceholderAgda.Auto.NarrowingSearch
newProblemAgda.TypeChecking.Constraints
newProblem_Agda.TypeChecking.Constraints
newQuestionMarkAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newRecordMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newRecordMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSortMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSortMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newSubConstraintsAgda.Auto.NarrowingSearch
newTelMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newTypeMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newTypeMeta_Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMeta'Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMetaCtxAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
newValueMetaCtx'Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
nextCharAgda.Syntax.Parser.LookAhead
nextFreshAgda.Utils.Fresh
nextNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
nextNodeAgda.Utils.Warshall
nextPolarityAgda.TypeChecking.Conversion
nextSplitAgda.TypeChecking.CompiledClause.Compile
nextSuffixAgda.Utils.Suffix
NiceAgda.Syntax.Concrete.Definitions
NiceConstructorAgda.Syntax.Concrete.Definitions
NiceDataSigAgda.Syntax.Concrete.Definitions
NiceDeclarationAgda.Syntax.Concrete.Definitions
niceDeclarationsAgda.Syntax.Concrete.Definitions
NiceFieldAgda.Syntax.Concrete.Definitions
NiceImportAgda.Syntax.Concrete.Definitions
NiceModuleAgda.Syntax.Concrete.Definitions
NiceModuleMacroAgda.Syntax.Concrete.Definitions
NiceMutualAgda.Syntax.Concrete.Definitions
NiceOpenAgda.Syntax.Concrete.Definitions
NicePragmaAgda.Syntax.Concrete.Definitions
NiceRecSigAgda.Syntax.Concrete.Definitions
NiceTypeSignatureAgda.Syntax.Concrete.Definitions
No 
1 (Data Constructor)Agda.TypeChecking.Coverage.Match
2 (Data Constructor)Agda.TypeChecking.Patterns.Match
NoAbsAgda.Syntax.Internal
NoAppAgda.TypeChecking.EtaContract
NoBindingForBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noblksAgda.Auto.Typecheck
NoBodyAgda.Syntax.Internal
noCompiledRepAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noConstraintsAgda.TypeChecking.Constraints
Node 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.Positivity
NodeIdAgda.Utils.Warshall
nodeMapAgda.Utils.Warshall
nodesAgda.Utils.Graph
NoElimAgda.TypeChecking.Eliminators
NoExpectedFailureAgda.Utils.QuickCheck
noFixityAgda.Syntax.Fixity
NoIdAgda.Auto.Syntax
NoInsertNeededAgda.TypeChecking.Implicit
NoInvAgda.TypeChecking.Injectivity
noiotastepAgda.Auto.Typecheck
noiotastep_termAgda.Auto.Typecheck
NoLayoutAgda.Syntax.Parser.Monad
noLiteralsAgda.TypeChecking.Test.Generators
noMatchLitAgda.TypeChecking.Coverage.Match
noModuleNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
noMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
NoNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
noName_Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NonAssocAgda.Syntax.Fixity
NonEmptyAgda.Utils.QuickCheck
NonEmptyListAgda.Utils.QuickCheck
nonfixPAgda.Syntax.Concrete.Operators.Parser
NonNegative 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
noNotationAgda.Syntax.Notation
NonPositivelyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NonStrictAgda.Syntax.Common
nonStrictToIrrAgda.TypeChecking.Irrelevance
NonZero 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
NoOccurrenceAgda.TypeChecking.Free
NoParseForApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoParseForLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noPatternMatchingOnCodataAgda.TypeChecking.Rules.LHS
NopeAgda.Syntax.Info
noPostponingAgda.TypeChecking.Rules.LHS.Unify
NoPrioAgda.Auto.NarrowingSearch
noPropAgda.TypeChecking.Test.Generators
noRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
NoRecordConstructorAgda.TypeChecking.Coverage
NoReductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoRHSRequiresAbsurdPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
normAgda.Auto.Convert
normalAgda.Syntax.Parser.Lexer
NormalHoleAgda.Syntax.Notation
NormaliseAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
normaliseAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
NormalisedAgda.Interaction.BasicOps
normaliseStaticAgda.Compiler.Epic.Static
normalMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noShadowingOfConstructorsAgda.TypeChecking.Rules.LHS
noShrinkAgda.TypeChecking.Test.Generators
NoSuchBuiltinNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuchModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuchNameAgda.TypeChecking.Implicit
NoSuchPrimitiveFunctionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoSuffixAgda.Utils.Suffix
not'Agda.Syntax.Parser.Alex
NotADatatypeAgda.TypeChecking.Coverage
notAHaskellKindAgda.Compiler.HaskellTypes
notAHaskellTypeAgda.Compiler.HaskellTypes
noTakenNamesAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
NotAllowedInMutualAgda.Syntax.Concrete.Definitions
NotAModuleExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAnExpressionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotAProperTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotationAgda.Syntax.Notation
NotAValidLetBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotBAgda.Auto.NarrowingSearch
NotBlockedAgda.Syntax.Internal
notBlockedAgda.Syntax.Internal
NotDelayedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
noteAgda.Interaction.Highlighting.Precise
notequalAgda.Auto.CaseSplit
NotForcedAgda.Compiler.Epic.Interface
notForcedAgda.Compiler.Epic.Interface
NotFoundAgda.Interaction.FindFile
NotHidden 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Common
notHiddenFreqAgda.TypeChecking.Test.Generators
NothingAgda.Utils.Maybe
NothingAppliedToHiddenArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NothingAppliedToInstanceArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NothingToPruneAgda.TypeChecking.MetaVars.Occurs
NothingToSplitAgda.TypeChecking.Rules.LHS.Problem
nothingToSplitErrorAgda.TypeChecking.Rules.LHS.Instantiate
NotImplementedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInductiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInjectiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notInScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
NotLeqSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotMAgda.Auto.NarrowingSearch
NotPBAgda.Auto.NarrowingSearch
NotReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
notSoNiceDeclarationsAgda.Syntax.Concrete.Definitions
NotStrictlyPositiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NotSupportedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NoType 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
NoUnfoldAgda.TypeChecking.MetaVars.Occurs
NoUnifyAgda.TypeChecking.Rules.LHS.Unify
NoWhereAgda.Syntax.Concrete
NoWithFunctionAgda.TypeChecking.Rules.Def
nowSolvingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
nPiAgda.TypeChecking.Primitive
nrBindsAgda.Compiler.Epic.Injection
nrRelAgda.Compiler.Epic.NatDetection
nsModulesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
nsNamesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
NumberAgda.Interaction.Highlighting.Precise
numParsAgda.Compiler.JS.Compiler
numShrinksAgda.Utils.QuickCheck
numTestsAgda.Utils.QuickCheck
numVarsAgda.Compiler.JS.Case
numVars'Agda.Compiler.JS.Case
OAgda.Auto.Convert
ObjectAgda.Compiler.JS.Syntax
object 
1 (Function)Agda.Compiler.JS.Substitution
2 (Function)Agda.Compiler.JS.Parser
OccAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OccClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OccConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occFunctionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OccPosAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occPositionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Occurrence 
1 (Type/Class)Agda.TypeChecking.Free
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
occurrenceAgda.TypeChecking.Free
OccurrencesAgda.TypeChecking.Positivity
occurrencesAgda.TypeChecking.Positivity
OccursAgda.TypeChecking.MetaVars.Occurs
occursAgda.TypeChecking.MetaVars.Occurs
occursAsAgda.TypeChecking.Positivity
occursCheck 
1 (Function)Agda.TypeChecking.MetaVars.Occurs
2 (Function)Agda.TypeChecking.Rules.LHS.Unify
OccursCtxAgda.TypeChecking.MetaVars.Occurs
OccursWhereAgda.TypeChecking.Positivity
octDigitAgda.Utils.Char
ofExprAgda.Interaction.BasicOps
offsideRuleAgda.Syntax.Parser.Layout
ofNameAgda.Interaction.BasicOps
OfTypeAgda.Interaction.BasicOps
OfType'Agda.Interaction.BasicOps
OHConAgda.Syntax.Internal.Pattern
OHPatsAgda.Syntax.Internal.Pattern
OKAgda.Auto.NarrowingSearch
OKHandleAgda.Auto.NarrowingSearch
OKMetaAgda.Auto.NarrowingSearch
OKVal 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
OldModuleNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
OldName 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
OldQNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
oldToNewNotationAgda.Syntax.Fixity
onAgda.Interaction.Highlighting.Vim
OneHolePatternAgda.Syntax.Internal.Pattern
OneHolePatternsAgda.Syntax.Internal.Pattern
OneLineModeAgda.Utils.Pretty
oneofAgda.Utils.QuickCheck
OnlyQualifiedAgda.Syntax.Common
OnlyQualifiedNSAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
onSubAgda.TypeChecking.Rules.LHS.Unify
onTopLevelAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
OpAgda.TypeChecking.Primitive
OpApp 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Concrete
OpAppPAgda.Syntax.Concrete
OpAppVAgda.Syntax.Concrete.Operators.Parser
opBracketsAgda.Syntax.Fixity
Open 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
4 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
openBraceAgda.Syntax.Parser.Layout
OpenIFSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
openModule_Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
OpenShortHandAgda.Syntax.Concrete
OpenThingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
oplusAgda.Utils.SemiRing
opPAgda.Syntax.Concrete.Operators.Parser
optAllowUnsolvedAgda.Interaction.Options
optCompileAgda.Interaction.Options
optCompileDirAgda.Interaction.Options
optCompletenessCheckAgda.Interaction.Options
optCSSFileAgda.Interaction.Options
optDependencyGraphAgda.Interaction.Options
optDisablePositivityAgda.Interaction.Options
optEpicCompileAgda.Interaction.Options
optEpicFlagsAgda.Interaction.Options
optExperimentalIrrelevanceAgda.Interaction.Options
optForcingAgda.Interaction.Options
optGenerateHTMLAgda.Interaction.Options
optGenerateVimFileAgda.Interaction.Options
optGhcFlagsAgda.Interaction.Options
optGuardingTypeConstructorsAgda.Interaction.Options
optHTMLDirAgda.Interaction.Options
optIgnoreInterfacesAgda.Interaction.Options
optIncludeDirsAgda.Interaction.Options
optInjectiveTypeConstructorsAgda.Interaction.Options
optInputFileAgda.Interaction.Options
optInteractiveAgda.Interaction.Options
optionAgda.Utils.ReadP
optionalAgda.Utils.ReadP
optionErrorAgda.Main
OptionsAgda.Interaction.Options
OptionsPragma 
1 (Type/Class)Agda.Interaction.Options
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
optIrrelevantProjectionsAgda.Interaction.Options
optJSCompileAgda.Interaction.Options
optPragmaOptionsAgda.Interaction.Options
optProgramNameAgda.Interaction.Options
optProofIrrelevanceAgda.Interaction.Options
optRunTestsAgda.Interaction.Options
optSafeAgda.Interaction.Options
optShowHelpAgda.Interaction.Options
optShowImplicitAgda.Interaction.Options
optShowVersionAgda.Interaction.Options
optSizedTypesAgda.Interaction.Options
optTerminationCheckAgda.Interaction.Options
optTerminationDepthAgda.Interaction.Options
optUniverseCheckAgda.Interaction.Options
optUniversePolymorphismAgda.Interaction.Options
optVerboseAgda.Interaction.Options
optWithoutKAgda.Interaction.Options
OrAgda.Auto.NarrowingSearch
OrderAgda.Termination.CallGraph
OrderedAgda.Utils.QuickCheck
OrderedListAgda.Utils.QuickCheck
orderedListAgda.Utils.QuickCheck
orderFieldsAgda.TypeChecking.Records
orderMatAgda.Termination.CallGraph
OrdinaryAgda.Syntax.Concrete
OtherAspectAgda.Interaction.Highlighting.Precise
otherAspectsAgda.Interaction.Highlighting.Precise
OtherSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
OtherVAgda.Syntax.Concrete.Operators.Parser
otimesAgda.Utils.SemiRing
OutAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
outFile 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
outFile'Agda.Compiler.MAlonzo.Compiler
outFile_ 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
outputAgda.Utils.QuickCheck
OutputConstraintAgda.Interaction.BasicOps
OutputConstraint'Agda.Interaction.BasicOps
OutputForm 
1 (Type/Class)Agda.Interaction.BasicOps
2 (Data Constructor)Agda.Interaction.BasicOps
outputFormIdAgda.Interaction.BasicOps
outsideScopeAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
overlappingAgda.Interaction.Highlighting.Range
OverlappingProjectsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PageModeAgda.Utils.Pretty
Pair 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
pairwiseFilterAgda.Compiler.Epic.Interface
ParenAgda.Syntax.Concrete
parenAgda.Syntax.Concrete.Operators
parenedAgda.Compiler.JS.Parser
ParenPAgda.Syntax.Concrete
parens 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
ParenVAgda.Syntax.Concrete.Operators.Parser
parse 
1 (Function)Agda.Utils.ReadP
2 (Function)Agda.Compiler.JS.Parser
3 (Function)Agda.Syntax.Parser.Monad
4 (Function)Agda.Syntax.Parser, Agda.Interaction.GhciTop
parse'Agda.Utils.ReadP
parseAndDoAtToplevelAgda.Interaction.GhciTop
parseApplicationAgda.Syntax.Concrete.Operators
ParseError 
1 (Type/Class)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
parseErrorAgda.Syntax.Parser.Monad
parseErrorAtAgda.Syntax.Parser.Monad
parseExpr 
1 (Function)Agda.Interaction.BasicOps
2 (Function)Agda.Interaction.CommandLine.CommandLine
parseExprInAgda.Interaction.BasicOps
ParseFailedAgda.Syntax.Parser.Monad
parseFileAgda.Syntax.Parser.Monad
parseFile'Agda.Syntax.Parser, Agda.Interaction.GhciTop
ParseFlags 
1 (Type/Class)Agda.Syntax.Parser.Monad
2 (Data Constructor)Agda.Syntax.Parser.Monad
parseFlagsAgda.Syntax.Parser.Monad
parseInpAgda.Syntax.Parser.Monad
parseKeepCommentsAgda.Syntax.Parser.Monad
parseLastPosAgda.Syntax.Parser.Monad
parseLayoutAgda.Syntax.Parser.Monad
parseLexStateAgda.Syntax.Parser.Monad
parseLHSAgda.Syntax.Concrete.Operators
parseLiterateAgda.Syntax.Parser, Agda.Interaction.GhciTop
ParseOkAgda.Syntax.Parser.Monad
parsePluginOptionsAgda.Interaction.Options
parsePosAgda.Syntax.Parser.Monad
parsePosString 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.Syntax.Parser, Agda.Interaction.GhciTop
parsePragmaOptionsAgda.Interaction.Options
parsePrevCharAgda.Syntax.Parser.Monad
parsePrevTokenAgda.Syntax.Parser.Monad
Parser 
1 (Type/Class)Agda.Compiler.JS.Parser
2 (Type/Class)Agda.Syntax.Parser.Monad
3 (Type/Class)Agda.Syntax.Parser, Agda.Interaction.GhciTop
ParseResultAgda.Syntax.Parser.Monad
parseStandardOptionsAgda.Interaction.Options
ParseStateAgda.Syntax.Parser.Monad
partPAgda.Syntax.Concrete.Operators.Parser
PatAgda.Auto.Syntax
PatConAppAgda.Auto.Syntax
PatExpAgda.Auto.Syntax
PatInfoAgda.Syntax.Info
PatNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
PatRangeAgda.Syntax.Info
patsAgda.Compiler.JS.Case
PatSourceAgda.Syntax.Info
patsToTermsAgda.TypeChecking.With
PattAgda.Compiler.JS.Case
Pattern 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Abstract
patternAgda.Compiler.JS.Compiler
Pattern'Agda.Syntax.Abstract
PatternErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
patternHeadAgda.Syntax.Concrete
patternNamesAgda.Syntax.Concrete
PatternShadowsConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
patternToTermAgda.Compiler.Epic.Injection
patternViolationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PatVarAgda.Auto.Syntax
PBAgda.Auto.NarrowingSearch
PBlockedAgda.Auto.NarrowingSearch
pconNameAgda.Compiler.MAlonzo.Primitives
PConstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PDoubleBlockedAgda.Auto.NarrowingSearch
PEConAppAgda.Auto.Typecheck
PENoAgda.Auto.Typecheck
performKillAgda.TypeChecking.MetaVars.Occurs
PermAgda.Utils.Permutation
PermutationAgda.Utils.Permutation
permuteAgda.Utils.Permutation
PersistentTCStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PersistentTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PEvalAgda.Auto.Typecheck
pfailAgda.Utils.ReadP
pHiddenAgda.Syntax.Concrete.Pretty
Pi 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Abstract
piAbstractTermAgda.TypeChecking.Abstract
piApplyAgda.TypeChecking.Substitute
piApplyMAgda.TypeChecking.Telescope
piApplyM'Agda.Compiler.Epic.Forcing
piBracketsAgda.Syntax.Fixity
pickidAgda.Auto.Typecheck
piFreqAgda.TypeChecking.Test.Generators
PiHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PiNotLamAgda.TypeChecking.Rules.Term
PiShAgda.TypeChecking.Rules.LHS.Unify
plugHoleAgda.Syntax.Internal.Pattern
PlusAgda.Syntax.Internal
PlusLevelAgda.Syntax.Internal
PnAgda.Syntax.Position, Agda.Interaction.GhciTop
polaritiesAgda.TypeChecking.Polarity
PolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
polarityAgda.TypeChecking.Polarity
popAgda.Compiler.JS.Case
popContextAgda.Syntax.Parser.Monad
popLexStateAgda.Syntax.Parser.Monad
popMapSAgda.Auto.Convert
posColAgda.Syntax.Position, Agda.Interaction.GhciTop
PositionAgda.Syntax.Position, Agda.Interaction.GhciTop
positionInvariantAgda.Syntax.Position, Agda.Interaction.GhciTop
Positive 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
positiveAgda.Utils.TestHelpers
positivityCheckEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
posLineAgda.Syntax.Position, Agda.Interaction.GhciTop
posPosAgda.Syntax.Position, Agda.Interaction.GhciTop
PossiblyAgda.TypeChecking.Rules.LHS.Unify
postfixPAgda.Syntax.Concrete.Operators.Parser
postopAgda.Syntax.Concrete.Operators.Parser
posToRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
PostponedTypeCheckingProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
postponeTypeCheckingProblemAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
postponeTypeCheckingProblem_Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
Postulate 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
Pragma 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Abstract
PragmaOptions 
1 (Type/Class)Agda.Interaction.Options
2 (Data Constructor)Agda.Interaction.Options
pragmaOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
PrecedenceAgda.Syntax.Fixity
PredAgda.TypeChecking.Primitive
PrefixAgda.Utils.List
prefixAgda.Compiler.JS.Compiler
PrefixDefAgda.Syntax.Common
prefixPAgda.Syntax.Concrete.Operators.Parser
pRelevanceAgda.Syntax.Concrete.Pretty
preMetaAgda.Interaction.GhciTop
PreOpAgda.Compiler.JS.Syntax
preop 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Concrete.Operators.Parser
PrettiesAgda.Compiler.JS.Pretty
prettiesAgda.Compiler.JS.Pretty
Pretty 
1 (Type/Class)Agda.Utils.Pretty
2 (Type/Class)Agda.Compiler.JS.Pretty
pretty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
prettyA 
1 (Function)Agda.Syntax.Abstract.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyATopAgda.Syntax.Abstract.Pretty
prettyBehaviourAgda.Termination.CallGraph
PrettyContext 
1 (Type/Class)Agda.TypeChecking.Pretty
2 (Data Constructor)Agda.TypeChecking.Pretty
prettyContextAgda.Interaction.GhciTop
prettyEpicAgda.Compiler.Epic.Epic
prettyEpicFunAgda.Compiler.Epic.Epic
prettyErrorAgda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyGraphAgda.TypeChecking.Positivity
prettyListAgda.TypeChecking.Pretty
prettyPrecAgda.Utils.Pretty
prettyPrintAgda.Compiler.MAlonzo.Pretty
PrettyTCMAgda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyTCMAgda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyTypeOfMetaAgda.Interaction.GhciTop
preUscoreAgda.Interaction.GhciTop
PreviousInputAgda.Syntax.Parser.Alex
prFalseAgda.Compiler.Epic.Primitive
PrimAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primAgdaDataDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataConstructorAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionFunDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionPostulateAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionPrimitiveAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionRecordDefAgda.TypeChecking.Monad.Builtin
primAgdaFunDefAgda.TypeChecking.Monad.Builtin
primAgdaRecordDefAgda.TypeChecking.Monad.Builtin
primAgdaSortAgda.TypeChecking.Monad.Builtin
primAgdaSortLitAgda.TypeChecking.Monad.Builtin
primAgdaSortSetAgda.TypeChecking.Monad.Builtin
primAgdaSortUnsupportedAgda.TypeChecking.Monad.Builtin
primAgdaTermAgda.TypeChecking.Monad.Builtin
primAgdaTermConAgda.TypeChecking.Monad.Builtin
primAgdaTermDefAgda.TypeChecking.Monad.Builtin
primAgdaTermLamAgda.TypeChecking.Monad.Builtin
primAgdaTermPiAgda.TypeChecking.Monad.Builtin
primAgdaTermSortAgda.TypeChecking.Monad.Builtin
primAgdaTermUnsupportedAgda.TypeChecking.Monad.Builtin
primAgdaTermVarAgda.TypeChecking.Monad.Builtin
primAgdaTypeAgda.TypeChecking.Monad.Builtin
primAgdaTypeElAgda.TypeChecking.Monad.Builtin
primArgAgda.TypeChecking.Monad.Builtin
primArgArgAgda.TypeChecking.Monad.Builtin
primBodyAgda.Compiler.MAlonzo.Primitives
primBoolAgda.TypeChecking.Monad.Builtin
primCharAgda.TypeChecking.Monad.Builtin
primClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primConsAgda.TypeChecking.Monad.Builtin
primDataConstructorsAgda.TypeChecking.Primitive
PrimeAgda.Utils.Suffix
primEqualityAgda.TypeChecking.Monad.Builtin
primExprAgda.Compiler.Epic.Primitive
primFalseAgda.TypeChecking.Monad.Builtin
primFlatAgda.TypeChecking.Monad.Builtin
primFloatAgda.TypeChecking.Monad.Builtin
PrimFun 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunAgda.Compiler.Epic.Primitive
primFunArityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunImplementationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primHiddenAgda.TypeChecking.Monad.Builtin
primHidingAgda.TypeChecking.Monad.Builtin
PrimImplAgda.TypeChecking.Primitive
primInfAgda.TypeChecking.Monad.Builtin
primInstanceAgda.TypeChecking.Monad.Builtin
primIntegerAgda.TypeChecking.Monad.Builtin
primIOAgda.TypeChecking.Monad.Builtin
primIrrelevantAgda.TypeChecking.Monad.Builtin
Primitive 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
4 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PrimitiveFunctionAgda.Syntax.Concrete.Definitions
primitiveFunctionsAgda.TypeChecking.Primitive
PrimitiveImplAgda.TypeChecking.Primitive
PrimitiveTypeAgda.Interaction.Highlighting.Precise
primitiviseAgda.Compiler.Epic.Primitive
primLevelAgda.TypeChecking.Monad.Builtin
primLevelMaxAgda.TypeChecking.Monad.Builtin
primLevelSucAgda.TypeChecking.Monad.Builtin
primLevelZeroAgda.TypeChecking.Monad.Builtin
primListAgda.TypeChecking.Monad.Builtin
primNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primNatAgda.TypeChecking.Monad.Builtin
primNatCaseZDAgda.Compiler.Epic.Primitive
primNatCaseZSAgda.Compiler.Epic.Primitive
primNatDivSucAuxAgda.TypeChecking.Monad.Builtin
primNatEqualityAgda.TypeChecking.Monad.Builtin
primNatLessAgda.TypeChecking.Monad.Builtin
primNatMinusAgda.TypeChecking.Monad.Builtin
primNatModSucAuxAgda.TypeChecking.Monad.Builtin
primNatPlusAgda.TypeChecking.Monad.Builtin
primNatTimesAgda.TypeChecking.Monad.Builtin
primNilAgda.TypeChecking.Monad.Builtin
primQNameAgda.TypeChecking.Monad.Builtin
primQNameDefinitionAgda.TypeChecking.Primitive
primQNameTypeAgda.TypeChecking.Primitive
primReflAgda.TypeChecking.Monad.Builtin
primRelevantAgda.TypeChecking.Monad.Builtin
primRelvanceAgda.TypeChecking.Monad.Builtin
primSharpAgda.TypeChecking.Monad.Builtin
primSizeAgda.TypeChecking.Monad.Builtin
primSizeInfAgda.TypeChecking.Monad.Builtin
primSizeSucAgda.TypeChecking.Monad.Builtin
primStringAgda.TypeChecking.Monad.Builtin
primSucAgda.TypeChecking.Monad.Builtin
PrimTagAgda.Compiler.Epic.Interface
PrimTermAgda.TypeChecking.Primitive
primTermAgda.TypeChecking.Primitive
PrimTFAgda.Compiler.Epic.Primitive
PrimTransformAgda.Compiler.Epic.Primitive
primTrueAgda.TypeChecking.Monad.Builtin
primTrustMeAgda.TypeChecking.Primitive
PrimTypeAgda.TypeChecking.Primitive
primTypeAgda.TypeChecking.Primitive
primVisibleAgda.TypeChecking.Monad.Builtin
primZeroAgda.TypeChecking.Monad.Builtin
printAgda.Utils.IO.Locale
printTestCaseAgda.Utils.QuickCheck
printUsageAgda.Main
printVersionAgda.Main
PrioAgda.Auto.NarrowingSearch
prioAbsurdLambdaAgda.Auto.SearchControl
prioCompareArgListAgda.Auto.SearchControl
prioCompBetaAgda.Auto.SearchControl
prioCompBetaStructuredAgda.Auto.SearchControl
prioCompChoiceAgda.Auto.SearchControl
prioCompCopyAgda.Auto.SearchControl
prioCompIotaAgda.Auto.SearchControl
prioCompUnifAgda.Auto.SearchControl
prioInferredTypeUnknownAgda.Auto.SearchControl
PrioMeta 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
prioNoAgda.Auto.SearchControl
prioNoIotaAgda.Auto.SearchControl
prioProjIndexAgda.Auto.SearchControl
prioTypecheckAgda.Auto.SearchControl
prioTypecheckArgListAgda.Auto.SearchControl
prioTypeUnknownAgda.Auto.SearchControl
PrivateAgda.Syntax.Concrete
PrivateAccessAgda.Syntax.Common
PrivateNSAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
prNatEqualityAgda.Compiler.Epic.Primitive
Problem 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
Problem'Agda.TypeChecking.Rules.LHS.Problem
ProblemConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ProblemId 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
problemInPatAgda.TypeChecking.Rules.LHS.Problem
problemOutPatAgda.TypeChecking.Rules.LHS.Problem
ProblemPartAgda.TypeChecking.Rules.LHS.Problem
problemTelAgda.TypeChecking.Rules.LHS.Problem
ProjAgda.Syntax.Internal
ProjectRootAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
projectRootAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
promoteAgda.Utils.QuickCheck
proofIrrelevanceAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Prop 
1 (Type/Class)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Auto.NarrowingSearch
3 (Data Constructor)Agda.Syntax.Concrete
4 (Data Constructor)Agda.Syntax.Internal
5 (Data Constructor)Agda.Syntax.Abstract
propAgda.Syntax.Internal
propagatePrioAgda.Auto.NarrowingSearch
PropertyAgda.Utils.QuickCheck
propertyAgda.Utils.QuickCheck
propFreqAgda.TypeChecking.Test.Generators
PropMustBeSingletonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
prop_disjointAgda.Utils.Warshall
prop_distinct_fastDistinctAgda.Utils.List
prop_extractNthElementAgda.Utils.List
prop_flattenTelInvAgda.TypeChecking.Tests
prop_flattenTelScopeAgda.TypeChecking.Tests
prop_genericElemIndexAgda.Utils.List
prop_groupBy'Agda.Utils.List
prop_pathAgda.Utils.Warshall
prop_reorderTelStableAgda.TypeChecking.Tests
prop_smallerAgda.Utils.Warshall
prop_splitTelescopePermScopeAgda.TypeChecking.Tests
prop_splitTelescopeScopeAgda.TypeChecking.Tests
prop_stableAgda.Utils.Warshall
prop_telToListInvAgda.TypeChecking.Tests
prop_uniqByAgda.Utils.List
prop_wellScopedVarsAgda.TypeChecking.Test.Generators
prop_zipWith'Agda.Utils.List
prPredAgda.Compiler.Epic.Primitive
prSucAgda.Compiler.Epic.Primitive
prTrueAgda.Compiler.Epic.Primitive
pruneAgda.TypeChecking.MetaVars.Occurs
PrunedEverythingAgda.TypeChecking.MetaVars.Occurs
PrunedNothingAgda.TypeChecking.MetaVars.Occurs
PrunedSomethingAgda.TypeChecking.MetaVars.Occurs
PruneResultAgda.TypeChecking.MetaVars.Occurs
prZeroAgda.Compiler.Epic.Primitive
PStateAgda.Syntax.Parser.Monad
PStrAgda.Utils.Pretty
ptextAgda.Utils.Pretty
PtrAgda.Utils.Pointer
PublicAccessAgda.Syntax.Common
publicModulesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
PublicNSAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
publicOpenAgda.Syntax.Concrete
punctAgda.Compiler.JS.Parser
punctuate 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
pureTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
pushContextAgda.Syntax.Parser.Monad
pushCurrentContextAgda.Syntax.Parser.Monad
pushLexStateAgda.Syntax.Parser.Monad
putConArityAgda.Compiler.Epic.CompileState
putConstrTagAgda.Compiler.Epic.CompileState
putDelayedAgda.Compiler.Epic.CompileState
putForcedArgsAgda.Compiler.Epic.CompileState
putMainAgda.Compiler.Epic.CompileState
putResponseAgda.Interaction.EmacsCommand
putStrAgda.Utils.IO.Locale
putStrLnAgda.Utils.IO.Locale
pwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
QAgda.Interaction.EmacsCommand
QName 
1 (Type/Class)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
4 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameAgda.Compiler.JS.Compiler
qnameFromListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qnameToConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameToListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qnameToMNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qNameTypeAgda.TypeChecking.Quote
QPBAgda.Auto.NarrowingSearch
QPBlockedAgda.Auto.NarrowingSearch
QPDoubleBlockedAgda.Auto.NarrowingSearch
QualAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qualify 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qualifyMAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
qualifyQAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
QuestionMark 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quickCheckAgda.Utils.QuickCheck
quickCheck'Agda.Utils.QuickCheck
quickCheckResultAgda.Utils.QuickCheck
quickCheckWithAgda.Utils.QuickCheck
quickCheckWith'Agda.Utils.QuickCheck
quickCheckWithResultAgda.Utils.QuickCheck
Quote 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quoteAgda.Utils.String
quotedAgda.Compiler.JS.Parser
QuoteGoal 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quoteNameAgda.TypeChecking.Quote
quotesAgda.Utils.Pretty
QuoteTerm 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quoteTermAgda.TypeChecking.Quote
quoteTypeAgda.TypeChecking.Quote
quotingKitAgda.TypeChecking.Quote
RAgda.Utils.Map
RaiseAgda.TypeChecking.Substitute
raiseAgda.TypeChecking.Substitute
raiseFromAgda.TypeChecking.Substitute
Range 
1 (Type/Class)Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Position, Agda.Interaction.GhciTop
3 (Type/Class)Agda.Interaction.Highlighting.Range
4 (Data Constructor)Agda.Interaction.Highlighting.Range
RangeAndPragma 
1 (Type/Class)Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
rangeInvariant 
1 (Function)Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Function)Agda.Interaction.Highlighting.Range
rangesAgda.Utils.QuickCheck
rangeToIntervalAgda.Syntax.Position, Agda.Interaction.GhciTop
rationalAgda.Utils.Pretty
RawAppAgda.Syntax.Concrete
RawAppPAgda.Syntax.Concrete
RBAgda.Termination.Lexicographic
rbraceAgda.Utils.Pretty
rbrackAgda.Utils.Pretty
RConstAgda.Utils.Warshall
reAbsAgda.TypeChecking.Substitute
readBinaryFile'Agda.Utils.IO.Binary
readInterfaceAgda.Interaction.Imports
readlineAgda.Interaction.Monad
readMAgda.Utils.Monad
ReadPAgda.Utils.ReadP
readTextFileAgda.Utils.IO.UTF8
reallyUnLevelViewAgda.TypeChecking.Level
reasonAgda.Utils.QuickCheck
rebindClauseAgda.TypeChecking.Rebind
rebindPrimitiveAgda.TypeChecking.Primitive
rebuildAgda.Syntax.Concrete.Operators.Parser
rebuildBindingAgda.Syntax.Concrete.Operators.Parser
Rec 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recalcAgda.Auto.NarrowingSearch
recalcsAgda.Auto.NarrowingSearch
recArgOccurrencesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecBehaviourAgda.Termination.Lexicographic
recBehaviourInvariantAgda.Termination.Lexicographic
reccalcAgda.Auto.NarrowingSearch
recClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recConTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecDef 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Concrete.Definitions
recEtaEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recNamedConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Record 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recordModuleAgda.TypeChecking.Records
RecordModuleIFS 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
RecordsAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
RecordSigAgda.Syntax.Concrete
recParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recPolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecSigAgda.Syntax.Abstract
recTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
RecUpdate 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
recursiveAgda.Syntax.Concrete.Operators.Parser
redBindAgda.TypeChecking.Primitive
redReturnAgda.TypeChecking.Primitive
ReduceAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
reduceAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
reduceBAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
reduceConAgda.TypeChecking.Rules.Term
Reduced 
1 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reduceHeadAgda.TypeChecking.Injectivity
RefCreateEnvAgda.Auto.NarrowingSearch
RefinableAgda.Auto.NarrowingSearch
refine 
1 (Function)Agda.Compiler.JS.Case
2 (Function)Agda.Interaction.BasicOps
refinementsAgda.Auto.NarrowingSearch
refineMetaAgda.Interaction.CommandLine.CommandLine
RefInfoAgda.Auto.Syntax
refreshStrAgda.Interaction.GhciTop
ReifyAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyAppAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyDisplayFormAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyDisplayFormPAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
reifyPatternsAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
Rel 
1 (Data Constructor)Agda.Compiler.Epic.Interface
2 (Type/Class)Agda.TypeChecking.Primitive
RelativeToAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Relevance 
1 (Type/Class)Agda.Syntax.Common
2 (Type/Class)Agda.Compiler.Epic.Interface
relevanciesAgda.Compiler.Epic.Erasure
RelevantAgda.Syntax.Common
relevantAgda.Compiler.Epic.Erasure
RelevantArgsAgda.Compiler.Epic.Interface
relevantArgsAgda.Compiler.Epic.Interface
relevantInAgda.TypeChecking.Free
relevantVarsAgda.TypeChecking.Free
relOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
remAbsAgda.Compiler.Epic.Injection
remForcedAgda.Compiler.Epic.Forcing
removeInteractionPointAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
removeOnlyQualifiedAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
removeUnusedAgda.Compiler.Epic.Erasure
removevarAgda.Auto.CaseSplit
RenAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
renAgda.Auto.CaseSplit
rename 
1 (Function)Agda.Auto.CaseSplit
2 (Function)Agda.TypeChecking.Substitute
renameCanonicalNamesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
renameFromAgda.TypeChecking.Substitute
renamePAgda.TypeChecking.Telescope
renamepAgda.Auto.CaseSplit
Renaming 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
renaming 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.TypeChecking.Telescope
renamingRAgda.TypeChecking.Telescope
rEndAgda.Syntax.Position, Agda.Interaction.GhciTop
renderAgda.Utils.Pretty
renderStyleAgda.Utils.Pretty
renFromAgda.Syntax.Concrete
renToAgda.Syntax.Concrete
renToRangeAgda.Syntax.Concrete
reorderAgda.Compiler.JS.Compiler
reorder'Agda.Compiler.JS.Compiler
reorderTelAgda.TypeChecking.Telescope
reorderTel_Agda.TypeChecking.Telescope
RepeatedVariablesInPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
replAgda.Compiler.MAlonzo.Primitives
replaceAgda.Auto.CaseSplit
replaceAtAgda.Compiler.Epic.CompileState
replaceForcedAgda.Compiler.Epic.Forcing
replaceFunCCAgda.Compiler.Epic.Injection
replacepAgda.Auto.CaseSplit
replayAgda.Utils.QuickCheck
reportAgda.Compiler.Epic.Forcing
reportPostponingAgda.TypeChecking.Rules.LHS.Unify
reportSAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
reportSDocAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
reportSLnAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
requireLevelsAgda.TypeChecking.Level
resetAllStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
resetNameSupplyAgda.Compiler.Epic.CompileState
resetStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
resizeAgda.Utils.QuickCheck
resizeConfAgda.TypeChecking.Test.Generators
ResolvedNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
resolveModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
resolveNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
Restore 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
restrictPrivateAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Result 
1 (Type/Class)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Termination.TermCheck
retryConstraintsAgda.Interaction.CommandLine.CommandLine
ReturnAgda.Interaction.CommandLine.CommandLine
returnBlockAgda.Compiler.JS.Parser
reverseCCBodyAgda.Compiler.Epic.FromAgda
reversePAgda.Utils.Permutation
RewriteAgda.Interaction.BasicOps
rewriteAgda.Interaction.BasicOps
RewriteRHSAgda.Syntax.Abstract
RHS 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Abstract
ribbonsPerLineAgda.Utils.Pretty
RICheckElimAgda.Auto.Syntax
RICheckProjIndexAgda.Auto.Syntax
RICopyInfoAgda.Auto.Syntax
rieDefFreeVarsAgda.Auto.Syntax
rieEqReasoningConstsAgda.Auto.Syntax
rieHintsAgda.Auto.Syntax
RIEnvAgda.Auto.Syntax
RIEqRStateAgda.Auto.Syntax
RightAssocAgda.Syntax.Fixity
RightDisjunctAgda.Auto.NarrowingSearch
rightDistributiveAgda.Utils.TestHelpers
RightHandSideAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
rightHHAgda.TypeChecking.Rules.LHS.Unify
RightOperandCtxAgda.Syntax.Fixity
Rigid 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.Utils.Warshall
3 (Data Constructor)Agda.TypeChecking.MetaVars.Occurs
4 (Data Constructor)Agda.TypeChecking.SizedTypes
RigidIdAgda.Utils.Warshall
rigidVarsAgda.TypeChecking.Free
RIInferredTypeUnknownAgda.Auto.Syntax
RIIotaStepAgda.Auto.Syntax
RIMainInfoAgda.Auto.Syntax
RINotConstructorAgda.Auto.Syntax
RIPickSubsvarAgda.Auto.Syntax
RIUnifInfoAgda.Auto.Syntax
RIUsedVarsAgda.Auto.Syntax
rmAgda.Auto.CaseSplit
rollbackAgda.Syntax.Parser.LookAhead
roundFixBracketsAgda.Syntax.Fixity
row 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
rowdescrAgda.Utils.Warshall
rows 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
rparenAgda.Utils.Pretty
rStartAgda.Syntax.Position, Agda.Interaction.GhciTop
rteModuleAgda.Compiler.MAlonzo.Compiler
rtmErrorAgda.Compiler.MAlonzo.Misc
rtmIncompleteMatchAgda.Compiler.MAlonzo.Misc
rtmModAgda.Compiler.MAlonzo.Misc
rtmQualAgda.Compiler.MAlonzo.Misc
rtmVarAgda.Compiler.MAlonzo.Misc
rToRAgda.Interaction.Highlighting.Range
runAbsToConAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
runAgdaAgda.Main
runExceptionTAgda.TypeChecking.Monad.Exception
runIMAgda.Interaction.Monad
runLookAheadAgda.Syntax.Parser.LookAhead
runNiceAgda.Syntax.Concrete.Definitions
runTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTCM'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runTestsAgda.Utils.TestHelpers
runUndoAgda.Auto.NarrowingSearch
RVarAgda.Utils.Warshall
S 
1 (Type/Class)Agda.Auto.Convert
2 (Data Constructor)Agda.Auto.Convert
SafeFlagPostulateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeFlagPragmaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SafeFlagPrimTrustMeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SameAgda.Compiler.Epic.Injection
sameVarsAgda.TypeChecking.Conversion
sampleAgda.Utils.QuickCheck
sample'Agda.Utils.QuickCheck
satisfyAgda.Utils.ReadP
sccomcountAgda.Auto.NarrowingSearch
scflipAgda.Auto.NarrowingSearch
sCheckedAgda.Interaction.GhciTop
SClauseAgda.TypeChecking.Coverage
sConstsAgda.Auto.Convert
Scope 
1 (Type/Class)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
3 (Type/Class)Agda.Utils.Warshall
ScopeCheckDeclarationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ScopeCheckExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
scopeCheckImportAgda.Interaction.Imports
ScopeCheckLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
scopeCurrentAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopedDeclAgda.Syntax.Abstract
ScopedExprAgda.Syntax.Abstract
scopeImportsAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopeInfo 
1 (Type/Class)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeLocalsAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeLookupAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeLookup'Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ScopeMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
scopeModulesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeNameSpacesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopeParentsAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scopePrecedenceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
scPatsAgda.TypeChecking.Coverage
scPermAgda.TypeChecking.Coverage
scsub1Agda.Auto.NarrowingSearch
scsub2Agda.Auto.NarrowingSearch
scSubstAgda.TypeChecking.Coverage
scTelAgda.TypeChecking.Coverage
sCurMetaAgda.Auto.Convert
secFreeVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
secondPartAgda.TypeChecking.Telescope
secTelescopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Section 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SectionApp 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
SectionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SelfAgda.Compiler.JS.Syntax
selfAgda.Compiler.JS.Substitution
semiAgda.Utils.Pretty
SemiRing 
1 (Type/Class)Agda.Utils.SemiRing
2 (Type/Class)Agda.Termination.Semiring
Semiring 
1 (Type/Class)Agda.Termination.Semiring
2 (Data Constructor)Agda.Termination.Semiring
semiringInvariantAgda.Termination.Semiring
sep 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
sepByAgda.Utils.ReadP
sepBy1Agda.Utils.ReadP
seqcAgda.Auto.NarrowingSearch
seqctxAgda.Auto.CaseSplit
sEqsAgda.Auto.Convert
Set 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
setAgda.Syntax.Internal
set0Agda.Syntax.Internal
setArgOccurrencesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setBuiltinThingsAgda.TypeChecking.Monad.Builtin
setCommandLineOptions 
1 (Function)Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
2 (Function)Agda.Interaction.GhciTop
setContextPrecedenceAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setCurrentModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setCurrentRangeAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
setDecodedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
setExtLambdaTeleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setFreqsAgda.TypeChecking.Test.Generators
setImportedSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setIncludeDirsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setInputAgda.Syntax.Parser.LookAhead
setInputFileAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setInterfaceAgda.Compiler.MAlonzo.Misc
setLastPosAgda.Syntax.Parser.Monad
setLexInputAgda.Syntax.Parser.Alex
setLocalVarsAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
setMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
SetNAgda.Syntax.Concrete
setNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
setOptionsFromPragmaAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setParsePosAgda.Syntax.Parser.Monad
setPolarityAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setPragmaOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setPrevTokenAgda.Syntax.Parser.Monad
SetRange 
1 (Type/Class)Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
setScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setScopeAccessAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
setShowImplicitArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setTagAgda.Compiler.Epic.Injection
setTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setVisitedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
severalAgda.Interaction.Highlighting.Precise
ShadowedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShapeViewAgda.TypeChecking.Rules.LHS.Unify
shapeViewAgda.TypeChecking.Rules.LHS.Unify
shapeViewHHAgda.TypeChecking.Rules.LHS.Unify
shiftAgda.Compiler.JS.Substitution
shifterAgda.Compiler.JS.Substitution
shiftFromAgda.Compiler.JS.Substitution
ShouldBeApplicationOfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeAppliedToTheDatatypeParametersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeASortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBePiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldBeRecordTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ShouldEndInApplicationOfTheDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
shouldEtaContractImplicitAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
shouldReifyInteractionPointsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showAAgda.Syntax.Abstract.Pretty
showATopAgda.Syntax.Abstract.Pretty
showChar'Agda.Syntax.Concrete.Pretty
showComparisonAgda.Interaction.BasicOps
showConstraintsAgda.Interaction.CommandLine.CommandLine
showContextAgda.Interaction.CommandLine.CommandLine
showHighlightingInfoAgda.Interaction.Highlighting.Emacs
showImplicitArgsAgda.Interaction.GhciTop
showImplicitArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showIndexAgda.Utils.String
showMetasAgda.Interaction.CommandLine.CommandLine
showModuleContentsAgda.Interaction.GhciTop
showNumIIdAgda.Interaction.GhciTop
showPatAgda.TypeChecking.With
showQNameIdAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
showScopeAgda.Interaction.CommandLine.CommandLine
showStatusAgda.Interaction.GhciTop
showString'Agda.Syntax.Concrete.Pretty
shrinkAgda.Utils.QuickCheck
Shrink2 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
ShrinkCAgda.TypeChecking.Test.Generators
shrinkCAgda.TypeChecking.Test.Generators
Shrinking 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
shrinkingAgda.Utils.QuickCheck
shrinkInitAgda.Utils.QuickCheck
shrinkIntegralAgda.Utils.QuickCheck
shrinkNothingAgda.Utils.QuickCheck
shrinkRealFracAgda.Utils.QuickCheck
ShrinkStateAgda.Utils.QuickCheck
shrinkStateAgda.Utils.QuickCheck
SideconditionAgda.Auto.NarrowingSearch
SigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigDefinitionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigMNameAgda.Compiler.MAlonzo.Misc
SignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sigSectionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
simplifyLevelConstraintAgda.TypeChecking.LevelConstraints
singleConstructorTypeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
singleton 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Graph
3 (Function)Agda.Utils.Trie
4 (Function)Agda.Interaction.Highlighting.Precise
SingletonRecordsAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
Size 
1 (Type/Class)Agda.Termination.SparseMatrix
2 (Data Constructor)Agda.Termination.SparseMatrix
3 (Type/Class)Agda.Termination.Matrix
4 (Data Constructor)Agda.Termination.Matrix
size 
1 (Function)Agda.Utils.Size
2 (Function)Agda.Termination.SparseMatrix
3 (Function)Agda.Termination.Matrix
4 (Function)Agda.Termination.Lexicographic
SizeConstAgda.Utils.Warshall
SizeConstraintAgda.TypeChecking.SizedTypes
SizedAgda.Utils.Size
sizedAgda.Utils.QuickCheck
SizedList 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
sizedTextAgda.Utils.Pretty
SizeExpr 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.SizedTypes
sizeExprAgda.TypeChecking.SizedTypes
SizeInfAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeInvariant 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
SizeMetaAgda.TypeChecking.SizedTypes
sizePolarityAgda.TypeChecking.Polarity
sizeRigidAgda.Utils.Warshall
SizeSucAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSucAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeTypeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeVarAgda.Utils.Warshall
SizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SkipAgda.Auto.Syntax
skipBlockAgda.Syntax.Parser.Comments
skipManyAgda.Utils.ReadP
skipMany1Agda.Utils.ReadP
skipSpacesAgda.Utils.ReadP
sLubAgda.TypeChecking.Substitute
sMainMetaAgda.Auto.Convert
smallestPosAgda.Interaction.Highlighting.Precise
Smart 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
smash'emAgda.Compiler.Epic.Smashing
smashableAgda.Compiler.Epic.Smashing
smashTelAgda.Syntax.Concrete.Pretty
sMetasAgda.Auto.Convert
SolAgda.Auto.CaseSplit
SolutionAgda.Utils.Warshall
solve 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.Compiler.Epic.Injection
solveAwakeConstraintsAgda.TypeChecking.Constraints
solveConstraintAgda.TypeChecking.Constraints
solveConstraint_Agda.TypeChecking.Constraints
solveSizeConstraintsAgda.TypeChecking.SizedTypes
solvingProblemAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
SomeWhereAgda.Syntax.Concrete
Sort 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.Auto.Syntax
3 (Type/Class)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Internal
sortAgda.Syntax.Internal
SortCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortFreqAgda.TypeChecking.Test.Generators
SortFreqs 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
sortFreqsAgda.TypeChecking.Test.Generators
SortHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
sortInteractionPointsAgda.Interaction.GhciTop
sortOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
SortShAgda.TypeChecking.Rules.LHS.Unify
sortTmAgda.TypeChecking.Substitute
sourceAgda.Termination.CallGraph
SourceToModuleAgda.Interaction.FindFile
sourceToModuleAgda.Interaction.FindFile
spaceAgda.Utils.Pretty
splashScreenAgda.Interaction.CommandLine.CommandLine
SplitAgda.TypeChecking.Rules.LHS.Problem
splitAgda.TypeChecking.Coverage
split'Agda.TypeChecking.Coverage
splitCAgda.TypeChecking.CompiledClause.Compile
SplitClauseAgda.TypeChecking.Coverage
splitClauseAgda.TypeChecking.Coverage
splitClauseWithAbsAgda.TypeChecking.Coverage
SplitError 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Type/Class)Agda.TypeChecking.Coverage
splitOnAgda.TypeChecking.CompiledClause.Compile
SplitOnIrrelevantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
SplitPanicAgda.TypeChecking.Rules.LHS.Problem
splitPermAgda.TypeChecking.Telescope
SplitProblemAgda.TypeChecking.Rules.LHS.Problem
splitProblemAgda.TypeChecking.Rules.LHS.Split
SplitTel 
1 (Type/Class)Agda.TypeChecking.Telescope
2 (Data Constructor)Agda.TypeChecking.Telescope
splitTelescopeAgda.TypeChecking.Telescope
square 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
srcFileAgda.Syntax.Position, Agda.Interaction.GhciTop
SResAgda.Auto.NarrowingSearch
sShowImplicitArgumentsAgda.Interaction.GhciTop
sSucAgda.Syntax.Internal
StackAgda.TypeChecking.CompiledClause.Match
standardOptions_Agda.Interaction.Options
startPosAgda.Syntax.Position, Agda.Interaction.GhciTop
State 
1 (Type/Class)Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Interaction.GhciTop
StaticPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
StatisticsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Status 
1 (Type/Class)Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Interaction.GhciTop
statusAgda.Interaction.GhciTop
stAwakeConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stBuiltinThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stCurrentModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stdArgsAgda.Utils.QuickCheck
stDecodedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stdoutFlushAgda.Utils.IO.Locale
stealConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
stepAgda.Compiler.Epic.Erasure
stExtLambdaTeleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stFreshThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stHaskellImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedBuiltinsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stInteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stLocalBuiltinsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stModuleToSourceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stMutualBlocksAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
storeAgda.Utils.Pointer
storeDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
stPersistentAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPersistentOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Str 
1 (Type/Class)Agda.Utils.QuickCheck
2 (Data Constructor)Agda.Utils.Pretty
3 (Type/Class)Agda.TypeChecking.Primitive
4 (Data Constructor)Agda.TypeChecking.Primitive
StrictAgda.Syntax.Strict
strictAgda.Syntax.Strict
String 
1 (Data Constructor)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
stringAgda.Utils.ReadP
stringChrAgda.Compiler.JS.Parser
stringLitAgda.Compiler.JS.Parser
stringPartsAgda.Syntax.Notation
stringStrAgda.Compiler.JS.Parser
stripImplicitsAgda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
stripNoNamesAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
stripWithClausePatternsAgda.TypeChecking.With
stronglyAgda.TypeChecking.MetaVars.Occurs
StronglyRigid 
1 (Data Constructor)Agda.TypeChecking.Free
2 (Data Constructor)Agda.TypeChecking.MetaVars.Occurs
StronglyRigidOccurrenceAgda.TypeChecking.Rules.LHS.Unify
stronglyRigidVarsAgda.TypeChecking.Free
stScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stSleepingConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stStatisticsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stVisitedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Style 
1 (Type/Class)Agda.Utils.Pretty
2 (Data Constructor)Agda.Utils.Pretty
styleAgda.Utils.Pretty
Sub 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.TypeChecking.Rules.LHS.Unify
subAgda.Auto.Syntax
SubConstraints 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
subiAgda.Auto.Syntax
SubstAgda.TypeChecking.Substitute
subst 
1 (Function)Agda.Compiler.JS.Substitution
2 (Function)Agda.Compiler.Epic.AuxAST
3 (Function)Agda.TypeChecking.Substitute
subst'Agda.Compiler.JS.Substitution
substBodyAgda.TypeChecking.CompiledClause.Compile
substBranchAgda.Compiler.Epic.AuxAST
substForDotAgda.Compiler.Epic.Injection
SubstHHAgda.TypeChecking.Rules.LHS.Unify
substHHAgda.TypeChecking.Rules.LHS.Unify
substituterAgda.Compiler.JS.Substitution
Substitution 
1 (Type/Class)Agda.TypeChecking.Substitute
2 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
substLitAgda.Compiler.Epic.FromAgda
substs 
1 (Function)Agda.Compiler.Epic.AuxAST
2 (Function)Agda.TypeChecking.Substitute
substTermAgda.Compiler.Epic.FromAgda
substUnderAgda.TypeChecking.Substitute
substUnderHHAgda.TypeChecking.Rules.LHS.Unify
subsvarsAgda.Auto.SearchControl
subtractAgda.Utils.VarSet
SuccessAgda.Utils.QuickCheck
suchThatAgda.Utils.QuickCheck
suchThatMaybeAgda.Utils.QuickCheck
sucNameAgda.TypeChecking.Level
Suffix 
1 (Type/Class)Agda.Utils.Suffix
2 (Type/Class)Agda.Utils.List
suffixViewAgda.Utils.Suffix
supremumAgda.Termination.CallGraph
SymArrowAgda.Syntax.Parser.Tokens
SymAsAgda.Syntax.Parser.Tokens
SymBarAgda.Syntax.Parser.Tokens
Symbol 
1 (Type/Class)Agda.Syntax.Parser.Tokens
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
symbolAgda.Syntax.Parser.LexActions
SymCloseBraceAgda.Syntax.Parser.Tokens
SymCloseParenAgda.Syntax.Parser.Tokens
SymClosePragmaAgda.Syntax.Parser.Tokens
SymCloseVirtualBraceAgda.Syntax.Parser.Tokens
SymColonAgda.Syntax.Parser.Tokens
SymDotAgda.Syntax.Parser.Tokens
SymDotDotAgda.Syntax.Parser.Tokens
SymDoubleCloseBraceAgda.Syntax.Parser.Tokens
SymDoubleOpenBraceAgda.Syntax.Parser.Tokens
SymEllipsisAgda.Syntax.Parser.Tokens
SymEqualAgda.Syntax.Parser.Tokens
SymLambdaAgda.Syntax.Parser.Tokens
SymOpenBraceAgda.Syntax.Parser.Tokens
SymOpenParenAgda.Syntax.Parser.Tokens
SymOpenPragmaAgda.Syntax.Parser.Tokens
SymOpenVirtualBraceAgda.Syntax.Parser.Tokens
SymQuestionMarkAgda.Syntax.Parser.Tokens
SymSemiAgda.Syntax.Parser.Tokens
SymUnderscoreAgda.Syntax.Parser.Tokens
SymVirtualSemiAgda.Syntax.Parser.Tokens
syncAgda.Syntax.Parser.LookAhead
SyntaxAgda.Syntax.Concrete
SyntaxBindingLambdaAgda.Syntax.Concrete
syntaxOfAgda.Syntax.Fixity
Tag 
1 (Type/Class)Agda.Compiler.JS.Case
2 (Data Constructor)Agda.Compiler.JS.Case
3 (Type/Class)Agda.Compiler.Epic.Interface
4 (Data Constructor)Agda.Compiler.Epic.Interface
tag 
1 (Function)Agda.Compiler.JS.Case
2 (Function)Agda.Compiler.JS.Compiler
TagEqAgda.Compiler.Epic.Injection
TaggedAgda.Compiler.JS.Case
Tags 
1 (Type/Class)Agda.Compiler.Epic.Injection
2 (Data Constructor)Agda.Compiler.Epic.Injection
tagsAgda.Compiler.JS.Case
takeAwakeConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
takeEqualitiesAgda.TypeChecking.Rules.LHS.Unify
takeIAgda.Syntax.Position, Agda.Interaction.GhciTop
takenNameStrAgda.Interaction.GhciTop
takePAgda.Utils.Permutation
takeRelevantAgda.TypeChecking.MetaVars.Occurs
takeTeleAgda.Compiler.Epic.Forcing
targetAgda.Termination.CallGraph
TBind 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
tcargsAgda.Auto.Typecheck
tcConstructorNamesAgda.TypeChecking.Test.Generators
tcDefinedNamesAgda.TypeChecking.Test.Generators
TCEnv 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCErr 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCErr'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcErrStringAgda.TypeChecking.Errors, Agda.Interaction.GhciTop
tcExpAgda.Auto.Typecheck
tcFixSizeAgda.TypeChecking.Test.Generators
tcFreeVariablesAgda.TypeChecking.Test.Generators
tcFrequenciesAgda.TypeChecking.Test.Generators
tcIsTypeAgda.TypeChecking.Test.Generators
tcLiteralsAgda.TypeChecking.Test.Generators
TCM 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcSearchAgda.Auto.Typecheck
TCStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TelCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TeleAgda.Syntax.Internal
teleArgNamesAgda.TypeChecking.Telescope
teleArgsAgda.TypeChecking.Telescope
teleLamAgda.TypeChecking.Substitute
teleNamesAgda.TypeChecking.Telescope
telePiAgda.TypeChecking.Substitute
telePi_Agda.TypeChecking.Substitute
Telescope 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Abstract
telFromListAgda.TypeChecking.Substitute
TelHHAgda.TypeChecking.Rules.LHS.Unify
tellEmacsToJumpToErrorAgda.Interaction.GhciTop
telToListAgda.TypeChecking.Substitute
TelV 
1 (Type/Class)Agda.TypeChecking.Substitute
2 (Data Constructor)Agda.TypeChecking.Substitute
telVarsAgda.TypeChecking.Substitute
TelViewAgda.TypeChecking.Substitute
telViewAgda.TypeChecking.Telescope
telView'Agda.TypeChecking.Substitute
TelViewHHAgda.TypeChecking.Rules.LHS.Unify
telViewMAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
telViewUpToAgda.TypeChecking.Telescope
telViewUpToHHAgda.TypeChecking.Rules.LHS.Unify
Term 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
3 (Type/Class)Agda.Syntax.Internal
term 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
term'Agda.Compiler.MAlonzo.Compiler
TermConfAgda.TypeChecking.Test.Generators
TermConfigurationAgda.TypeChecking.Test.Generators
termDeclsAgda.Termination.TermCheck
termErrCallsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
termErrFunctionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermFreqs 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
termFreqsAgda.TypeChecking.Test.Generators
TermFunDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermHHAgda.TypeChecking.Rules.LHS.Unify
terminatesAgda.Termination.Termination
TerminationCheckFailedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TerminationError 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TerminationProblemAgda.Interaction.Highlighting.Precise
terminationProblemsAgda.Interaction.Imports
TermLikeAgda.Syntax.Internal.Generic
TestableAgda.Utils.QuickCheck
tests 
1 (Function)Agda.Utils.FileName, Agda.Interaction.FindFile
2 (Function)Agda.Syntax.Position, Agda.Interaction.GhciTop
3 (Function)Agda.Utils.List
4 (Function)Agda.Interaction.Options
5 (Function)Agda.Interaction.Highlighting.Range
6 (Function)Agda.Interaction.Highlighting.Precise
7 (Function)Agda.Syntax.Parser.Parser
8 (Function)Agda.Termination.Semiring
9 (Function)Agda.Termination.SparseMatrix
10 (Function)Agda.Termination.CallGraph
11 (Function)Agda.Termination.Matrix
12 (Function)Agda.Utils.Either
13 (Function)Agda.Termination.Lexicographic
14 (Function)Agda.Termination.Termination
15 (Function)Agda.Utils.Warshall
16 (Function)Agda.TypeChecking.Tests
17 (Function)Agda.Interaction.Highlighting.Emacs
18 (Function)Agda.Interaction.Highlighting.Generate
19 (Function)Agda.Compiler.MAlonzo.Encode
testSuiteAgda.Tests
text 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
TextDetailsAgda.Utils.Pretty
theConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theCurrentFileAgda.Interaction.GhciTop
theDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theFixityAgda.Syntax.Fixity
theInteractionPointsAgda.Interaction.GhciTop
theNotationAgda.Syntax.Fixity
theStateAgda.Interaction.GhciTop
theTCStateAgda.Interaction.GhciTop
ThingsInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
thingsInScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ThingWithFixity 
1 (Type/Class)Agda.Syntax.Fixity, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Fixity, Agda.Syntax.Concrete
threadAgda.Utils.Monad
threeAgda.Utils.TestHelpers
throwExceptionAgda.TypeChecking.Monad.Exception
throwImpossibleAgda.Utils.Impossible
tickAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
tickMaxAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
tickNAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
tlmnameAgda.Compiler.MAlonzo.Misc
tlmodOfAgda.Compiler.MAlonzo.Misc
TMAllAgda.Auto.Convert
TModeAgda.Auto.Convert
TNoBind 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
toAgda.Interaction.Highlighting.Range
ToAbstractAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
toAbstractAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
ToConcreteAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
toConcreteAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
toConcreteCtxAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
toggleImplicitArgsAgda.Interaction.GhciTop
toIFileAgda.Interaction.FindFile
TokCommentAgda.Syntax.Parser.Tokens
TokDummyAgda.Syntax.Parser.Tokens
TokenAgda.Syntax.Parser.Tokens
token 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Parser.LexActions
TokenLengthAgda.Syntax.Parser.Alex
tokensParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser, Agda.Interaction.GhciTop
TokEOFAgda.Syntax.Parser.Tokens
TokIdAgda.Syntax.Parser.Tokens
TokKeywordAgda.Syntax.Parser.Tokens
TokLiteralAgda.Syntax.Parser.Tokens
TokQIdAgda.Syntax.Parser.Tokens
TokSetNAgda.Syntax.Parser.Tokens
TokStringAgda.Syntax.Parser.Tokens
TokSymbolAgda.Syntax.Parser.Tokens
TokTeXAgda.Syntax.Parser.Tokens
toList 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Interaction.Highlighting.Range
3 (Function)Agda.Termination.CallGraph
toLists 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
TOMAgda.Auto.Convert
toMapAgda.Interaction.Highlighting.Precise
tomyAgda.Auto.Convert
tomyBodyAgda.Auto.Convert
tomyClauseAgda.Auto.Convert
tomyClausesAgda.Auto.Convert
tomyExpAgda.Auto.Convert
tomyExpsAgda.Auto.Convert
tomyIneqAgda.Auto.Convert
tomyPatAgda.Auto.Convert
tomyTypeAgda.Auto.Convert
TooFewFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooManyArgumentsInLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooManyFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
topBindingsAgda.Compiler.Epic.CompileState
topContextAgda.Syntax.Parser.Monad
TopCtxAgda.Syntax.Fixity
TopLevel 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
topLevelAgda.Compiler.JS.Parser
topLevelDeclsAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
TopLevelInfo 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
TopLevelModuleName 
1 (Type/Class)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
topLevelModuleName 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
topoSortAgda.Utils.Permutation
topSearchAgda.Auto.NarrowingSearch
topSortAgda.Syntax.Internal
top_command'Agda.Interaction.GhciTop
ToTermAgda.TypeChecking.Primitive
toTermAgda.TypeChecking.Primitive
toTopLevelModuleName 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
toVimAgda.Interaction.Highlighting.Vim
traceCallAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallCPSAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallCPS_Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallEAgda.TypeChecking.Rules.Term
traceCall_Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceFunAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
traceFun'Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
transitiveClosureAgda.Utils.Graph
translateCaseAgda.Compiler.Epic.Primitive
translateDefnAgda.Compiler.Epic.FromAgda
translateRecordPatternsAgda.TypeChecking.RecordPatterns
transposeAgda.Termination.SparseMatrix
TravAgda.Auto.NarrowingSearch
traverseAgda.Auto.NarrowingSearch
traversePiAgda.Auto.Typecheck
traverseTermAgda.Syntax.Internal.Generic
traverseTermMAgda.Syntax.Internal.Generic
TrBr 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
treatAbstractlyAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
treatAbstractly'Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
TrieAgda.Utils.Trie
trivialAgda.TypeChecking.SizedTypes
trivialHHAgda.TypeChecking.Rules.LHS.Unify
tryOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
tsetAgda.TypeChecking.Primitive
tvaldeclAgda.Compiler.MAlonzo.Compiler
twoAgda.Utils.TestHelpers
Type 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Internal
typeCheckAgda.Interaction.Imports
TypeCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TypedAssignAgda.Interaction.BasicOps
TypedBinding 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
TypedBindings 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Abstract
TypeError 
1 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
typeErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TypeHHAgda.TypeChecking.Rules.LHS.Unify
typeInAgda.Interaction.CommandLine.CommandLine
typeInCurrentAgda.Interaction.BasicOps
typeInMetaAgda.Interaction.BasicOps
typeInTypeAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
typeNameAgda.TypeChecking.Level
typeOfAgda.Interaction.CommandLine.CommandLine
typeOfBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
typeOfBV'Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
typeOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
typeOfFlatAgda.TypeChecking.Rules.Builtin.Coinduction
typeOfInfAgda.TypeChecking.Rules.Builtin.Coinduction
typeOfMetaAgda.Interaction.BasicOps
typeOfMetaMIAgda.Interaction.BasicOps
typeOfSharpAgda.TypeChecking.Rules.Builtin.Coinduction
typeOfVarAgda.TypeChecking.Coverage
TypeSigAgda.Syntax.Concrete
TypeSignature 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
typesOfHiddenMetasAgda.Interaction.BasicOps
typesOfVisibleMetasAgda.Interaction.BasicOps
UAgda.TypeChecking.Rules.LHS.Unify
UIdAgda.Auto.Syntax
umodifyIORefAgda.Auto.NarrowingSearch
unAbsAgda.Syntax.Internal
unAmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
unAppViewAgda.Syntax.Abstract.Views
unArgAgda.Syntax.Common
UnBlockAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unblockedTesterAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
unConNameAgda.TypeChecking.Test.Generators
uncurry3Agda.Utils.Tuple
undefAgda.Compiler.JS.Parser
UndefinedAgda.Compiler.JS.Syntax
unDefNameAgda.TypeChecking.Test.Generators
underAbsAgda.TypeChecking.MetaVars.Occurs
underAbstractionAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
underAbstraction_Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
Underscore 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
underscoreAgda.Syntax.Concrete.Pretty
UndoAgda.Auto.NarrowingSearch
unElAgda.Syntax.Internal
unElimAgda.TypeChecking.Eliminators
unElimViewAgda.TypeChecking.Eliminators
unequalAgda.Auto.Typecheck
UnequalHidingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unequalsAgda.Auto.Typecheck
UnequalSortsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTelescopesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTermsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTypesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unescapeAgda.Compiler.JS.Pretty
unescapesAgda.Compiler.JS.Pretty
UnexpectedWithPatternsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unExprViewAgda.Syntax.Concrete.Operators.Parser
unflattenTelAgda.TypeChecking.Telescope
unfoldAgda.TypeChecking.MetaVars.Occurs
unfoldCorecursionAgda.TypeChecking.CompiledClause.Match
unfoldDefinitionAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
UnfoldStrategyAgda.TypeChecking.MetaVars.Occurs
unfreezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unGraphAgda.Utils.Graph
uniConstrAgda.TypeChecking.Rules.LHS.Unify
UnifiableAgda.TypeChecking.Rules.LHS.Unify
unifiableAgda.Compiler.Epic.Injection
UnificationResultAgda.TypeChecking.Rules.LHS.Unify
UnifiesAgda.TypeChecking.Rules.LHS.Unify
UnifyAgda.TypeChecking.Rules.LHS.Unify
unifyAgda.Compiler.Epic.Injection
UnifyEnvAgda.TypeChecking.Rules.LHS.Unify
UnifyExceptionAgda.TypeChecking.Rules.LHS.Unify
unifyexpAgda.Auto.CaseSplit
unifyIAgda.Compiler.Epic.Forcing
unifyIndicesAgda.TypeChecking.Rules.LHS.Unify
unifyIndices_Agda.TypeChecking.Rules.LHS.Unify
UnifyMayPostponeAgda.TypeChecking.Rules.LHS.Unify
UnifyOutputAgda.TypeChecking.Rules.LHS.Unify
UnifyStateAgda.TypeChecking.Rules.LHS.Unify
UninstantiatedDotPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UninstantiatedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
union 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Graph
3 (Function)Agda.Utils.Trie
4 (Function)Agda.Compiler.JS.Substitution
5 (Function)Agda.Termination.CallGraph
unionConstraintsAgda.Compiler.Epic.Injection
unions 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Graph
unionSignaturesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
unionWithMAgda.Utils.Map
uniqByAgda.Utils.List
uniSubAgda.TypeChecking.Rules.LHS.Unify
UNITAgda.Compiler.Epic.AuxAST
univarAgda.Auto.SearchControl
UnknownAgda.TypeChecking.Positivity
unknownAgda.Termination.CallGraph
UnknownNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
UnknownNamesInFixityDeclAgda.Syntax.Concrete.Definitions
UnknownSortAgda.Auto.Syntax
unlessMAgda.Utils.Monad
unLevelAtomAgda.TypeChecking.Substitute
unlistenToMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unLvlAgda.TypeChecking.Primitive
unnamedAgda.Syntax.Common
unNatAgda.TypeChecking.Primitive
unNoTypeAgda.TypeChecking.Test.Generators
unqhnameAgda.Compiler.MAlonzo.Misc
unqnameAgda.Compiler.Epic.CompileState
unqualifyAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
Unquote 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Type/Class)Agda.TypeChecking.Quote
unquoteAgda.TypeChecking.Quote
unquoteFailedAgda.TypeChecking.Quote
unquoteFailedGenericAgda.TypeChecking.Quote
unquoteHAgda.TypeChecking.Quote
unquoteNAgda.TypeChecking.Quote
UnreachableClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnreducedLevelAgda.Syntax.Internal
unsafeCoerceModAgda.Compiler.MAlonzo.Misc
unsafePragmaOptionsAgda.Interaction.Options
unScopeAgda.TypeChecking.Rules.Term
unSizedListAgda.TypeChecking.Test.Generators
unSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
UnsolvedConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedConstraintsAgda.Interaction.Imports
UnsolvedMetaAgda.Interaction.Highlighting.Precise
UnsolvedMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedMetaVariablesAgda.Interaction.Imports
unStrAgda.TypeChecking.Primitive
unTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unUnifyAgda.TypeChecking.Rules.LHS.Unify
unusableRelevanceAgda.TypeChecking.Irrelevance
UnusedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unVarNameAgda.TypeChecking.Test.Generators
unYesTypeAgda.TypeChecking.Test.Generators
updateMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
updateMetaVarAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateMetaVarRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updatePtrAgda.Utils.Pointer
ureadIORefAgda.Auto.NarrowingSearch
ureadmodifyIORefAgda.Auto.NarrowingSearch
UReduceAgda.TypeChecking.Rules.LHS.Unify
ureduceAgda.TypeChecking.Rules.LHS.Unify
usageAgda.Interaction.Options
usedSeedAgda.Utils.QuickCheck
usedSizeAgda.Utils.QuickCheck
useInjectivityAgda.TypeChecking.Injectivity
UselessAbstractAgda.Syntax.Concrete.Definitions
UselessPrivateAgda.Syntax.Concrete.Definitions
UseLitAgda.TypeChecking.Test.Generators
useLitCharAgda.TypeChecking.Test.Generators
UseLiteralsAgda.TypeChecking.Test.Generators
useLitFloatAgda.TypeChecking.Test.Generators
useLitIntAgda.TypeChecking.Test.Generators
useLitStringAgda.TypeChecking.Test.Generators
useNamesFromPatternAgda.TypeChecking.Rules.LHS
UsesAgda.Compiler.JS.Syntax
usesAgda.Compiler.JS.Syntax
UsingAgda.Syntax.Concrete
UsingOrHidingAgda.Syntax.Concrete
usingOrHidingAgda.Syntax.Concrete
UStAgda.TypeChecking.Rules.LHS.Unify
uwriteIORefAgda.Auto.NarrowingSearch
ValueCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Var 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Internal
3 (Type/Class)Agda.Compiler.Epic.Interface
4 (Data Constructor)Agda.Compiler.Epic.AuxAST
5 (Data Constructor)Agda.Syntax.Abstract
varAgda.TypeChecking.Primitive
VarArgAgda.TypeChecking.Positivity
VarElimAgda.TypeChecking.Eliminators
varFreqAgda.TypeChecking.Test.Generators
VariableIsIrrelevantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
variantAgda.Utils.QuickCheck
VarMPAgda.TypeChecking.Coverage.Match
VarName 
1 (Data Constructor)Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
2 (Type/Class)Agda.TypeChecking.Test.Generators
3 (Data Constructor)Agda.TypeChecking.Test.Generators
VarP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract
VarPattAgda.Compiler.JS.Case
VarsAgda.TypeChecking.MetaVars.Occurs
VarSetAgda.Utils.VarSet
VarShAgda.TypeChecking.Rules.LHS.Unify
varSortAgda.Syntax.Internal
vcat 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
vectorAgda.Utils.QuickCheck
vectorOfAgda.Utils.QuickCheck
verboseAgda.Utils.QuickCheck
verboseBracketAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
verboseCheckAgda.Utils.QuickCheck
verboseCheckResultAgda.Utils.QuickCheck
verboseCheckWithAgda.Utils.QuickCheck
verboseCheckWithResultAgda.Utils.QuickCheck
VerboseKeyAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
verboseSAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
VerbosityAgda.Interaction.Options
versionAgda.Version
vimFileAgda.Interaction.Highlighting.Vim
vineAgda.Compiler.JS.Substitution
visitAgda.Compiler.JS.Case
VisitedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
visitModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
visitorNameAgda.Compiler.JS.Compiler
waitokAgda.Auto.NarrowingSearch
wakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
wakeIrrelevantVarsAgda.TypeChecking.Irrelevance
wakeupConstraintsAgda.TypeChecking.Constraints
wakeupConstraints_Agda.TypeChecking.Constraints
wakeupListenerAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
Warnings 
1 (Type/Class)Agda.Interaction.Imports
2 (Data Constructor)Agda.Interaction.Imports
warningsToErrorAgda.Interaction.Imports
warshallAgda.Utils.Warshall
warshallGAgda.Utils.Warshall
WeakAgda.Auto.Syntax
weakAgda.Auto.Syntax
weakarglistAgda.Auto.Syntax
weakelrAgda.Auto.Syntax
weakenAgda.Auto.Convert
weakensAgda.Auto.Convert
weakiAgda.Auto.Syntax
weaklyAgda.TypeChecking.MetaVars.Occurs
WeaklyRigidAgda.TypeChecking.Free
weaklyRigidVarsAgda.TypeChecking.Free
WeightAgda.Utils.Warshall
wellFormedIndicesAgda.TypeChecking.Rules.LHS.Split
whatInductionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
whenConstraintsAgda.TypeChecking.Constraints
whenFailAgda.Utils.QuickCheck
whenFail'Agda.Utils.QuickCheck
whenMAgda.Utils.Monad
WhereClauseAgda.Syntax.Concrete
WildMPAgda.TypeChecking.Coverage.Match
WildP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
WildVAgda.Syntax.Concrete.Operators.Parser
withAnonymousModuleAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
WithApp 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
withAppBracketsAgda.Syntax.Fixity
WithArgCtxAgda.Syntax.Fixity
withArgsFromAgda.Syntax.Common
WithClausePatternMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
withConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
withContextPrecedenceAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
withCurrentModule 
1 (Function)Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
2 (Function)Agda.Syntax.Scope.Monad
withCurrentModule'Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
withDisplayFormAgda.TypeChecking.With
withEnvAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
withFreshAgda.Utils.Fresh
WithFunctionAgda.TypeChecking.Rules.Def
WithFunctionProblemAgda.TypeChecking.Rules.Def
withFunctionTypeAgda.TypeChecking.With
WithFunCtxAgda.Syntax.Fixity
withImportPathAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
withinAgda.Utils.QuickCheck
withInteractionIdAgda.Interaction.BasicOps
withIntervalAgda.Syntax.Parser.LexActions
withInterval'Agda.Syntax.Parser.LexActions
withInterval_Agda.Syntax.Parser.LexActions
withLayoutAgda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout
withLocalVarsAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
withMetaIdAgda.Interaction.BasicOps
withMetaInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
withRangeOfAgda.Syntax.Position, Agda.Interaction.GhciTop
withRangesOfAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
withRangesOfQAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
WithRHSAgda.Syntax.Abstract
withScope 
1 (Function)Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
2 (Function)Agda.Syntax.Translation.AbstractToConcrete
withScope_Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
withSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
withTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
wordBoundaryAgda.Compiler.JS.Parser
wordsByAgda.Utils.List
workOnTypesAgda.TypeChecking.Irrelevance
workOnTypes'Agda.TypeChecking.Irrelevance
writeFileAgda.Utils.IO.UTF8
writeInterfaceAgda.Interaction.Imports
writeModule 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
WrongHidingInApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongHidingInLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongHidingInLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongIrrelevanceInLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WrongNumberOfConstructorArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
WSMAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
xForPrimAgda.Compiler.MAlonzo.Primitives
xhqnAgda.Compiler.MAlonzo.Misc
xqualAgda.Compiler.MAlonzo.Misc
Yes 
1 (Data Constructor)Agda.TypeChecking.Coverage.Match
2 (Data Constructor)Agda.TypeChecking.Patterns.Match
yesMatchLitAgda.TypeChecking.Coverage.Match
YesReductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
YesType 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
YesUnfoldAgda.TypeChecking.MetaVars.Occurs
zeroAgda.Termination.Semiring
zeroElementAgda.Termination.Semiring
zeroNameAgda.TypeChecking.Level
zeroWidthTextAgda.Utils.Pretty
ZigZagModeAgda.Utils.Pretty
zipNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
zipScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
zipScope_Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
zipWithAgda.Termination.Matrix
zipWith'Agda.Utils.List
zipWithM'Agda.Utils.Monad
|->Agda.TypeChecking.Rules.LHS.Unify
||-Agda.Compiler.Epic.Erasure