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

Index

!Agda.Utils.HashMap
!!! 
1 (Function)Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
2 (Function)Agda.Compiler.Epic.Injection
$$ 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
$$$Agda.Syntax.Concrete.Operators.Parser
$+$ 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
&&-Agda.Compiler.Epic.Erasure
++#Agda.TypeChecking.Substitute
+++ 
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
.-->Agda.TypeChecking.Primitive
.||. 
1 (Function)Agda.Utils.QuickCheck
2 (Function)Agda.Syntax.Parser.Alex
/\ 
1 (Function)Agda.Utils.Tuple
2 (Function)Agda.TypeChecking.Polarity
:#Agda.TypeChecking.Substitute
:->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.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
AbsNameAgda.Syntax.Scope.Base
absNameAgda.Syntax.Internal
absoluteAgda.Utils.FileName
AbsolutePathAgda.Utils.FileName
abspatvarnameAgda.Auto.CaseSplit
AbsToConAgda.Syntax.Translation.AbstractToConcrete
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
AbstractNameAgda.Syntax.Scope.Base
AbstractRHSAgda.Syntax.Translation.ConcreteToAbstract
AbstractTermAgda.TypeChecking.Abstract
abstractTermAgda.TypeChecking.Abstract
abstractToConcreteAgda.Syntax.Translation.AbstractToConcrete
abstractToConcreteCtxAgda.Syntax.Translation.AbstractToConcrete
abstractToConcrete_Agda.Syntax.Translation.AbstractToConcrete
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
acyclicAgda.Utils.Graph
add 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.Matrix
3 (Function)Agda.Termination.SparseMatrix
addAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
addblkAgda.Auto.Typecheck
addColumn 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
addConnectionAgda.Interaction.Highlighting.Dot
addConstantAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addConstraint 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.TypeChecking.Constraints
3 (Function)Agda.Compiler.Epic.Injection
addConstraint'Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
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
addCtxString_Agda.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
addNamesToScopeAgda.Syntax.Scope.Base
addNameToScopeAgda.Syntax.Scope.Base
addNodeAgda.Utils.Warshall
addRow 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
addSectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addSuffixAgda.Utils.Suffix
addtrailingargsAgda.Auto.Syntax
ADefAgda.TypeChecking.Positivity
AdjListAgda.Utils.Warshall
adjustAgda.Utils.HashMap
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
allKindsOfNamesAgda.Syntax.Scope.Base
allMetaKindsAgda.TypeChecking.MetaVars
allMetasAgda.TypeChecking.MetaVars
allNamesAgda.Syntax.Abstract
allNamesInScopeAgda.Syntax.Scope.Base
allNamesInScope'Agda.Syntax.Scope.Base
allowedVarAgda.TypeChecking.MetaVars.Occurs
allPathsAgda.Utils.Graph
allRightAgda.Utils.Either
allThingsInScopeAgda.Syntax.Scope.Base
allVarsAgda.TypeChecking.Free
ALNilAgda.Auto.Syntax
ALProjAgda.Auto.Syntax
alreadyVisitedAgda.Interaction.Imports
altM1Agda.Utils.Monad
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
AmbiguousTopLevelModuleNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
amodNameAgda.Syntax.Scope.Base
anameKindAgda.Syntax.Scope.Base
anameNameAgda.Syntax.Scope.Base
AnArgAgda.TypeChecking.Positivity
AndAgda.Auto.NarrowingSearch
and2MAgda.Utils.Monad
andMAgda.Utils.Monad
AnyAbstractAgda.Syntax.Abstract
anyAbstractAgda.Syntax.Abstract
AnyWhereAgda.Syntax.Concrete
APatNameAgda.Syntax.Translation.ConcreteToAbstract
App 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Compiler.Epic.AuxAST
4 (Data Constructor)Agda.Syntax.Abstract
5 (Data Constructor)Agda.TypeChecking.EtaContract
appAgda.Syntax.Abstract
appBracketsAgda.Syntax.Fixity
appDefAgda.TypeChecking.Reduce
appDef'Agda.TypeChecking.Reduce
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
applyDroppingParametersAgda.TypeChecking.InstanceArguments
ApplyHHAgda.TypeChecking.Rules.LHS.Unify
applyHHAgda.TypeChecking.Rules.LHS.Unify
applyImportDirectiveAgda.Syntax.Scope.Base
applyImportDirectiveMAgda.Syntax.Scope.Monad
applypermAgda.Auto.CaseSplit
applyRelevanceAgda.TypeChecking.Irrelevance
applyRelevanceToContextAgda.TypeChecking.Irrelevance
applySectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
applySubstAgda.TypeChecking.Substitute
AppPAgda.Syntax.Concrete
appPAgda.Syntax.Concrete.Operators.Parser
appsAgda.Compiler.Epic.AuxAST
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
apTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ArbitraryAgda.Utils.QuickCheck
arbitraryAgda.Utils.QuickCheck
arbitraryBoundedEnumAgda.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
argFromDomAgda.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
arity 
1 (Function)Agda.Syntax.Internal
2 (Function)Agda.TypeChecking.CompiledClause
arrowAgda.Syntax.Concrete.Pretty
AsAgda.Syntax.Concrete
AsBAgda.TypeChecking.Rules.LHS.Problem
AsBindingAgda.TypeChecking.Rules.LHS.Problem
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
assignConstrTagAgda.Compiler.Epic.CompileState
assignConstrTag'Agda.Compiler.Epic.CompileState
assignTermAgda.TypeChecking.MetaVars
assignTerm'Agda.TypeChecking.MetaVars
assignVAgda.TypeChecking.MetaVars
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.InteractionTop
backupPosAgda.Syntax.Position
BadImplicitsAgda.TypeChecking.Implicit
beginAgda.Syntax.Parser.LexActions
beginningOfAgda.Syntax.Position
beginningOfFileAgda.Syntax.Position
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
bindNameAgda.Syntax.Scope.Monad
bindParametersAgda.TypeChecking.Rules.Data
bindPostulatedNameAgda.TypeChecking.Rules.Builtin
bindPrimitiveAgda.TypeChecking.Monad.Builtin
bindQModuleAgda.Syntax.Scope.Monad
bindTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
bindToConcreteAgda.Syntax.Translation.AbstractToConcrete
bindVariableAgda.Syntax.Scope.Monad
BinOpAgda.Compiler.JS.Syntax
binop 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Concrete.Operators.Parser
blendInAbsurdClauseAgda.TypeChecking.Coverage
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
BlockingVarAgda.TypeChecking.Coverage.Match
BlockingVarsAgda.TypeChecking.Coverage.Match
blockOfLinesAgda.Syntax.Scope.Base
blockTermAgda.TypeChecking.MetaVars
blockTermOnProblemAgda.TypeChecking.MetaVars
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
BoundedLtAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
BoundedNoAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
BoundedSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
boundedSizeMetaHookAgda.TypeChecking.SizedTypes
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
bracket_Agda.Utils.Monad
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
buildParserAgda.Syntax.Concrete.Operators
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
builtinIrrAxiomAgda.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
builtinSizeHookAgda.TypeChecking.SizedTypes
builtinSizeInfAgda.TypeChecking.Monad.Builtin
builtinSizeLtAgda.TypeChecking.Monad.Builtin
builtinSizeMaxAgda.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.Termination.CallGraph
2 (Data Constructor)Agda.Termination.CallGraph
3 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callCompilerAgda.Compiler.CallCompiler
callCompiler'Agda.Compiler.CallCompiler
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
canonicalizeSizeConstraintAgda.TypeChecking.SizedTypes
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
checkAliasAgda.TypeChecking.Rules.Def
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
checkCandidatesAgda.TypeChecking.InstanceArguments
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
checkDeclsAgda.TypeChecking.Rules.Decl, Agda.TypeChecker
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
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
checkLinearityAgda.TypeChecking.MetaVars
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
clauseLHSAgda.Syntax.Abstract
clausePatsAgda.Syntax.Internal
clausePermAgda.Syntax.Internal
clauseRangeAgda.Syntax.Internal
clauseRHSAgda.Syntax.Abstract
clauseTelAgda.Syntax.Internal
clauseToSplitClauseAgda.TypeChecking.Coverage
clauseWhereDeclsAgda.Syntax.Abstract
clearMetaListenersAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
clearRunningInfoAgda.Interaction.EmacsCommand
clEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClockTimeAgda.Utils.Time
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.InteractionTop
Cmd_compileAgda.Interaction.InteractionTop
Cmd_computeAgda.Interaction.InteractionTop
Cmd_compute_toplevelAgda.Interaction.InteractionTop
Cmd_constraintsAgda.Interaction.InteractionTop
Cmd_contextAgda.Interaction.InteractionTop
Cmd_giveAgda.Interaction.InteractionTop
Cmd_goal_typeAgda.Interaction.InteractionTop
Cmd_goal_type_contextAgda.Interaction.InteractionTop
cmd_goal_type_context_andAgda.Interaction.InteractionTop
Cmd_goal_type_context_inferAgda.Interaction.InteractionTop
Cmd_inferAgda.Interaction.InteractionTop
Cmd_infer_toplevelAgda.Interaction.InteractionTop
Cmd_introAgda.Interaction.InteractionTop
Cmd_loadAgda.Interaction.InteractionTop
cmd_load'Agda.Interaction.InteractionTop
Cmd_load_highlighting_infoAgda.Interaction.InteractionTop
Cmd_make_caseAgda.Interaction.InteractionTop
Cmd_metasAgda.Interaction.InteractionTop
Cmd_refineAgda.Interaction.InteractionTop
Cmd_refine_or_introAgda.Interaction.InteractionTop
Cmd_show_module_contentsAgda.Interaction.InteractionTop
Cmd_show_module_contents_toplevelAgda.Interaction.InteractionTop
Cmd_solveAllAgda.Interaction.InteractionTop
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
CName 
1 (Type/Class)Agda.TypeChecking.Coverage.SplitTree
2 (Data Constructor)Agda.TypeChecking.Coverage.SplitTree
cnvhAgda.Auto.Convert
CoArbitraryAgda.Utils.QuickCheck
coarbitraryAgda.Utils.QuickCheck
coarbitraryEnumAgda.Utils.QuickCheck
coarbitraryIntegralAgda.Utils.QuickCheck
coarbitraryRealAgda.Utils.QuickCheck
coarbitraryShowAgda.Utils.QuickCheck
CodataAgda.Syntax.Concrete.Definitions
codeAgda.Syntax.Parser.Lexer
coerceAgda.TypeChecking.Conversion
CoinductionKit 
1 (Type/Class)Agda.TypeChecking.Monad.Builtin
2 (Data Constructor)Agda.TypeChecking.Monad.Builtin
coinductionKitAgda.TypeChecking.Monad.Builtin
CoInductiveAgda.Syntax.Common
CoinductiveDatatypeAgda.TypeChecking.Coverage
col 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
coldescrAgda.Utils.Warshall
collectAgda.Utils.QuickCheck
colon 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
cols 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
ColumnAgda.Termination.Lexicographic
columnsAgda.Termination.Lexicographic
comma 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
CommandAgda.Interaction.CommandLine.CommandLine
CommandLineOptionsAgda.Interaction.Options
commandLineOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
CommandM 
1 (Type/Class)Agda.Interaction.InteractionTop
2 (Data Constructor)Agda.Interaction.InteractionTop
commandMToIOAgda.Interaction.InteractionTop
CommandState 
1 (Type/Class)Agda.Interaction.InteractionTop
2 (Data Constructor)Agda.Interaction.InteractionTop
Comment 
1 (Data Constructor)Agda.Interaction.Highlighting.Precise
2 (Type/Class)Agda.Compiler.Epic.AuxAST
commutativeAgda.Utils.TestHelpers
comp'Agda.Auto.Typecheck
compactPAgda.Utils.Permutation
compareArgsAgda.TypeChecking.Conversion
compareAtomAgda.TypeChecking.Conversion
compareBelowMaxAgda.TypeChecking.SizedTypes
compareElimsAgda.TypeChecking.Conversion
compareIrrelevantAgda.TypeChecking.Conversion
compareLevelAgda.TypeChecking.UniversePolymorphism
compareMaxViewsAgda.TypeChecking.SizedTypes
compareRelevanceAgda.TypeChecking.Conversion
compareSizesAgda.TypeChecking.SizedTypes
compareSizeViewsAgda.TypeChecking.SizedTypes
compareSortAgda.TypeChecking.Conversion
compareTelAgda.TypeChecking.Conversion
compareTermAgda.TypeChecking.Conversion
compareTerm'Agda.TypeChecking.Conversion
compareTypeAgda.TypeChecking.Conversion
compareWithPolAgda.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
compileWithSplitTreeAgda.TypeChecking.CompiledClause.Compile
completeAgda.Termination.CallGraph
composePAgda.Utils.Permutation
composePolAgda.TypeChecking.Polarity
composeRelevanceAgda.TypeChecking.Irrelevance
composeSAgda.TypeChecking.Substitute
compressAgda.Interaction.Highlighting.Precise
CompressedFile 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
compressedFileInvariantAgda.Interaction.Highlighting.Precise
compressPointerChainAgda.Syntax.Internal
computeEdgeAgda.TypeChecking.Positivity
computeNeighbourhoodAgda.TypeChecking.Coverage
ComputeOccurrencesAgda.TypeChecking.Positivity
computeOccurrencesAgda.TypeChecking.Positivity
computePolarityAgda.TypeChecking.Polarity
computeSizeConstraintAgda.TypeChecking.SizedTypes
computeSizeConstraintsAgda.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
concatOccursAgda.TypeChecking.Positivity
ConcreteDefAgda.Syntax.Common
ConcreteModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
concreteToAbstractAgda.Syntax.Translation.ConcreteToAbstract
concreteToAbstract_Agda.Syntax.Translation.ConcreteToAbstract
conDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
condeclAgda.Compiler.MAlonzo.Compiler
ConditionAgda.TypeChecking.MetaVars
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
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.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constraintProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Constraints 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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 (Data Constructor)Agda.Interaction.Highlighting.Precise
4 (Type/Class)Agda.Syntax.Abstract
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
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
contentAgda.TypeChecking.CompiledClause
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
continuousPerLineAgda.Syntax.Position
ContravariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
convErrorAgda.TypeChecking.Conversion
convertLineEndingsAgda.Utils.Unicode
copyargAgda.Auto.Typecheck
copyScopeAgda.Syntax.Scope.Monad
copyTermAgda.Syntax.Internal.Generic
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
coverageCheckAgda.TypeChecking.Coverage
CoverageFailureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Covering 
1 (Type/Class)Agda.TypeChecking.Coverage
2 (Data Constructor)Agda.TypeChecking.Coverage
CoverMAgda.TypeChecking.Coverage
covSplitArgAgda.TypeChecking.Coverage
covSplitClausesAgda.TypeChecking.Coverage
createInterfaceAgda.Interaction.Imports
createMetaInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
createMetaInfo'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
createModuleAgda.Syntax.Scope.Monad
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
currentOrFreshMutualBlockAgda.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
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
dataIxsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataMustEndInSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataOrRecordAgda.TypeChecking.Datatypes
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
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
dbIndexToLevelAgda.TypeChecking.Coverage
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
dealAgda.Utils.List
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
decreaseAgda.Termination.CallGraph
decreasingAgda.Termination.CallGraph
DeepSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
deepSizeViewAgda.TypeChecking.SizedTypes
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
defArgOccurrencesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
defaultInteractionOptionsAgda.Interaction.Options
defaultInteractionOutputCallbackAgda.Interaction.Response
defaultNamedArgAgda.Syntax.Common
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
defCopyAgda.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
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
defIsDataOrRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
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
defNeedsCheckingAgda.TypeChecking.MetaVars.Occurs
DefNodeAgda.TypeChecking.Positivity
defnParsAgda.Compiler.Epic.Smashing
defOrVarAgda.TypeChecking.Rules.Term
DefPAgda.Syntax.Abstract
defPolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
delete 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.HashMap
dependentPolarityAgda.TypeChecking.Polarity
depthofvarAgda.Auto.CaseSplit
derefPtrAgda.Utils.Pointer, Agda.Syntax.Internal
detecteliminandAgda.Auto.Syntax
detectsemiflexAgda.Auto.Syntax
diagonal 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
diffAgda.Compiler.Epic.Erasure
differenceAgda.Utils.HashMap
DifferentAritiesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DirectAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
disableDestructiveUpdateAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
disableDisplayFormsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
discardAgda.Utils.QuickCheck
disjoinAgda.Utils.QuickCheck
DisplayAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayDebugMessageAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayFormAgda.TypeChecking.DisplayForm
displayFormsEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DisplayInfoAgda.Interaction.Response
displayRunningInfoAgda.Interaction.EmacsCommand
displayStatusAgda.Interaction.InteractionTop
DisplayTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
display_infoAgda.Interaction.InteractionTop
display_info'Agda.Interaction.EmacsCommand
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
doesFileExistCaseSensitiveAgda.Utils.FileName
DoesNotConstructAnElementOfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
doEtaContractImplicitAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Dom 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
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
domFromArgAgda.Syntax.Common
domHAgda.TypeChecking.Primitive
domHidingAgda.Syntax.Common
domNAgda.TypeChecking.Primitive
domRelevanceAgda.Syntax.Common
DoneAgda.TypeChecking.CompiledClause
dontAssignMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
DontCare 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Abstract
dontCareAgda.Auto.Syntax
dontDescendIntoAgda.Utils.Geniplate
dontEtaContractImplicitAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontExpandInstanceArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DontExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
DontRunMetaOccursCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DontTouchMeAgda.Syntax.Translation.AbstractToConcrete
DontUseBoundNamesAgda.Syntax.Concrete.Operators
DoOpenAgda.Syntax.Concrete
DotAgda.Syntax.Concrete
DOtherSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
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.Problem
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
DoubleAgda.Compiler.JS.Syntax
doubleAgda.Utils.Pretty
doubleblockAgda.Auto.NarrowingSearch
doubleQuotesAgda.Utils.Pretty
downFromAgda.Utils.List
doWorkOnTypesAgda.TypeChecking.Irrelevance
DPIAgda.TypeChecking.Rules.LHS.Problem
DropArgsAgda.TypeChecking.DropArgs
dropArgsAgda.TypeChecking.DropArgs
dropConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
dropDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
drophidAgda.Auto.CaseSplit
dropIAgda.Syntax.Position
dropNonHiddenAgda.TypeChecking.Rules.Def
dropSAgda.TypeChecking.Substitute
dryInstantiateAgda.Auto.NarrowingSearch
dsConnectionAgda.Interaction.Highlighting.Dot
DSizeInfAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
DSizeMetaAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
DSizeVarAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
dsModulesAgda.Interaction.Highlighting.Dot
dsNameSupplyAgda.Interaction.Highlighting.Dot
dsubnameAgda.Compiler.MAlonzo.Misc
DTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dummyAgda.Compiler.MAlonzo.Misc
dummyDomAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
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
edgeInAgda.Utils.Graph
edges 
1 (Function)Agda.Utils.Graph
2 (Function)Agda.Utils.Warshall
edgesFromAgda.Utils.Graph
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
elementsUnlessEmptyAgda.Utils.TestHelpers
elemsAgda.Utils.HashMap
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
emacsifyDebugMessageAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
emapAgda.TypeChecking.Records
EmbPrjAgda.TypeChecking.Serialise
empAgda.Compiler.JS.Substitution
empty 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Pretty
3 (Function)Agda.Utils.HashMap
4 (Function)Agda.Utils.Trie
5 (Function)Agda.Termination.CallGraph
6 (Function)Agda.Utils.Graph
7 (Function)Agda.Interaction.Highlighting.Range
8 (Function)Agda.TypeChecking.Pretty
emptyBranchesAgda.TypeChecking.CompiledClause
emptyCAgda.Compiler.Epic.Injection
emptyConstraintsAgda.Utils.Warshall
emptyLayoutAgda.Syntax.Parser.Layout
emptyMetaInfoAgda.Syntax.Info
emptyNameSpaceAgda.Syntax.Scope.Base
EmptySAgda.TypeChecking.Substitute
emptyScopeAgda.Syntax.Scope.Base
emptyScopeInfoAgda.Syntax.Scope.Base
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
enablePhantomTypesAgda.TypeChecking.Polarity
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
enterClosureAgda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad
EnvAgda.Syntax.Translation.AbstractToConcrete
envAbstractModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envActiveProblemsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAllowDestructiveUpdateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAnonymousModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAssignMetasAgda.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
envCurrentPathAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envDisplayFormsEnabledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envEmacsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envEtaContractImplicitAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envHighlightingLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envHighlightingMethodAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envHighlightingRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envImportPathAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envLetBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envModuleNestingLevelAgda.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
eofAgda.Syntax.Parser.LexActions
EpicAgda.Interaction.InteractionTop
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
equals 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.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
errInputAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errMsgAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
Error 
1 (Data Constructor)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
errPosAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errPrevTokenAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
escapeAgda.Interaction.Highlighting.Vim
escapeContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
escapeContextToTopLevelAgda.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
etaExpandClauseAgda.TypeChecking.Positivity
etaExpandListenersAgda.TypeChecking.MetaVars
etaExpandMetaAgda.TypeChecking.MetaVars
etaExpandMetaSafeAgda.TypeChecking.MetaVars
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
everythingInScopeAgda.Syntax.Scope.Base
exactAgda.Interaction.InteractionTop
ExceptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExceptionT 
1 (Type/Class)Agda.TypeChecking.Monad.Exception
2 (Data Constructor)Agda.TypeChecking.Monad.Exception
exhaustiveAgda.Utils.QuickCheck
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.Monad.Base, Agda.TypeChecking.Monad
ExpandInstanceArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExpandInstancesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
expandLitPatternAgda.TypeChecking.Rules.LHS.Split
expandPAgda.Utils.Permutation
expectFailureAgda.Utils.QuickCheck
explicitForAllAgda.Compiler.MAlonzo.Compiler
expNameAgda.Compiler.JS.Syntax
Export 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
exportedNamesInScopeAgda.Syntax.Scope.Base
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
exprParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser
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
extractblkinfosAgda.Auto.NarrowingSearch
extractNthElementAgda.Utils.List
extractNthElement'Agda.Utils.List
extrarefAgda.Auto.SearchControl
FailAgda.TypeChecking.CompiledClause
FailedAgda.Auto.NarrowingSearch
failOnExceptionAgda.Interaction.Exceptions
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 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Abstract
fieldAgda.Compiler.JS.Parser
FieldNameAgda.Syntax.Scope.Monad
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
filterAgda.Utils.HashMap
filterEdgesAgda.Utils.Graph
filterKeysAgda.Utils.Map
filterScopeAgda.Syntax.Scope.Base
filterWithKeyAgda.Utils.HashMap
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
findInjectionAgda.Compiler.Epic.Injection
FindInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
findInScopeAgda.TypeChecking.InstanceArguments
findInScope'Agda.TypeChecking.InstanceArguments
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
fIntAgda.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
flattenScopeAgda.Syntax.Scope.Base
flattenSubstitutionAgda.TypeChecking.Rules.LHS.Unify
flattenTelAgda.TypeChecking.Telescope
FldNameAgda.Syntax.Scope.Base
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
fmapTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.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
foldl'Agda.Utils.HashMap
foldlWithKey'Agda.Utils.HashMap
foldrAgda.Utils.HashMap
foldrWithKeyAgda.Utils.HashMap
foldTermAgda.Syntax.Internal.Generic
followedByAgda.Syntax.Parser.LexActions
forAllAgda.Utils.QuickCheck
forAllShrinkAgda.Utils.QuickCheck
forceAgda.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
forcedExprAgda.Compiler.Epic.Forcing
forcedVariablesAgda.TypeChecking.Forcing
forceEqualTermsAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
forceFunAgda.Compiler.Epic.ForceConstrs
forceHomAgda.TypeChecking.Rules.LHS.Unify
forkTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
forM'Agda.Utils.Monad
fProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
FreeAgda.TypeChecking.Free
freeIn 
1 (Function)Agda.TypeChecking.Free
2 (Function)Agda.Auto.Convert
freeInIgnoringSortAnnAgda.TypeChecking.Free
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
freshAbstractName_Agda.Syntax.Scope.Monad
freshAbstractQNameAgda.Syntax.Scope.Monad
freshNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
freshName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
freshNoNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
freshNoName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
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.Matrix
2 (Function)Agda.Termination.SparseMatrix
fromJustAgda.Utils.Maybe
fromList 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.HashMap
3 (Function)Agda.Termination.CallGraph
4 (Function)Agda.Utils.Graph
fromLists 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
fromListWithAgda.Utils.HashMap
fromLiteralAgda.TypeChecking.Primitive
fromMaybeAgda.Utils.Maybe
fromMaybeMAgda.Utils.Maybe
frommyAgda.Auto.Convert
frommyClauseAgda.Auto.Convert
frommyExpAgda.Auto.Convert
frommyExpsAgda.Auto.Convert
frommyTypeAgda.Auto.Convert
fromNodesAgda.Utils.Graph
fromOrdinaryAgda.Syntax.Concrete
fromReducedTermAgda.TypeChecking.Primitive
fromSubscriptDigitAgda.Utils.Suffix
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
fst3Agda.Utils.Tuple
FullAgda.Interaction.Highlighting.Generate
fullParenAgda.Syntax.Concrete.Operators
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
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
funCopyAgda.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
FunctionInverse'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
funMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
funNameAgda.Compiler.Epic.AuxAST
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
funTerminatesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
fuseRangeAgda.Syntax.Position
fuseRangesAgda.Syntax.Position
FVAgda.TypeChecking.Free
fvAgda.Compiler.Epic.AuxAST
FVsAgda.TypeChecking.MetaVars
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
generateAndPrintSyntaxInfoAgda.Interaction.Highlighting.Generate
generateDotAgda.Interaction.Highlighting.Dot
generateHTMLAgda.Interaction.Highlighting.HTML
generateLaTeXAgda.Interaction.Highlighting.LaTeX
generateTokenInfoAgda.Interaction.Highlighting.Generate
generateVimFileAgda.Interaction.Highlighting.Vim
GenericDocErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
genericElemIndexAgda.Utils.List
GenericErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
GenericSplitErrorAgda.TypeChecking.Coverage
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
getArgOccurrencesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
getblksAgda.Auto.CaseSplit
getBrVarsAgda.Compiler.Epic.AuxAST
getBuiltinAgda.TypeChecking.Monad.Builtin
getBuiltin'Agda.TypeChecking.Monad.Builtin
getBuiltinDefNameAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
getBuiltinsAgda.Compiler.Epic.Primitive
getBuiltinSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
getBuiltinThingAgda.TypeChecking.Monad.Builtin
getClockTimeAgda.Utils.Time
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
getConstructorArityAgda.TypeChecking.Datatypes
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
getContextSizeAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextTelescopeAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextTermsAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getCurrentModuleAgda.Syntax.Scope.Monad
getCurrentRangeAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
getCurrentScopeAgda.Syntax.Scope.Monad
getDataConAgda.Compiler.Epic.CompileState
getDatatypeAgda.Auto.Typecheck
getDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getDecodedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getDefArityAgda.TypeChecking.Positivity
getDefFreeVarsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getDefinedNamesAgda.Syntax.Concrete.Operators
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
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
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
getMetaNameSuggestionAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaPriorityAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaSigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaStoreAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaTypeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaTypeInContextAgda.TypeChecking.InstanceArguments
getModuleFreeVarsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getMutualAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getMutualBlocksAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
getNamedScopeAgda.Syntax.Scope.Monad
getNArgsAgda.Auto.Typecheck
getNatishAgda.Compiler.Epic.NatDetection
getNonEmptyAgda.Utils.QuickCheck
getNonNegativeAgda.Utils.QuickCheck
getNonZeroAgda.Utils.QuickCheck
getNumberOfParametersAgda.TypeChecking.Datatypes
getOccurrencesAgda.TypeChecking.Positivity
getOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
getOpenMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getOrderedAgda.Utils.QuickCheck
getParseFlagsAgda.Syntax.Parser.Monad
getParseIntervalAgda.Syntax.Parser.Monad
getPatternSynImportsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getPatternSynsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getPolarityAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getPolarity'Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getPositiveAgda.Utils.QuickCheck
getPrimitiveAgda.TypeChecking.Monad.Builtin
getRangeAgda.Syntax.Position
getRecordConstructorAgda.TypeChecking.Records
getRecordConstructorTypeAgda.TypeChecking.Records
getRecordDefAgda.TypeChecking.Records
getRecordFieldNamesAgda.TypeChecking.Records
getRecordFieldTypesAgda.TypeChecking.Records
getRecordTypeFieldsAgda.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
GiveResultAgda.Interaction.Response
give_genAgda.Interaction.InteractionTop
give_gen'Agda.Interaction.InteractionTop
Give_NoParenAgda.Interaction.Response
Give_ParenAgda.Interaction.Response
Give_StringAgda.Interaction.Response
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
GoalCommandAgda.Interaction.InteractionTop
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
growingElementsAgda.Utils.QuickCheck
GuardAgda.Interaction.BasicOps
guardConstraintAgda.TypeChecking.Constraints
GuardedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
GuardPosAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
handleParseExceptionAgda.Interaction.Exceptions
HandleSolAgda.Auto.NarrowingSearch
hangAgda.Utils.Pretty
hasBadRigidAgda.TypeChecking.MetaVars.Occurs
hasCompiledDataAgda.Compiler.MAlonzo.Primitives
HasFreshAgda.Utils.Fresh
hashAgda.Utils.Hash
HashMapAgda.Utils.HashMap
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
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
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
highlightAsTypeCheckedAgda.Interaction.Highlighting.Generate
highlightFromInterfaceAgda.Interaction.Imports
HighlightingInfoAgda.Interaction.Highlighting.Precise
HighlightingLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
HighlightingMethodAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
IdSAgda.TypeChecking.Substitute
idSAgda.TypeChecking.Substitute
iEndAgda.Syntax.Position
If 
1 (Data Constructor)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.Epic.AuxAST
ifBlockAgda.Compiler.JS.Parser
ifBlockedAgda.TypeChecking.Reduce
ifBlockedTypeAgda.TypeChecking.Reduce
ifCleanAgda.TypeChecking.Rules.LHS.Unify
ifMAgda.Utils.Monad
ifNoConstraintsAgda.TypeChecking.Constraints
ifNoConstraints_Agda.TypeChecking.Constraints
IFSNoCandidateInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ifTopLevelAndHighlightingLevelIsAgda.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
ignoreSharingAgda.Syntax.Internal
ignoreSharingTypeAgda.Syntax.Internal
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
implicitArgsAgda.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
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
increaseAgda.Termination.CallGraph
IndArgTypeAgda.TypeChecking.Positivity
InDefOfAgda.TypeChecking.Positivity
indentAgda.Utils.String
independentAgda.Interaction.InteractionTop
Index 
1 (Data Constructor)Agda.Utils.Suffix
2 (Type/Class)Agda.Termination.CallGraph
IndexVariablesNotDistinctAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndicesFreeInParametersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndicesNotConstructorApplicationsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndirectAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InductionAgda.Syntax.Common
InductiveAgda.Syntax.Common
InfAgda.Syntax.Internal
infAgda.TypeChecking.Positivity
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
inferExprForWithAgda.TypeChecking.Rules.Term
inferHeadAgda.TypeChecking.Rules.Term
inferMetaAgda.TypeChecking.Rules.Term
inferOrCheckAgda.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
Info_AllGoalsAgda.Interaction.Response
Info_AutoAgda.Interaction.Response
Info_CompilationOkAgda.Interaction.Response
Info_ConstraintsAgda.Interaction.Response
Info_ContextAgda.Interaction.Response
Info_CurrentGoalAgda.Interaction.Response
Info_ErrorAgda.Interaction.Response
Info_GoalTypeAgda.Interaction.Response
Info_InferredTypeAgda.Interaction.Response
Info_IntroAgda.Interaction.Response
Info_ModuleContentsAgda.Interaction.Response
Info_NormalFormAgda.Interaction.Response
initCommandStateAgda.Interaction.InteractionTop
initCompileStateAgda.Compiler.Epic.CompileState
initEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initGraphAgda.Utils.Warshall
initialDotStateAgda.Interaction.Highlighting.Dot
initialIFSCandidatesAgda.TypeChecking.InstanceArguments
initializeIFSMetaAgda.TypeChecking.InstanceArguments
initialPrimsAgda.Compiler.Epic.Primitive
initialRelsAgda.Compiler.Epic.Erasure
initialTagsAgda.Compiler.Epic.Injection
initiateAgda.Compiler.Epic.Erasure
initMapSAgda.Auto.Convert
initMetaAgda.Auto.NarrowingSearch
initOccursCheckAgda.TypeChecking.MetaVars.Occurs
initState 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
InScopeAgda.Syntax.Scope.Base
InScopeTagAgda.Syntax.Scope.Base
inScopeTagAgda.Syntax.Scope.Base
insert 
1 (Function)Agda.Utils.HashMap
2 (Function)Agda.Utils.Trie
3 (Function)Agda.Termination.CallGraph
4 (Function)Agda.Utils.Graph
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
insertWithAgda.Utils.HashMap
insertWithKeyMAgda.Utils.Map
InsideOperandCtxAgda.Syntax.Fixity
insideScopeAgda.Syntax.Translation.ConcreteToAbstract
Instance 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Common
InstanceArgAgda.Syntax.Concrete
InstanceArgVAgda.Syntax.Concrete.Operators.Parser
InstancePAgda.Syntax.Concrete
instanceTransformBiMT'Agda.Utils.Geniplate
instanceUniverseBiT'Agda.Utils.Geniplate
InstantiableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstantiateAgda.TypeChecking.Reduce
instantiateAgda.TypeChecking.Reduce
InstantiatedAgda.Interaction.BasicOps
instantiateDefAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
InstantiateFullAgda.TypeChecking.Reduce
instantiateFullAgda.TypeChecking.Reduce
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
InteractionAgda.Interaction.InteractionTop
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
InteractionOutputCallbackAgda.Interaction.Response
InteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InteractiveAgda.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
interpretAgda.Interaction.InteractionTop
interruptedAgda.Utils.QuickCheck
intersectionAgda.Utils.HashMap
intersectionWithAgda.Utils.HashMap
intersectVarsAgda.TypeChecking.Conversion
intersectWithAgda.Termination.SparseMatrix
Interval 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
Interval'Agda.Syntax.Position
intervalInvariantAgda.Syntax.Position
intLitAgda.Compiler.JS.Parser
intMapAgda.Utils.Warshall
inTopContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
introTacticAgda.Interaction.BasicOps
InvAgda.TypeChecking.Injectivity
InvalidNoTerminationCheckPragmaAgda.Syntax.Concrete.Definitions
InvalidPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InvariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
invariantAgda.Utils.Graph
InverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inverseApplyRelevanceAgda.TypeChecking.Irrelevance
inverseComposeRelevanceAgda.TypeChecking.Irrelevance
inverseScopeLookupAgda.Syntax.Scope.Base
inverseScopeLookupModuleAgda.Syntax.Scope.Base
inverseScopeLookupNameAgda.Syntax.Scope.Base
inverseSubstAgda.TypeChecking.MetaVars
invertPAgda.Utils.Permutation
InvViewAgda.TypeChecking.Injectivity
ioAgda.TypeChecking.Primitive
IOExceptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iotapossmetaAgda.Auto.Typecheck
iotastepAgda.Auto.Typecheck
IOTCM 
1 (Type/Class)Agda.Interaction.InteractionTop
2 (Data Constructor)Agda.Interaction.InteractionTop
iPatternSynsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IrrAgda.Compiler.Epic.Interface
IrrelAgda.TypeChecking.MetaVars.Occurs
IrrelevantAgda.Syntax.Common
IrrelevantDatatypeAgda.TypeChecking.Coverage
IrrelevantlyAgda.TypeChecking.Free
irrelevantOrUnusedAgda.TypeChecking.Irrelevance
irrelevantVarsAgda.TypeChecking.Free
irrToNonStrictAgda.TypeChecking.Irrelevance
IsAbstractAgda.Syntax.Common
isAHoleAgda.Syntax.Notation
isAnonymousModuleNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
isBelowAgda.Utils.Warshall
isBinderUsedAgda.TypeChecking.Free
isBindingHoleAgda.Syntax.Notation
isBlockedTermAgda.TypeChecking.MetaVars
isBoundedAgda.TypeChecking.SizedTypes
isCoinductiveAgda.TypeChecking.Rules.Data
isConAgda.TypeChecking.Quote
iScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IsDataAgda.TypeChecking.Datatypes
isDataOrRecordAgda.TypeChecking.Datatypes
isDataOrRecordTypeAgda.TypeChecking.Datatypes
isDatatype 
1 (Function)Agda.TypeChecking.Datatypes
2 (Function)Agda.TypeChecking.Coverage
isDatatypeModuleAgda.Syntax.Scope.Monad
IsEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmpty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Termination.Matrix
3 (Function)Agda.Termination.SparseMatrix
isEmptyObjectAgda.Compiler.JS.Compiler
IsEmptyTypeAgda.Interaction.BasicOps
isEmptyTypeAgda.TypeChecking.Empty
isEtaExpandableAgda.TypeChecking.MetaVars
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
isInductiveRecordAgda.TypeChecking.Records
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
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
IsLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
IsPatSynAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
isRecAgda.Compiler.Epic.NatDetection
IsRecordAgda.TypeChecking.Datatypes
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
isSetAgda.Syntax.Abstract.Views
isSingleton 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Compiler.JS.Compiler
isSingletonRecordAgda.TypeChecking.Records
isSingletonRecord'Agda.TypeChecking.Records
isSingletonRecordModuloRelevanceAgda.TypeChecking.Records
isSingletonTypeAgda.TypeChecking.Records
isSingletonType'Agda.TypeChecking.Records
isSingletonTypeModuloRelevanceAgda.TypeChecking.Records
isSizeConstraintAgda.TypeChecking.SizedTypes
isSizeNameTestAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeNameTestRawAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeProblemAgda.TypeChecking.SizedTypes
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
isSublistOfAgda.Utils.List
isSubModuleOfAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
isSubscriptDigitAgda.Utils.Suffix
isSubsetOfAgda.Utils.VarSet
isSuccessAgda.Utils.QuickCheck
IsTagAgda.Compiler.Epic.Injection
iStartAgda.Syntax.Position
isTopLevelValueAgda.Compiler.JS.Compiler
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.InteractionTop
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
JustNegAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
JustPosAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
JustSortAgda.Interaction.BasicOps
JustTypeAgda.Interaction.BasicOps
keepCommentsAgda.Syntax.Parser.Comments
keepCommentsMAgda.Syntax.Parser.Comments
keysAgda.Utils.HashMap
Keyword 
1 (Data Constructor)Agda.Interaction.Highlighting.Precise
2 (Type/Class)Agda.Syntax.Parser.Tokens
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
killRangeAgda.Syntax.Position
killRange1Agda.Syntax.Position
killRange2Agda.Syntax.Position
killRange3Agda.Syntax.Position
killRange4Agda.Syntax.Position
killRange5Agda.Syntax.Position
killRange6Agda.Syntax.Position
killRange7Agda.Syntax.Position
KillVarAgda.TypeChecking.Test.Generators
killVarAgda.TypeChecking.Test.Generators
KindOfNameAgda.Syntax.Scope.Base
KwAbstractAgda.Syntax.Parser.Tokens
KwBUILTINAgda.Syntax.Parser.Tokens
KwCoDataAgda.Syntax.Parser.Tokens
KwCoInductiveAgda.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
KwInductiveAgda.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
KwNO_TERMINATION_CHECKAgda.Syntax.Parser.Tokens
KwOpenAgda.Syntax.Parser.Tokens
KwOPTIONSAgda.Syntax.Parser.Tokens
KwPatternSynAgda.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
lambdaLiftExprAgda.Syntax.Abstract
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
lblBindingsAgda.TypeChecking.Coverage.SplitTree
lblConstructorNameAgda.TypeChecking.Coverage.SplitTree
lblSplitArgAgda.TypeChecking.Coverage.SplitTree
lbraceAgda.Utils.Pretty
lbrackAgda.Utils.Pretty
LCharAgda.Compiler.Epic.AuxAST
leAgda.Termination.CallGraph
leaveTopAgda.TypeChecking.MetaVars.Occurs
LeftAssocAgda.Syntax.Fixity
LeftDisjunctAgda.Auto.NarrowingSearch
leftDistributiveAgda.Utils.TestHelpers
LeftHandSideAgda.Syntax.Translation.ConcreteToAbstract
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
LetDefsAgda.Syntax.Translation.ConcreteToAbstract
LetInfoAgda.Syntax.Info
LetOpenAgda.Syntax.Abstract
LetPatBindAgda.Syntax.Abstract
LetRangeAgda.Syntax.Info
lettAgda.Compiler.Epic.AuxAST
Level 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
3 (Type/Class)Agda.Interaction.Highlighting.Generate
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
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
lhsAsBAgda.TypeChecking.Rules.LHS.Problem
LHSCore 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
lhsCoreAgda.Syntax.Abstract
LHSCore'Agda.Syntax.Abstract
lhsCoreAllPatternsAgda.Syntax.Abstract
lhsCoreToPatternAgda.Syntax.Abstract
lhsCoreToSpineAgda.Syntax.Abstract
lhsDefName 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsDestructor 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsDPIAgda.TypeChecking.Rules.LHS.Problem
lhsFocus 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
LHSHead 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
LHSInfoAgda.Syntax.Info
lhsInfoAgda.Syntax.Abstract
lhsOriginalPatternAgda.Syntax.Concrete
LHSOrPatSynAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lhsPats 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsPatsLeft 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsPatsRight 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsProblemAgda.TypeChecking.Rules.LHS.Problem
LHSProj 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
LHSRangeAgda.Syntax.Info
lhsRewriteEqnAgda.Syntax.Concrete
LHSState 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
lhsSubstAgda.TypeChecking.Rules.LHS.Problem
lhsToSpineAgda.Syntax.Abstract
lhsWithExprAgda.Syntax.Concrete
lhsWithPatsAgda.Syntax.Abstract
lhsWithPatternAgda.Syntax.Concrete
LiftAgda.TypeChecking.Substitute
liftAgda.Auto.CaseSplit
liftCommandMAgda.Interaction.InteractionTop
liftCommandMTAgda.Interaction.InteractionTop
liftP 
1 (Function)Agda.Utils.Permutation
2 (Function)Agda.Syntax.Parser.LookAhead
liftSAgda.TypeChecking.Substitute
liftTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
liftUnderAbsAgda.TypeChecking.MetaVars.Occurs
lineLengthAgda.Utils.Pretty
LIntAgda.Compiler.Epic.AuxAST
LispAgda.Interaction.EmacsCommand
lispifyHighlightingInfoAgda.Interaction.Highlighting.Emacs
listAgda.TypeChecking.Primitive
List2 
1 (Type/Class)Agda.Utils.Tuple
2 (Data Constructor)Agda.Utils.Tuple
list2Agda.Utils.Tuple
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.Monad.Builtin
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
localScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localStateAgda.Utils.Monad
localTerminationEnvAgda.Auto.CaseSplit
localTerminationSidecondAgda.Auto.CaseSplit
localToAbstractAgda.Syntax.Translation.ConcreteToAbstract
LocalVAgda.Syntax.Concrete.Operators.Parser
LocalVarsAgda.Syntax.Scope.Base
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.HashMap
2 (Function)Agda.Utils.Graph
3 (Function)Agda.Compiler.JS.Substitution
lookupDefaultAgda.Utils.HashMap
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
lookupPatternSynAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
lookupPrimitiveFunctionAgda.TypeChecking.Primitive
lookupPrimitiveFunctionQAgda.TypeChecking.Primitive
lookupSAgda.TypeChecking.Substitute
lookupSectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
LowerMetaAgda.Interaction.InteractionTop
lowerMetaAgda.Interaction.InteractionTop
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
makeForcedArgsAgda.Compiler.Epic.ForceConstrs
makeInstanceAgda.Syntax.Common
makeOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
makeProjectionAgda.TypeChecking.ProjectionLike
makeSubstitutionAgda.TypeChecking.Rules.LHS.Unify
MAlonzoAgda.Interaction.InteractionTop
manyAgda.Utils.ReadP
many1Agda.Utils.ReadP
manyTillAgda.Utils.ReadP
map 
1 (Function)Agda.Utils.HashMap
2 (Function)Agda.Compiler.JS.Substitution
map'Agda.Compiler.JS.Substitution
mapArgHidingAgda.Syntax.Common
mapArgRelevanceAgda.Syntax.Common
mapConAgda.Compiler.Epic.Primitive
mapDomHidingAgda.Syntax.Common
mapDomRelevanceAgda.Syntax.Common
mapEither 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.Either
mapFlagAgda.Interaction.Options
mapFstAgda.Utils.Tuple
mapFstMAgda.Utils.Tuple
mapLeftAgda.Utils.Either
mapLHSHeadAgda.Syntax.Abstract
mapM'Agda.Utils.Monad
mapMaybeAgda.Utils.Maybe
mapMaybeMAgda.Utils.Monad
mapNameSpaceAgda.Syntax.Scope.Base
mapNameSpaceMAgda.Syntax.Scope.Base
mapNodesAgda.Utils.Warshall
mapPairMAgda.Utils.Tuple
mappingAgda.Compiler.JS.Compiler
mapping'Agda.Compiler.JS.Compiler
mapRightAgda.Utils.Either
MapSAgda.Auto.Convert
mapScopeAgda.Syntax.Scope.Base
mapScopeMAgda.Syntax.Scope.Base
mapScopeM_Agda.Syntax.Scope.Base
mapScope_Agda.Syntax.Scope.Base
mapSizeAgda.Utils.QuickCheck
mapSndAgda.Utils.Tuple
mapSndMAgda.Utils.Tuple
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
MatchedAgda.TypeChecking.Positivity
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.Matrix
2 (Type/Class)Agda.Termination.SparseMatrix
3 (Type/Class)Agda.Utils.Warshall
matrix 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
3 (Function)Agda.Utils.Warshall
matrixInvariant 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
matrixUsingRowGen 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
MaxAgda.Syntax.Internal
maxDiscardRatioAgda.Utils.QuickCheck
maxNameAgda.TypeChecking.Level
maxSizeAgda.Utils.QuickCheck
maxSuccessAgda.Utils.QuickCheck
maxViewConsAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
maxViewMaxAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
maxViewSuc_Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
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
member 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.HashMap
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
mergeScopeAgda.Syntax.Scope.Base
mergeScopesAgda.Syntax.Scope.Base
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.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Type/Class)Agda.Syntax.Info
4 (Data Constructor)Agda.Syntax.Info
5 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
6 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaInstantiationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MetaKindAgda.TypeChecking.MetaVars
MetaLevelAgda.Syntax.Internal
metaliseokhAgda.Auto.Syntax
MetaNameSuggestionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
metaNameSuggestionAgda.Syntax.Info
metaNumberAgda.Syntax.Info
metaOccursAgda.TypeChecking.MetaVars.Occurs
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
miClosRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
MIdAgda.Auto.Syntax
miInterfaceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
miMetaOccursCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mimicGHCiAgda.Interaction.GhcTop
miNameSuggestionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
minfoAsNameAgda.Syntax.Info
minfoAsToAgda.Syntax.Info
minfoDirectiveAgda.Syntax.Info
minfoOpenShortAgda.Syntax.Info
minfoRangeAgda.Syntax.Info
minusAgda.Interaction.Highlighting.Range
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.Matrix
2 (Data Constructor)Agda.Termination.Matrix
3 (Type/Class)Agda.Termination.SparseMatrix
4 (Data Constructor)Agda.Termination.SparseMatrix
MixedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
mIxInvariant 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
mkAbsAgda.TypeChecking.Substitute
mkAbsoluteAgda.Utils.FileName
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
mkName_Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mkNotationAgda.Syntax.Notation
mkPiAgda.TypeChecking.Substitute
mkPrimFun1Agda.TypeChecking.Primitive
mkPrimFun1TCMAgda.TypeChecking.Primitive
mkPrimFun2Agda.TypeChecking.Primitive
mkPrimFun4Agda.TypeChecking.Primitive
mkPrimLevelMaxAgda.TypeChecking.Primitive
mkPrimLevelSucAgda.TypeChecking.Primitive
mkPrimLevelZeroAgda.TypeChecking.Primitive
MkStrAgda.Utils.QuickCheck
mkTypeAgda.Syntax.Internal
mkUnusedAgda.TypeChecking.Polarity
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
mnameFromListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mnameToConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mnameToListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mnameToQNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
mobsAgda.Auto.NarrowingSearch
ModeAgda.Utils.Pretty
modeAgda.Utils.Pretty
modifyAbstractClauseAgda.Auto.Convert
modifyAbstractExprAgda.Auto.Convert
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
modifyCurrentScopeAgda.Syntax.Scope.Monad
modifyCurrentScopeMAgda.Syntax.Scope.Monad
modifyEIAgda.Compiler.Epic.CompileState
modifyImportedSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
modifyMetaStoreAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
modifyNamedScopeAgda.Syntax.Scope.Monad
modifyNamedScopeMAgda.Syntax.Scope.Monad
modifyOccursCheckDefsAgda.TypeChecking.MetaVars.Occurs
modifyPatternSynsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
modifyScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
modifyScopeInfoAgda.Syntax.Scope.Monad
modifyScopesAgda.Syntax.Scope.Monad
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
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
ModulesInScopeAgda.Syntax.Scope.Base
ModuleTagAgda.Syntax.Scope.Base
ModuleToSourceAgda.Interaction.FindFile
MonadExceptionAgda.TypeChecking.Monad.Exception
MonadTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
moreRelevantAgda.Syntax.Common
movePosAgda.Syntax.Position
movePosByStringAgda.Syntax.Position
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.Matrix
3 (Function)Agda.Termination.SparseMatrix
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
MutualInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
mutuallyRecursiveAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
mutualRangeAgda.Syntax.Info
mutualTermCheckAgda.Syntax.Info
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
4 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
5 (Data Constructor)Agda.Interaction.Highlighting.Precise
nameBindingSiteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
nameConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
Named 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
namedAgda.Syntax.Common
NamedArgAgda.Syntax.Common
namedArgAgda.Syntax.Common
NamedClauseAgda.Syntax.Translation.InternalToAbstract
NamedMeta 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
namedThingAgda.Syntax.Common
nameFixityAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
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
NameKindAgda.Interaction.Highlighting.Precise
nameModifiersAgda.Interaction.InteractionTop
nameOfAgda.Syntax.Common
nameOfBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
nameOfFlatAgda.TypeChecking.Monad.Builtin
nameOfInfAgda.TypeChecking.Monad.Builtin
nameOfSharpAgda.TypeChecking.Monad.Builtin
NamePartAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
namePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
NamesInScopeAgda.Syntax.Scope.Base
namesInScopeAgda.Syntax.Scope.Base
NameSpace 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
nameSpaceAccessAgda.Syntax.Scope.Base
NameSpaceIdAgda.Syntax.Scope.Base
nameStringPartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
nameSupplyAgda.Compiler.Epic.CompileState
NameTagAgda.Syntax.Scope.Base
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
NeedOptionCopatternsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
negAgda.TypeChecking.Polarity
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
newArgsMeta'Agda.TypeChecking.MetaVars
newArgsMetaCtxAgda.TypeChecking.MetaVars
newArgsMetaCtx'Agda.TypeChecking.MetaVars
newCTreeAgda.Auto.NarrowingSearch
newEdgeAgda.Utils.Warshall
NewFlexAgda.Utils.Warshall
newIFSMetaAgda.TypeChecking.MetaVars
newIFSMetaCtxAgda.TypeChecking.MetaVars
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
NewModuleQName 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract
NewNameAgda.Syntax.Translation.ConcreteToAbstract
newNameAgda.Compiler.Epic.CompileState
newNamedValueMetaAgda.TypeChecking.MetaVars
NewNotationAgda.Syntax.Fixity
newOKHandleAgda.Auto.NarrowingSearch
newPlaceholderAgda.Auto.NarrowingSearch
newProblemAgda.TypeChecking.Constraints
newProblem_Agda.TypeChecking.Constraints
newPtrAgda.Utils.Pointer, Agda.Syntax.Internal
newQuestionMarkAgda.TypeChecking.MetaVars
newRecordMetaAgda.TypeChecking.MetaVars
newRecordMetaCtxAgda.TypeChecking.MetaVars
newSortMetaAgda.TypeChecking.MetaVars
newSortMetaCtxAgda.TypeChecking.MetaVars
newSubConstraintsAgda.Auto.NarrowingSearch
newTelMetaAgda.TypeChecking.MetaVars
newTypeMetaAgda.TypeChecking.MetaVars
newTypeMeta_Agda.TypeChecking.MetaVars
newValueMetaAgda.TypeChecking.MetaVars
newValueMeta'Agda.TypeChecking.MetaVars
newValueMetaCtxAgda.TypeChecking.MetaVars
newValueMetaCtx'Agda.TypeChecking.MetaVars
nextCharAgda.Syntax.Parser.LookAhead
nextFreshAgda.Utils.Fresh
nextNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
nextNodeAgda.Utils.Warshall
nextPolarityAgda.TypeChecking.Polarity
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
NiceFunClauseAgda.Syntax.Concrete.Definitions
NiceImportAgda.Syntax.Concrete.Definitions
NiceModuleAgda.Syntax.Concrete.Definitions
NiceModuleMacroAgda.Syntax.Concrete.Definitions
NiceMutualAgda.Syntax.Concrete.Definitions
NiceOpenAgda.Syntax.Concrete.Definitions
NicePatternSynAgda.Syntax.Concrete.Definitions
NicePragmaAgda.Syntax.Concrete.Definitions
NiceRecSigAgda.Syntax.Concrete.Definitions
NiceTypeSignatureAgda.Syntax.Concrete.Definitions
nmidAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
nmSuggestionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
nodeInAgda.Utils.Graph
nodeMapAgda.Utils.Warshall
nodesAgda.Utils.Graph
NoElimAgda.TypeChecking.Eliminators
NoExpectedFailureAgda.Utils.QuickCheck
noFixityAgda.Syntax.Fixity
NoHighlightingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
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
NoneAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
NonEmptyAgda.Utils.QuickCheck
NonEmptyListAgda.Utils.QuickCheck
nonfixPAgda.Syntax.Concrete.Operators.Parser
NonInteractiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
NonvariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
nonvariantToUnusedArgAgda.TypeChecking.Polarity
nonvariantToUnusedArgInClauseAgda.TypeChecking.Polarity
nonvariantToUnusedArgInDefAgda.TypeChecking.Polarity
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
noProblemRestAgda.TypeChecking.Rules.LHS.ProblemRest
noPropAgda.TypeChecking.Test.Generators
noRangeAgda.Syntax.Position
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
normaliseAgda.TypeChecking.Reduce
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
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
NotComparableAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
NotDelayedAgda.Syntax.Common
noteAgda.Interaction.Highlighting.Precise
notequalAgda.Auto.CaseSplit
NoTerminationCheckPragmaAgda.Syntax.Concrete
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
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
notSoNiceDeclarationAgda.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
nsNamesAgda.Syntax.Scope.Base
nullAgda.Utils.HashMap
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
OccEnv 
1 (Type/Class)Agda.TypeChecking.Positivity
2 (Data Constructor)Agda.TypeChecking.Positivity
occFunctionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OccMAgda.TypeChecking.Positivity
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
OffsetAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
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
OldName 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract
OldQNameAgda.Syntax.Translation.ConcreteToAbstract
oldToNewNotationAgda.Syntax.Fixity
onceAgda.Utils.QuickCheck
OneHolePatternAgda.Syntax.Internal.Pattern
OneHolePatternsAgda.Syntax.Internal.Pattern
OneLineModeAgda.Utils.Pretty
oneofAgda.Utils.QuickCheck
OnlyQualifiedAgda.Syntax.Common
OnlyQualifiedNSAgda.Syntax.Scope.Base
onlyVarsUpToAgda.TypeChecking.Positivity
onSubAgda.TypeChecking.Rules.LHS.Unify
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
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
optCopatternsAgda.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
optGenerateLaTeXAgda.Interaction.Options
optGenerateVimFileAgda.Interaction.Options
optGhcFlagsAgda.Interaction.Options
optGHCiInteractionAgda.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
optionsOnReloadAgda.Interaction.InteractionTop
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
optLaTeXDirAgda.Interaction.Options
optPragmaOptionsAgda.Interaction.Options
optProgramNameAgda.Interaction.Options
optProofIrrelevanceAgda.Interaction.Options
optRunTestsAgda.Interaction.Options
optSafeAgda.Interaction.Options
optShowHelpAgda.Interaction.Options
optShowImplicitAgda.Interaction.Options
optShowIrrelevantAgda.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
or2MAgda.Utils.Monad
OrderAgda.Termination.CallGraph
OrderedAgda.Utils.QuickCheck
OrderedListAgda.Utils.QuickCheck
orderedListAgda.Utils.QuickCheck
orderFieldsAgda.TypeChecking.Records
orderMatAgda.Termination.CallGraph
OrdinaryAgda.Syntax.Concrete
orMAgda.Utils.Monad
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
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
overlapping 
1 (Function)Agda.Interaction.Highlighting.Range
2 (Function)Agda.TypeChecking.Coverage.Match
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
parallelSAgda.TypeChecking.Substitute
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
parens'Agda.Interaction.InteractionTop
ParenVAgda.Syntax.Concrete.Operators.Parser
ParseAgda.Interaction.InteractionTop
parse 
1 (Function)Agda.Utils.ReadP
2 (Function)Agda.Compiler.JS.Parser
3 (Function)Agda.Syntax.Parser.Monad
4 (Function)Agda.Syntax.Parser
parse'Agda.Utils.ReadP
parseAndDoAtToplevelAgda.Interaction.InteractionTop
parseApplicationAgda.Syntax.Concrete.Operators
ParseError 
1 (Type/Class)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
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
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
ParseOkAgda.Syntax.Parser.Monad
parsePatAgda.Syntax.Concrete.Operators
parsePatternAgda.Syntax.Concrete.Operators
parsePatternSynAgda.Syntax.Concrete.Operators
parsePluginOptionsAgda.Interaction.Options
parsePosAgda.Syntax.Parser.Monad
parsePosString 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.Syntax.Parser
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
ParseResultAgda.Syntax.Parser.Monad
parseStandardOptionsAgda.Interaction.Options
ParseStateAgda.Syntax.Parser.Monad
parseToReadsPrecAgda.Interaction.InteractionTop
PartialAgda.Interaction.Highlighting.Generate
partPAgda.Syntax.Concrete.Operators.Parser
PatAgda.Auto.Syntax
patchUpTrailingImplicitsAgda.TypeChecking.Rules.Def
PatConAppAgda.Auto.Syntax
PatExpAgda.Auto.Syntax
PatInfoAgda.Syntax.Info
PatNameAgda.Syntax.Translation.ConcreteToAbstract
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
patternAppViewAgda.Syntax.Concrete.Operators
PatternErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
patternHeadAgda.Syntax.Concrete
patternNamesAgda.Syntax.Concrete
patternQNamesAgda.Syntax.Concrete.Operators
PatternsAgda.Syntax.Abstract
PatternShadowsConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PatternSyn 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
PatternSynDefnAgda.Syntax.Abstract
PatternSynDefnsAgda.Syntax.Abstract
PatternSynNameAgda.Syntax.Scope.Base
PatternSynonymArityMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PatternSynPAgda.Syntax.Abstract
PatternSynResNameAgda.Syntax.Scope.Monad
patternToExprAgda.Syntax.Abstract
patternToTermAgda.Compiler.Epic.Injection
patternVarsAgda.Syntax.Internal
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
permPicksAgda.Utils.Permutation
permRangeAgda.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
pointAgda.Utils.Pointed
PointedAgda.Utils.Pointed
pointerChainAgda.Syntax.Internal
polaritiesAgda.TypeChecking.Polarity
PolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
polarityAgda.TypeChecking.Polarity
polFromOccAgda.TypeChecking.Polarity
popAgda.Compiler.JS.Case
popContextAgda.Syntax.Parser.Monad
popLexStateAgda.Syntax.Parser.Monad
popMapSAgda.Auto.Convert
posColAgda.Syntax.Position
PositionAgda.Syntax.Position
Position'Agda.Syntax.Position
positionInvariantAgda.Syntax.Position
Positive 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
positiveAgda.Utils.TestHelpers
positivityCheckEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
posLineAgda.Syntax.Position
posPosAgda.Syntax.Position
PossiblyAgda.TypeChecking.Rules.LHS.Unify
postfixPAgda.Syntax.Concrete.Operators.Parser
postopAgda.Syntax.Concrete.Operators.Parser
posToRangeAgda.Syntax.Position
PostponedTypeCheckingProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
postponeTypeCheckingProblemAgda.TypeChecking.MetaVars
postponeTypeCheckingProblem_Agda.TypeChecking.MetaVars
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.InteractionTop
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.InteractionTop
prettyEpicAgda.Compiler.Epic.Epic
prettyEpicFunAgda.Compiler.Epic.Epic
prettyErrorAgda.TypeChecking.Errors
prettyListAgda.TypeChecking.Pretty
prettyOpAppAgda.Syntax.Concrete.Pretty
prettyPrecAgda.Utils.Pretty
prettyPrintAgda.Compiler.MAlonzo.Pretty
PrettyTCMAgda.TypeChecking.Pretty, Agda.TypeChecking.Errors
prettyTCMAgda.TypeChecking.Pretty, Agda.TypeChecking.Errors
prettyTypeOfMetaAgda.Interaction.InteractionTop
preUscoreAgda.Interaction.InteractionTop
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
primIrrAxiomAgda.TypeChecking.Monad.Builtin
primIrrelevantAgda.TypeChecking.Monad.Builtin
Primitive 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.Syntax.Abstract
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
primRelevanceAgda.TypeChecking.Monad.Builtin
primRelevantAgda.TypeChecking.Monad.Builtin
primSharpAgda.TypeChecking.Monad.Builtin
primSizeAgda.TypeChecking.Monad.Builtin
primSizeInfAgda.TypeChecking.Monad.Builtin
primSizeLtAgda.TypeChecking.Monad.Builtin
primSizeMaxAgda.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
printErrorInfoAgda.Interaction.Highlighting.Generate
printHighlightingInfoAgda.Interaction.Highlighting.Generate
printTestCaseAgda.Utils.QuickCheck
printUnsolvedInfoAgda.Interaction.Highlighting.Generate
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
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
problemFromPatsAgda.TypeChecking.Rules.LHS.ProblemRest
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
ProblemRest 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
problemRestAgda.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
properlyMatchingAgda.Syntax.Internal
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_galoisAgda.TypeChecking.Irrelevance
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, Agda.Syntax.Internal
PublicAccessAgda.Syntax.Common
publicModulesAgda.Syntax.Scope.Base
PublicNSAgda.Syntax.Scope.Base
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
purgeNonvariantAgda.TypeChecking.Polarity
pushContextAgda.Syntax.Parser.Monad
pushCurrentContextAgda.Syntax.Parser.Monad
pushLexStateAgda.Syntax.Parser.Monad
putAllConstraintsToSleepAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
putConArityAgda.Compiler.Epic.CompileState
putConstrTagAgda.Compiler.Epic.CompileState
putDelayedAgda.Compiler.Epic.CompileState
putForcedArgsAgda.Compiler.Epic.CompileState
putMainAgda.Compiler.Epic.CompileState
putResponse 
1 (Function)Agda.Interaction.EmacsCommand
2 (Function)Agda.Interaction.InteractionTop
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
4 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qname 
1 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
2 (Function)Agda.Compiler.JS.Compiler
QNamed 
1 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qnamedAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qnameFromListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qnameModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qnameNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qnamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qnameToConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qnameToListAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qnameToMNameAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qNameTypeAgda.TypeChecking.Quote
QPBAgda.Auto.NarrowingSearch
QPBlockedAgda.Auto.NarrowingSearch
QPDoubleBlockedAgda.Auto.NarrowingSearch
QualAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qualifierModulesAgda.Syntax.Concrete.Operators
qualify 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qualifyMAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
qualifyQAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
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
raiseFromAgda.TypeChecking.Substitute
raiseSAgda.TypeChecking.Substitute
Range 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
3 (Type/Class)Agda.Interaction.Highlighting.Range
4 (Data Constructor)Agda.Interaction.Highlighting.Range
Range'Agda.Syntax.Position
RangeAndPragma 
1 (Type/Class)Agda.Syntax.Translation.AbstractToConcrete
2 (Data Constructor)Agda.Syntax.Translation.AbstractToConcrete
rangeInvariant 
1 (Function)Agda.Syntax.Position
2 (Function)Agda.Interaction.Highlighting.Range
Ranges 
1 (Type/Class)Agda.Interaction.Highlighting.Range
2 (Data Constructor)Agda.Interaction.Highlighting.Range
ranges 
1 (Function)Agda.Utils.QuickCheck
2 (Function)Agda.Interaction.Highlighting.Precise
rangesInvariantAgda.Interaction.Highlighting.Range
rangesToPositionsAgda.Interaction.Highlighting.Range
rangeToIntervalAgda.Syntax.Position
rangeToPositionsAgda.Interaction.Highlighting.Range
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
readParseAgda.Interaction.InteractionTop
readsToParseAgda.Interaction.InteractionTop
readTextFileAgda.Utils.IO.UTF8
reallyUnLevelViewAgda.TypeChecking.Level
reasonAgda.Utils.QuickCheck
rebindClauseAgda.TypeChecking.Rebind
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
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
recInductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recMutualAgda.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
recordPatternToProjectionsAgda.TypeChecking.RecordPatterns
RecordsAgda.TypeChecking.MetaVars
RecordSigAgda.Syntax.Concrete
recParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
recRecursiveAgda.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
recursiveRecordAgda.TypeChecking.Records
redBindAgda.TypeChecking.Primitive
redReturnAgda.TypeChecking.Primitive
ReduceAgda.TypeChecking.Reduce
reduceAgda.TypeChecking.Reduce
reduceBAgda.TypeChecking.Reduce
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
reduceDefAgda.TypeChecking.Reduce
reduceDefCopyAgda.TypeChecking.Reduce
reduceDef_Agda.TypeChecking.Reduce
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.InteractionTop
ReifyAgda.Syntax.Translation.InternalToAbstract
reifyAgda.Syntax.Translation.InternalToAbstract
reifyPatternsAgda.Syntax.Translation.InternalToAbstract
ReifyWhenAgda.Syntax.Translation.InternalToAbstract
reifyWhenAgda.Syntax.Translation.InternalToAbstract
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
relevantInIgnoringNonvariantAgda.TypeChecking.Polarity
relevantInIgnoringSortAnnAgda.TypeChecking.Free
relevantVarsAgda.TypeChecking.Free
relOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
remAbsAgda.Compiler.Epic.Injection
remForcedAgda.Compiler.Epic.Forcing
removeEdgeAgda.Utils.Graph
removeInteractionPointAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
removeNodeAgda.Utils.Graph
removeOnlyQualifiedAgda.Syntax.Scope.Base
removeSucsAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
removeUnusedAgda.Compiler.Epic.Erasure
removevarAgda.Auto.CaseSplit
RenAgda.Syntax.Scope.Monad
renAgda.Auto.CaseSplit
renameAgda.Auto.CaseSplit
renameCanonicalNamesAgda.Syntax.Scope.Base
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
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
ResAgda.TypeChecking.MetaVars
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
resolveModuleAgda.Syntax.Scope.Monad
resolveNameAgda.Syntax.Scope.Monad
ResponseAgda.Interaction.Response
responseAgda.Interaction.EmacsCommand
Resp_ClearHighlightingAgda.Interaction.Response
Resp_ClearRunningInfoAgda.Interaction.Response
Resp_DisplayInfoAgda.Interaction.Response
Resp_GiveActionAgda.Interaction.Response
Resp_HighlightingInfoAgda.Interaction.Response
Resp_InteractionPointsAgda.Interaction.Response
Resp_JumpToErrorAgda.Interaction.Response
Resp_MakeCaseAgda.Interaction.Response
Resp_MakeCaseActionAgda.Interaction.Response
Resp_RunningInfoAgda.Interaction.Response
Resp_SolveAllAgda.Interaction.Response
Resp_StatusAgda.Interaction.Response
Restore 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
restPatsAgda.TypeChecking.Rules.LHS.Problem
restrictPrivateAgda.Syntax.Scope.Base
restTypeAgda.TypeChecking.Rules.LHS.Problem
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
returnTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
reverseCCBodyAgda.Compiler.Epic.FromAgda
reversePAgda.Utils.Permutation
revLiftAgda.Interaction.InteractionTop
RewriteAgda.Interaction.BasicOps
rewriteAgda.Interaction.BasicOps
RewriteEqnAgda.Syntax.Concrete
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
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.SizedTypes
4 (Data Constructor)Agda.TypeChecking.MetaVars.Occurs
RigidIdAgda.Utils.Warshall
rigidVarsAgda.TypeChecking.Free
rigidVarsNotContainedInAgda.TypeChecking.MetaVars.Occurs
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.Matrix
2 (Function)Agda.Termination.SparseMatrix
rowdescrAgda.Utils.Warshall
rows 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
rparenAgda.Utils.Pretty
rStartAgda.Syntax.Position
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
runAgdaAgda.Main
runCommandMAgda.Interaction.InteractionTop
runExceptionTAgda.TypeChecking.Monad.Exception
runIMAgda.Interaction.Monad
runInteractionAgda.Interaction.InteractionTop
runLookAheadAgda.Syntax.Parser.LookAhead
RunMetaOccursCheck 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
runNiceAgda.Syntax.Concrete.Definitions
runSafeTCMAgda.Interaction.InteractionTop
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
SafeFlagNoTerminationCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
sccsAgda.Utils.Graph
sccs'Agda.Utils.Graph
scflipAgda.Auto.NarrowingSearch
sCheckedAgda.Interaction.Response
SClauseAgda.TypeChecking.Coverage
sConstsAgda.Auto.Convert
Scope 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.Syntax.Scope.Base
3 (Data Constructor)Agda.Syntax.Scope.Base
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
scopeDatatypeModuleAgda.Syntax.Scope.Base
ScopedDeclAgda.Syntax.Abstract
ScopedExprAgda.Syntax.Abstract
scopeImportsAgda.Syntax.Scope.Base
ScopeInfo 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
scopeLocalsAgda.Syntax.Scope.Base
scopeLookupAgda.Syntax.Scope.Base
scopeLookup'Agda.Syntax.Scope.Base
ScopeMAgda.Syntax.Scope.Monad
scopeModulesAgda.Syntax.Scope.Base
scopeNameAgda.Syntax.Scope.Base
scopeNameSpaceAgda.Syntax.Scope.Base
scopeNameSpacesAgda.Syntax.Scope.Base
scopeParentsAgda.Syntax.Scope.Base
scopePrecedenceAgda.Syntax.Scope.Base
scPatsAgda.TypeChecking.Coverage
scPermAgda.TypeChecking.Coverage
scsub1Agda.Auto.NarrowingSearch
scsub2Agda.Auto.NarrowingSearch
scSubstAgda.TypeChecking.Coverage
scTargetAgda.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
setCommandLineOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setCommandLineOptions'Agda.Interaction.InteractionTop
setContextPrecedenceAgda.Syntax.Scope.Monad
setCurrentModuleAgda.Syntax.Scope.Monad
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
setMetaNameSuggestionAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
setMutualAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
SetNAgda.Syntax.Concrete
setNameSpaceAgda.Syntax.Scope.Base
SetOmegaNotValidTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setOptionsFromPragmaAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setParsePosAgda.Syntax.Parser.Monad
setPatternSynsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setPolarityAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setPragmaOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
setPrevTokenAgda.Syntax.Parser.Monad
setPtrAgda.Utils.Pointer, Agda.Syntax.Internal
SetRange 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
setRangeAgda.Syntax.Position
setScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setScopeAccessAgda.Syntax.Scope.Base
setSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setTagAgda.Compiler.Epic.Injection
setTerminatesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
setTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
setValueMetaNameAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
setVisitedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
severalAgda.Interaction.Highlighting.Precise
severalCAgda.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
SharedAgda.Syntax.Internal
sharedAgda.Syntax.Internal
sharedTypeAgda.Syntax.Internal
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
ShouldBeRecordPatternAgda.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
ShowImplicitArgsAgda.Interaction.InteractionTop
showImplicitArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showIndexAgda.Utils.String
showIrrelevantArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
showMetasAgda.Interaction.CommandLine.CommandLine
showModuleContentsAgda.Interaction.InteractionTop
showPatAgda.TypeChecking.With
showQNameIdAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
showScopeAgda.Interaction.CommandLine.CommandLine
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.HashMap
3 (Function)Agda.Utils.Trie
4 (Function)Agda.Utils.Graph
5 (Function)Agda.Interaction.Highlighting.Precise
singletonCAgda.Interaction.Highlighting.Precise
SingletonRecordsAgda.TypeChecking.MetaVars
singletonSAgda.TypeChecking.Substitute
Size 
1 (Type/Class)Agda.Termination.Matrix
2 (Data Constructor)Agda.Termination.Matrix
3 (Type/Class)Agda.Termination.SparseMatrix
4 (Data Constructor)Agda.Termination.SparseMatrix
size 
1 (Function)Agda.Utils.HashMap
2 (Function)Agda.Termination.Matrix
3 (Function)Agda.Utils.Size
4 (Function)Agda.Termination.SparseMatrix
5 (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.Matrix
2 (Function)Agda.Termination.SparseMatrix
sizeMaxAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
SizeMaxViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeMaxViewAgda.TypeChecking.SizedTypes
SizeMetaAgda.TypeChecking.SizedTypes
sizePolarityAgda.TypeChecking.Polarity
sizeRigidAgda.Utils.Warshall
SizeSucAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSucAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSucNameAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeSuc_Agda.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
SizeViewComparableAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewComparableAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewComparableWithMaxAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewOffsetAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewPredAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
sizeViewSuc_Agda.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
smallestPosCAgda.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
snd3Agda.Utils.Tuple
SolAgda.Auto.CaseSplit
SolutionAgda.Utils.Warshall
solve 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.Compiler.Epic.Injection
solveAwakeConstraintsAgda.TypeChecking.Constraints
solveAwakeConstraints'Agda.TypeChecking.Constraints
solveConstraintAgda.TypeChecking.Constraints
solveConstraint_Agda.TypeChecking.Constraints
solveIrrelevantMetasAgda.TypeChecking.InstanceArguments
solveMetaIfIrrelevantAgda.TypeChecking.InstanceArguments
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
sortedAgda.Utils.List
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.InteractionTop
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
SpineLHS 
1 (Type/Class)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Abstract
splashScreenAgda.Interaction.CommandLine.CommandLine
spLhsDefNameAgda.Syntax.Abstract
spLhsInfoAgda.Syntax.Abstract
spLhsPatsAgda.Syntax.Abstract
spLhsWithPatsAgda.Syntax.Abstract
SplitAgda.TypeChecking.Rules.LHS.Problem
splitAgda.TypeChecking.Coverage
split'Agda.TypeChecking.Coverage
splitArgAgda.TypeChecking.Coverage.SplitTree
SplitAtAgda.TypeChecking.Coverage.SplitTree
splitAtCAgda.Interaction.Highlighting.Precise
splitBindingsAgda.TypeChecking.Coverage.SplitTree
splitCAgda.TypeChecking.CompiledClause.Compile
SplitClauseAgda.TypeChecking.Coverage
splitClausesAgda.TypeChecking.Coverage
splitClauseWithAbsAgda.TypeChecking.Coverage
splitDbIndexToLevelAgda.TypeChecking.Coverage
SplitError 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Type/Class)Agda.TypeChecking.Coverage
splitLastAgda.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
splitSAgda.TypeChecking.Substitute
splitStrategyAgda.TypeChecking.Coverage
SplitTel 
1 (Type/Class)Agda.TypeChecking.Telescope
2 (Data Constructor)Agda.TypeChecking.Telescope
splitTelescopeAgda.TypeChecking.Telescope
SplittingDoneAgda.TypeChecking.Coverage.SplitTree
splitTrailingImplicitsAgda.TypeChecking.Rules.Def
SplitTreeAgda.TypeChecking.Coverage.SplitTree
SplitTree'Agda.TypeChecking.Coverage.SplitTree
SplitTreeLabel 
1 (Type/Class)Agda.TypeChecking.Coverage.SplitTree
2 (Data Constructor)Agda.TypeChecking.Coverage.SplitTree
SplitTreesAgda.TypeChecking.Coverage.SplitTree
splitTreesAgda.TypeChecking.Coverage.SplitTree
SplitTrees'Agda.TypeChecking.Coverage.SplitTree
square 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
srcFileAgda.Syntax.Position
SResAgda.Auto.NarrowingSearch
sShowImplicitArgumentsAgda.Interaction.Response
sSucAgda.Syntax.Internal
StackAgda.TypeChecking.CompiledClause.Match
standardOptions_Agda.Interaction.Options
startPosAgda.Syntax.Position
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.Response
2 (Data Constructor)Agda.Interaction.Response
statusAgda.Interaction.InteractionTop
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
stDirtyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
stInteractionOutputCallbackAgda.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
stOccursCheckDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
storeDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
stPatternSynImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stPatternSynsAgda.TypeChecking.Monad.Base, 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
StrictPosAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
stripDontCareAgda.Syntax.Internal
stripNoNamesAgda.Syntax.Scope.Monad
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
stSyntaxInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stTermErrsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
stTokensAgda.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
SubscriptAgda.Utils.Suffix
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
SubstCandAgda.TypeChecking.MetaVars
substExprAgda.Syntax.Abstract
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
substLetBindingAgda.Syntax.Abstract
substLitAgda.Compiler.Epic.FromAgda
substPatternAgda.Syntax.Abstract
substsAgda.Compiler.Epic.AuxAST
substTermAgda.Compiler.Epic.FromAgda
substTypedBindingAgda.Syntax.Abstract
substTypedBindingsAgda.Syntax.Abstract
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.List
2 (Type/Class)Agda.Utils.Suffix
suffixViewAgda.Utils.Suffix
supremumAgda.Termination.CallGraph
SymArrowAgda.Syntax.Parser.Tokens
SymAsAgda.Syntax.Parser.Tokens
SymBarAgda.Syntax.Parser.Tokens
Symbol 
1 (Data Constructor)Agda.Interaction.Highlighting.Precise
2 (Type/Class)Agda.Syntax.Parser.Tokens
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
takenNameStrAgda.Interaction.InteractionTop
takePAgda.Utils.Permutation
takeRelevantAgda.TypeChecking.MetaVars.Occurs
takeTeleAgda.Compiler.Epic.Forcing
tallyDefAgda.TypeChecking.MetaVars.Occurs
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
TCErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcErrStringAgda.TypeChecking.Errors
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.InteractionTop
tellToUpdateHighlightingAgda.Interaction.InteractionTop
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
telViewUpToAgda.TypeChecking.Telescope
telViewUpTo'Agda.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
termDeclAgda.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
TermHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermHHAgda.TypeChecking.Rules.LHS.Unify
terminatesAgda.Termination.Termination
terminatesFilterAgda.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.TypeChecking.Errors
TermLikeAgda.Syntax.Internal.Generic
TestableAgda.Utils.QuickCheck
tests 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.Matrix
3 (Function)Agda.Utils.List
4 (Function)Agda.Utils.Either
5 (Function)Agda.Termination.SparseMatrix
6 (Function)Agda.Termination.CallGraph
7 (Function)Agda.Termination.Lexicographic
8 (Function)Agda.Termination.Termination
9 (Function)Agda.Utils.FileName, Agda.Interaction.FindFile
10 (Function)Agda.Utils.Graph
11 (Function)Agda.Interaction.Options
12 (Function)Agda.Syntax.Position
13 (Function)Agda.Utils.Warshall
14 (Function)Agda.Interaction.Highlighting.Range
15 (Function)Agda.Interaction.Highlighting.Precise
16 (Function)Agda.Syntax.Parser.Parser
17 (Function)Agda.TypeChecking.Irrelevance
18 (Function)Agda.Interaction.Highlighting.Emacs
19 (Function)Agda.Interaction.Highlighting.Generate
20 (Function)Agda.Compiler.MAlonzo.Encode
21 (Function)Agda.TypeChecking.Tests
testSplitTreePrintingAgda.TypeChecking.Coverage.SplitTree
testSuiteAgda.Tests
text 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
TextDetailsAgda.Utils.Pretty
thd3Agda.Utils.Tuple
theConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theCurrentFileAgda.Interaction.InteractionTop
theDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theFixityAgda.Syntax.Fixity
theInteractionPointsAgda.Interaction.InteractionTop
theNotationAgda.Syntax.Fixity
thenTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ThingsInScopeAgda.Syntax.Scope.Base
thingsInScopeAgda.Syntax.Scope.Base
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
toAbstractAgda.Syntax.Translation.ConcreteToAbstract
ToConcreteAgda.Syntax.Translation.AbstractToConcrete
toConcreteAgda.Syntax.Translation.AbstractToConcrete
toConcreteCtxAgda.Syntax.Translation.AbstractToConcrete
ToggleImplicitArgsAgda.Interaction.InteractionTop
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
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.Utils.HashMap
3 (Function)Agda.Termination.CallGraph
toLists 
1 (Function)Agda.Termination.Matrix
2 (Function)Agda.Termination.SparseMatrix
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
TopAgda.TypeChecking.MetaVars.Occurs
topBindingsAgda.Compiler.Epic.CompileState
topContextAgda.Syntax.Parser.Monad
TopCtxAgda.Syntax.Fixity
TopLevel 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract
topLevelAgda.Compiler.JS.Parser
topLevelDeclsAgda.Syntax.Translation.ConcreteToAbstract
TopLevelInfo 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract
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
topoSortAgda.Utils.Permutation
topSearchAgda.Auto.NarrowingSearch
topSortAgda.Syntax.Internal
toSubscriptDigitAgda.Utils.Suffix
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
toTreeAgda.TypeChecking.Coverage.SplitTree
toTreesAgda.TypeChecking.Coverage.SplitTree
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
traceCallMAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCall_Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceFunAgda.TypeChecking.Reduce
traceFun'Agda.TypeChecking.Reduce
trailingImplicitsAgda.TypeChecking.Rules.Def
transitiveClosureAgda.Utils.Graph
transitiveClosure1Agda.Utils.Graph
translateCaseAgda.Compiler.Epic.Primitive
translateCompiledClausesAgda.TypeChecking.RecordPatterns
translateCopatternClausesAgda.Syntax.Abstract.Copatterns
translateDefnAgda.Compiler.Epic.FromAgda
translateRecordPatternsAgda.TypeChecking.RecordPatterns
translateSplitTreeAgda.TypeChecking.RecordPatterns
transposeAgda.Termination.SparseMatrix
TravAgda.Auto.NarrowingSearch
traverseAgda.Auto.NarrowingSearch
traversePiAgda.Auto.Typecheck
traverseTermAgda.Syntax.Internal.Generic
traverseTermMAgda.Syntax.Internal.Generic
traverseWithKeyAgda.Utils.HashMap
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
trueConditionAgda.TypeChecking.MetaVars
tryOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
trySizeUnivAgda.TypeChecking.SizedTypes
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
TypeChecksAgda.Interaction.Highlighting.Precise
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
typeDontCareAgda.Syntax.Internal
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
typeFromProblemAgda.TypeChecking.Rules.LHS.ProblemRest
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
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
unAppViewAgda.Syntax.Abstract.Views
unArgAgda.Syntax.Common
UnBlockAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unblockedTesterAgda.TypeChecking.MetaVars
unCommandMAgda.Interaction.InteractionTop
unConNameAgda.TypeChecking.Test.Generators
unconsAgda.Utils.List
uncurry3Agda.Utils.Tuple
uncurry4Agda.Utils.Tuple
unDeepSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
undefAgda.Compiler.JS.Parser
UndefinedAgda.Compiler.JS.Syntax
unDefNameAgda.TypeChecking.Test.Generators
underAbsAgda.TypeChecking.Substitute
underAbstractionAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
underAbstraction_Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
UnderInfAgda.TypeChecking.Positivity
underLambdasAgda.TypeChecking.Substitute
Underscore 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
underscoreAgda.Syntax.Concrete.Pretty
UndoAgda.Auto.NarrowingSearch
unDomAgda.Syntax.Common
unElAgda.Syntax.Internal
unequalAgda.Auto.Typecheck
UnequalBecauseOfUniverseConflictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
UnfoldStrategyAgda.TypeChecking.MetaVars.Occurs
unfreezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unGraphAgda.Utils.Graph
unguardedRecordAgda.TypeChecking.Records
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
unifyPointersAgda.TypeChecking.Conversion
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.HashMap
3 (Function)Agda.Utils.Trie
4 (Function)Agda.Termination.CallGraph
5 (Function)Agda.Utils.Graph
6 (Function)Agda.Compiler.JS.Substitution
unionConstraintsAgda.Compiler.Epic.Injection
unions 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.HashMap
3 (Function)Agda.Utils.Graph
unionSignaturesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
unionWithAgda.Utils.HashMap
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
UnknownNamesInFixityDeclAgda.Syntax.Concrete.Definitions
UnknownSortAgda.Auto.Syntax
unlessMAgda.Utils.Monad
unless_Agda.Utils.Monad
unLevelAgda.TypeChecking.Level
unLevelAtomAgda.TypeChecking.Substitute
unlistenToMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unLvlAgda.TypeChecking.Primitive
unMaxViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
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
UnsolvedConstraintAgda.Interaction.Highlighting.Precise
UnsolvedConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedConstraintsAgda.TypeChecking.Errors
UnsolvedMetaAgda.Interaction.Highlighting.Precise
UnsolvedMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedMetaVariablesAgda.TypeChecking.Errors
unStrAgda.TypeChecking.Primitive
unTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unUnifyAgda.TypeChecking.Rules.LHS.Unify
unusableRelevanceAgda.TypeChecking.Irrelevance
Unused 
1 (Data Constructor)Agda.TypeChecking.Free
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnusedArgAgda.Syntax.Common
UnusedVariableInPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unusedVarsAgda.TypeChecking.Free
unVarNameAgda.TypeChecking.Test.Generators
unwrapAgda.Compiler.MAlonzo.Pretty
unYesTypeAgda.TypeChecking.Test.Generators
unzipAgda.Utils.Map
unzip3Agda.Utils.Map
unzipMaybeAgda.Utils.Maybe
updateDefArgOccurrencesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateDefCompiledRepAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateDefinitionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateDefPolarityAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateDefTypeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateLastAgda.Utils.List
updateMetaAgda.TypeChecking.MetaVars
updateMetaVarAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateMetaVarRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateNamedArgAgda.Syntax.Common
updateProblemRestAgda.TypeChecking.Rules.LHS.ProblemRest
updateProblemRest_Agda.TypeChecking.Rules.LHS.ProblemRest
updatePtrAgda.Utils.Pointer, Agda.Syntax.Internal
updatePtrMAgda.Utils.Pointer, Agda.Syntax.Internal
updateSharedAgda.Syntax.Internal
updateSharedFMAgda.Syntax.Internal
updateSharedMAgda.Syntax.Internal
updateSharedTermAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateSharedTermFAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateSharedTermTAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateTheDefAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ureadIORefAgda.Auto.NarrowingSearch
ureadmodifyIORefAgda.Auto.NarrowingSearch
UReduceAgda.TypeChecking.Rules.LHS.Unify
ureduceAgda.TypeChecking.Rules.LHS.Unify
usageAgda.Interaction.Options
UseBoundNames 
1 (Type/Class)Agda.Syntax.Concrete.Operators
2 (Data Constructor)Agda.Syntax.Concrete.Operators
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.ProblemRest
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
validConPatternAgda.Syntax.Concrete.Operators
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.Syntax.Internal
VarArgAgda.TypeChecking.Positivity
VarElimAgda.TypeChecking.Eliminators
varFreqAgda.TypeChecking.Test.Generators
VariableIsIrrelevantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
variantAgda.Utils.QuickCheck
varMAgda.TypeChecking.Primitive
VarMPAgda.TypeChecking.Coverage.Match
VarName 
1 (Data Constructor)Agda.Syntax.Scope.Monad
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
varsAgda.TypeChecking.Positivity
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
Warnings 
1 (Type/Class)Agda.TypeChecking.Errors
2 (Data Constructor)Agda.TypeChecking.Errors
warningsToErrorAgda.TypeChecking.Errors
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
whenJustAgda.Utils.Monad
whenJustMAgda.Utils.Monad
whenMAgda.Utils.Monad
when_Agda.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
WithArity 
1 (Type/Class)Agda.TypeChecking.CompiledClause
2 (Data Constructor)Agda.TypeChecking.CompiledClause
WithClausePatternMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
withConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
withContextPrecedenceAgda.Syntax.Scope.Monad
withCurrentModule 
1 (Function)Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
2 (Function)Agda.Syntax.Scope.Monad
withCurrentModule'Agda.Syntax.Scope.Monad
withDisplayFormAgda.TypeChecking.With
withEnvAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
WithExprAgda.Syntax.Concrete
withExtendedOccEnvAgda.TypeChecking.Positivity
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
withIncreasedModuleNestingLevelAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
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
withMetaIdAgda.Interaction.BasicOps
withMetaInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
withMetaInfo'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
withRangeOfAgda.Syntax.Position
withRangesOfAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
withRangesOfQAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
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
withShowAllArgumentsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
withSignatureAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
withTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
withTypesFromAgda.TypeChecking.Rules.LHS.Split
WkAgda.TypeChecking.Substitute
wkSAgda.TypeChecking.Substitute
wordBoundaryAgda.Compiler.JS.Parser
wordsByAgda.Utils.List
workOnTypesAgda.TypeChecking.Irrelevance
workOnTypes'Agda.TypeChecking.Irrelevance
Wrap 
1 (Type/Class)Agda.Compiler.MAlonzo.Pretty
2 (Data Constructor)Agda.Compiler.MAlonzo.Pretty
writeFileAgda.Utils.IO.UTF8
writeInterfaceAgda.Interaction.Imports
writeModule 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
WrongDefinitionAgda.Syntax.Concrete.Definitions
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
WrongParametersAgda.Syntax.Concrete.Definitions
WSMAgda.Syntax.Scope.Monad
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
YesAboveAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
YesBelowAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
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
zipBlockingVarsAgda.TypeChecking.Coverage.Match
zipNameSpaceAgda.Syntax.Scope.Base
zipScopeAgda.Syntax.Scope.Base
zipScope_Agda.Syntax.Scope.Base
zipWithAgda.Termination.Matrix
zipWith'Agda.Utils.List
zipWithM'Agda.Utils.Monad
zipWithTailsAgda.Utils.List
|->Agda.TypeChecking.Rules.LHS.Unify
||-Agda.Compiler.Epic.Erasure