A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
$
%
&
+
.
/
<
=
>
^
|
-
_
All

Index - T

Tactic	Agda.Syntax.Concrete
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
TagEq	Agda.Compiler.Epic.Injection
Tagged	Agda.Compiler.JS.Case
Tags
1 (Type/Class)	Agda.Compiler.Epic.Injection
2 (Data Constructor)	Agda.Compiler.Epic.Injection
tags	Agda.Compiler.JS.Case
takeAwakeConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
takeEqualities	Agda.TypeChecking.Rules.LHS.Unify
takeI	Agda.Syntax.Position
takeP	Agda.Utils.Permutation
takeRelevant	Agda.TypeChecking.MetaVars.Occurs
takeTele	Agda.Compiler.Epic.Forcing
takeWhileJust	Agda.Utils.List
tallyDef	Agda.TypeChecking.MetaVars.Occurs
Target	Agda.Termination.Monad
target	Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
targetNodes
1 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)	Agda.Termination.CallGraph
TBind
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
tcargs	Agda.Auto.Typecheck
tcConstructorNames	Agda.TypeChecking.Test.Generators
tcDefinedNames	Agda.TypeChecking.Test.Generators
TCEnv
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCErr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcErrString	Agda.TypeChecking.Errors
tcExp	Agda.Auto.Typecheck
tcFixSize	Agda.TypeChecking.Test.Generators
tcFreeVariables	Agda.TypeChecking.Test.Generators
tcFrequencies	Agda.TypeChecking.Test.Generators
tcIsType	Agda.TypeChecking.Test.Generators
tcLiterals	Agda.TypeChecking.Test.Generators
TCM
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcProjectionNames	Agda.TypeChecking.Test.Generators
tcSearch	Agda.Auto.Typecheck
TCSt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Tel
1 (Type/Class)	Agda.Syntax.Concrete.Pretty
2 (Data Constructor)	Agda.Syntax.Concrete.Pretty
TelCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Tele	Agda.Syntax.Internal
teleArgNames	Agda.TypeChecking.Telescope
teleArgs	Agda.TypeChecking.Telescope
teleLam	Agda.TypeChecking.Substitute
teleNames	Agda.TypeChecking.Telescope
TeleNoAbs	Agda.TypeChecking.Substitute
teleNoAbs	Agda.TypeChecking.Substitute
telePi	Agda.TypeChecking.Substitute
telePi'	Agda.TypeChecking.Substitute
telePi_	Agda.TypeChecking.Substitute
Telescope
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
3 (Type/Class)	Agda.Syntax.Internal
telFromList	Agda.TypeChecking.Substitute
telFromList'	Agda.TypeChecking.Substitute
TelHH	Agda.TypeChecking.Rules.LHS.Unify
tellDirty	Agda.Utils.Update
tellEmacsToJumpToError	Agda.Interaction.InteractionTop
tellEq	Agda.TypeChecking.Rewriting.NonLinMatch
tellSub	Agda.TypeChecking.Rewriting.NonLinMatch
tellToUpdateHighlighting	Agda.Interaction.InteractionTop
telToArgs	Agda.TypeChecking.Substitute
telToList	Agda.TypeChecking.Substitute
TelV
1 (Type/Class)	Agda.TypeChecking.Substitute
2 (Data Constructor)	Agda.TypeChecking.Substitute
telVars	Agda.TypeChecking.Substitute
TelView	Agda.TypeChecking.Substitute
telView	Agda.TypeChecking.Telescope
telView'	Agda.TypeChecking.Substitute
TelViewHH	Agda.TypeChecking.Rules.LHS.Unify
telViewUpTo	Agda.TypeChecking.Telescope
telViewUpTo'	Agda.TypeChecking.Telescope
telViewUpToHH	Agda.TypeChecking.Rules.LHS.Unify
TempInstanceTable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
terAsk	Agda.Termination.Monad
terAsks	Agda.Termination.Monad
terCurrent	Agda.Termination.Monad
terCutOff	Agda.Termination.Monad
terDelayed	Agda.Termination.Monad
TerEnv
1 (Type/Class)	Agda.Termination.Monad
2 (Data Constructor)	Agda.Termination.Monad
terGetCurrent	Agda.Termination.Monad
terGetCutOff	Agda.Termination.Monad
terGetDelayed	Agda.Termination.Monad
terGetGuarded	Agda.Termination.Monad
terGetGuardingTypeConstructors	Agda.Termination.Monad
terGetInlineWithFunctions	Agda.Termination.Monad
terGetMaskArgs	Agda.Termination.Monad
terGetMaskResult	Agda.Termination.Monad
terGetMutual	Agda.Termination.Monad
terGetPatterns	Agda.Termination.Monad
terGetSharp	Agda.Termination.Monad
terGetSizeSuc	Agda.Termination.Monad
terGetTarget	Agda.Termination.Monad
terGetUsableVars	Agda.Termination.Monad
terGetUseDotPatterns	Agda.Termination.Monad
terGetUserNames	Agda.Termination.Monad
terGetUseSizeLt	Agda.Termination.Monad
terGuarded	Agda.Termination.Monad
terGuardingTypeConstructors	Agda.Termination.Monad
terInlineWithFunctions	Agda.Termination.Monad
terLocal	Agda.Termination.Monad
TerM
1 (Type/Class)	Agda.Termination.Monad
2 (Data Constructor)	Agda.Termination.Monad
Term
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
3 (Type/Class)	Agda.Syntax.Internal
terM	Agda.Termination.Monad
term
1 (Function)	Agda.Compiler.JS.Compiler
2 (Function)	Agda.Compiler.MAlonzo.Compiler
term'	Agda.Compiler.MAlonzo.Compiler
terMaskArgs	Agda.Termination.Monad
terMaskResult	Agda.Termination.Monad
TermConf	Agda.TypeChecking.Test.Generators
TermConfiguration	Agda.TypeChecking.Test.Generators
TermDBP	Agda.Termination.Monad
termDecl	Agda.Termination.TermCheck
termErrCalls	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
termErrFunctions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermFreqs
1 (Type/Class)	Agda.TypeChecking.Test.Generators
2 (Data Constructor)	Agda.TypeChecking.Test.Generators
termFreqs	Agda.TypeChecking.Test.Generators
TermHead	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermHH	Agda.TypeChecking.Rules.LHS.Unify
terminates	Agda.Termination.Termination
terminatesFilter	Agda.Termination.Termination
Terminating	Agda.Syntax.Common
Termination	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TerminationCheck
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
TerminationCheckFailed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TerminationCheckPragma	Agda.Syntax.Concrete
TerminationError
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TerminationMeasure	Agda.Syntax.Common
TerminationProblem	Agda.Interaction.Highlighting.Precise
TermLike	Agda.Syntax.Internal.Generic
terModifyGuarded	Agda.Termination.Monad
terModifyUsableVars	Agda.Termination.Monad
terModifyUseSizeLt	Agda.Termination.Monad
TermSize	Agda.Syntax.Internal
termSize	Agda.Syntax.Internal
terMutual	Agda.Termination.Monad
terPatterns	Agda.Termination.Monad
terPatternsRaise	Agda.Termination.Monad
terPiGuarded	Agda.Termination.Monad
terRaise	Agda.Termination.Monad
terSetCurrent	Agda.Termination.Monad
terSetDelayed	Agda.Termination.Monad
terSetGuarded	Agda.Termination.Monad
terSetMaskArgs	Agda.Termination.Monad
terSetMaskResult	Agda.Termination.Monad
terSetPatterns	Agda.Termination.Monad
terSetSizeDepth	Agda.Termination.Monad
terSetTarget	Agda.Termination.Monad
terSetUsableVars	Agda.Termination.Monad
terSetUseDotPatterns	Agda.Termination.Monad
terSetUseSizeLt	Agda.Termination.Monad
terSharp	Agda.Termination.Monad
terSizeDepth	Agda.Termination.Monad
terSizeSuc	Agda.Termination.Monad
terTarget	Agda.Termination.Monad
terUnguarded	Agda.Termination.Monad
terUsableVars	Agda.Termination.Monad
terUseDotPatterns	Agda.Termination.Monad
terUserNames	Agda.Termination.Monad
terUseSizeLt	Agda.Termination.Monad
Testable	Agda.Utils.QuickCheck
testChar	Agda.Utils.Char
testLub	Agda.TypeChecking.SizedTypes.WarshallSolver
tests
1 (Function)	Agda.Utils.Cluster
2 (Function)	Agda.Utils.BiMap
3 (Function)	Agda.Utils.Either
4 (Function)	Agda.Termination.Semiring
5 (Function)	Agda.Utils.PartialOrd
6 (Function)	Agda.Utils.Bag
7 (Function)	Agda.Utils.List
8 (Function)	Agda.Utils.FileName, Agda.Interaction.FindFile
9 (Function)	Agda.Utils.Favorites
10 (Function)	Agda.TypeChecking.SizedTypes.Tests
11 (Function)	Agda.Interaction.Options
12 (Function)	Agda.Termination.SparseMatrix
13 (Function)	Agda.Termination.Order
14 (Function)	Agda.Termination.CallMatrix
15 (Function)	Agda.Termination.CallGraph
16 (Function)	Agda.Termination.Termination
17 (Function)	Agda.Utils.ListT.Tests
18 (Function)	Agda.Syntax.Position
19 (Function)	Agda.Utils.Warshall
20 (Function)	Agda.Interaction.Highlighting.Range
21 (Function)	Agda.Interaction.Highlighting.Precise
22 (Function)	Agda.Syntax.Parser.Parser
23 (Function)	Agda.TypeChecking.Positivity.Occurrence
24 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional.Tests
25 (Function)	Agda.TypeChecking.Free.Tests
26 (Function)	Agda.Compiler.MAlonzo.Encode
27 (Function)	Agda.TypeChecking.Irrelevance
28 (Function)	Agda.Interaction.Highlighting.Emacs
29 (Function)	Agda.TypeChecking.Positivity.Tests
30 (Function)	Agda.TypeChecking.Tests
31 (Function)	Agda.Utils.Permutation.Tests
32 (Function)	Agda.Interaction.Highlighting.Generate
testSplitTreePrinting	Agda.TypeChecking.Coverage.SplitTree
testSuccs	Agda.TypeChecking.SizedTypes.WarshallSolver
testSuite	Agda.Tests
text
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
tgtNodes	Agda.Utils.Graph.AdjacencyMap.Unidirectional
thd3	Agda.Utils.Tuple
theBenchmark	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
theBlockingMeta	Agda.Syntax.Internal
theCallGraph	Agda.Termination.CallGraph
theConstraint	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theCore	Agda.TypeChecking.Substitute
theCurrentFile	Agda.Interaction.InteractionTop
theDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theException	Agda.Utils.QuickCheck
theFixity	Agda.Syntax.Fixity
theInteractionPoints	Agda.Interaction.InteractionTop
theNotation	Agda.Syntax.Fixity
thenTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theSize	Agda.Utils.Size
theTel	Agda.TypeChecking.Substitute
ThingsInScope	Agda.Syntax.Scope.Base
thingsInScope	Agda.Syntax.Scope.Base
ThingWithFixity
1 (Type/Class)	Agda.Syntax.Fixity, Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Fixity, Agda.Syntax.Concrete
thread	Agda.Utils.Monad
three	Agda.Utils.TestHelpers
throwError	Agda.Utils.Except
throwException	Agda.TypeChecking.Monad.Exception
throwImpossible	Agda.Utils.Impossible
tick	Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
tickMax	Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
tickN	Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
Timings	Agda.Utils.Benchmark
timings	Agda.Utils.Benchmark
TLet
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
tlmname	Agda.Compiler.MAlonzo.Misc
tlmodOf	Agda.Compiler.MAlonzo.Misc
TMAll	Agda.Auto.Convert
TMode	Agda.Auto.Convert
to	Agda.Interaction.Highlighting.Range
ToAbstract	Agda.Syntax.Translation.ConcreteToAbstract
toAbstract	Agda.Syntax.Translation.ConcreteToAbstract
toAscList
1 (Function)	Agda.Utils.Bag
2 (Function)	Agda.Utils.Trie
ToConcrete	Agda.Syntax.Translation.AbstractToConcrete
toConcrete	Agda.Syntax.Translation.AbstractToConcrete
toConcreteCtx	Agda.Syntax.Translation.AbstractToConcrete
toDescList	Agda.Utils.VarSet
ToggleImplicitArgs	Agda.Interaction.InteractionTop
toIFile	Agda.Interaction.FindFile
TokComment	Agda.Syntax.Parser.Tokens
TokDummy	Agda.Syntax.Parser.Tokens
Token	Agda.Syntax.Parser.Tokens
token
1 (Function)	Agda.Compiler.JS.Parser
2 (Function)	Agda.Syntax.Parser.LexActions
TokenLength	Agda.Syntax.Parser.Alex
tokensParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser
tokenStream	Agda.Interaction.Highlighting.HTML
TokEOF	Agda.Syntax.Parser.Tokens
TokId	Agda.Syntax.Parser.Tokens
TokKeyword	Agda.Syntax.Parser.Tokens
TokLiteral	Agda.Syntax.Parser.Tokens
TokQId	Agda.Syntax.Parser.Tokens
TokSetN	Agda.Syntax.Parser.Tokens
TokString	Agda.Syntax.Parser.Tokens
TokSymbol	Agda.Syntax.Parser.Tokens
TokTeX	Agda.Syntax.Parser.Tokens
toLazy	Agda.Utils.Maybe.Strict
toList
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.BiMap
3 (Function)	Agda.Utils.HashMap
4 (Function)	Agda.Utils.Bag
5 (Function)	Agda.Utils.Favorites
6 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
7 (Function)	Agda.Utils.Trie
8 (Function)	Agda.Termination.CallMatrix
9 (Function)	Agda.Termination.CallGraph
toLists	Agda.Termination.SparseMatrix
TOM	Agda.Auto.Convert
toMap	Agda.Interaction.Highlighting.Precise
tomy	Agda.Auto.Convert
tomyBody	Agda.Auto.Convert
tomyClause	Agda.Auto.Convert
tomyClauses	Agda.Auto.Convert
tomyExp	Agda.Auto.Convert
tomyExps	Agda.Auto.Convert
tomyIneq	Agda.Auto.Convert
tomyPat	Agda.Auto.Convert
tomyType	Agda.Auto.Convert
TooFewArgumentsToPatternSynonym	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooFewFields	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooManyArgumentsInLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooManyFields	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
toOrderings	Agda.Utils.PartialOrd
Top
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Utils
2 (Data Constructor)	Agda.TypeChecking.MetaVars.Occurs
top	Agda.TypeChecking.SizedTypes.Utils
topBindings	Agda.Compiler.Epic.CompileState
topContext	Agda.Syntax.Parser.Monad
TopCtx	Agda.Syntax.Fixity
TopLevel
1 (Type/Class)	Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)	Agda.Syntax.Translation.ConcreteToAbstract
topLevel	Agda.Compiler.JS.Parser
topLevelDecls	Agda.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
topLevelPath	Agda.Syntax.Translation.ConcreteToAbstract
topLevelTheThing	Agda.Syntax.Translation.ConcreteToAbstract
topoSort	Agda.Utils.Permutation
topSearch	Agda.Auto.NarrowingSearch
topSort	Agda.Syntax.Internal
topVarOcc	Agda.TypeChecking.Free.Lazy
toStrict	Agda.Utils.Maybe.Strict
toSubscriptDigit	Agda.Utils.Suffix
ToTerm	Agda.TypeChecking.Primitive
toTerm	Agda.TypeChecking.Primitive
toTermR	Agda.TypeChecking.Primitive
toTopLevelModuleName
1 (Function)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)	Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
toTree	Agda.TypeChecking.Coverage.SplitTree
toTrees	Agda.TypeChecking.Coverage.SplitTree
toVim	Agda.Interaction.Highlighting.Vim
toWeight	Agda.TypeChecking.SizedTypes.WarshallSolver
trace	Agda.TypeChecking.SizedTypes.Utils
traceCall	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallCPS	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallCPS_	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceCallE	Agda.TypeChecking.Rules.Term
traceCallM	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceM	Agda.TypeChecking.SizedTypes.Utils
traceSDoc	Agda.TypeChecking.Reduce.Monad
traceSDocNLM	Agda.TypeChecking.Rewriting.NonLinMatch
traceSLn	Agda.TypeChecking.Reduce.Monad
trampoline	Agda.Utils.Function
trampolineM	Agda.Utils.Function
trampolineWhile	Agda.Utils.Function
trampolineWhileM	Agda.Utils.Function
transClos	Agda.TypeChecking.SizedTypes.WarshallSolver
translateCase	Agda.Compiler.Epic.Primitive
translateCompiledClauses	Agda.TypeChecking.RecordPatterns
translateCopatternClauses	Agda.Syntax.Abstract.Copatterns
translateDefn	Agda.Compiler.Epic.FromAgda
translateRecordPatterns	Agda.TypeChecking.RecordPatterns
translateSplitTree	Agda.TypeChecking.RecordPatterns
transpose	Agda.Termination.SparseMatrix
transposeEdge	Agda.Utils.Graph.AdjacencyMap.Unidirectional
Trav	Agda.Auto.NarrowingSearch
trav	Agda.Auto.NarrowingSearch
traverse'	Agda.Utils.Bag
traverseEither	Agda.Utils.Either
traverseExpr
1 (Function)	Agda.Syntax.Concrete.Generic
2 (Function)	Agda.Syntax.Abstract.Views
traverseF	Agda.Utils.Functor
traversePi	Agda.Auto.Typecheck
traverseTerm	Agda.Syntax.Internal.Generic
traverseTermM	Agda.Syntax.Internal.Generic
traverseWithKey	Agda.Utils.HashMap
TrBr
1 (Type/Class)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Auto.Syntax
treatAbstractly	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
treatAbstractly'	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
Trie	Agda.Utils.Trie
trim	Agda.Utils.String
trivial	Agda.TypeChecking.SizedTypes
trivialHH	Agda.TypeChecking.Rules.LHS.Unify
trueCondition	Agda.TypeChecking.MetaVars
TruncateOffset	Agda.TypeChecking.SizedTypes.Syntax
truncateOffset	Agda.TypeChecking.SizedTypes.Syntax
tryConversion	Agda.TypeChecking.Conversion
tryConversion'	Agda.TypeChecking.Conversion
tryHom	Agda.TypeChecking.Rules.LHS.Unify
tryOpen	Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
tryRecordType	Agda.TypeChecking.Records
trySizeUniv	Agda.TypeChecking.SizedTypes
tset	Agda.TypeChecking.Primitive
tSetOmega	Agda.TypeChecking.Primitive
tsize	Agda.Syntax.Internal
tSizeUniv	Agda.TypeChecking.Primitive
tvaldecl	Agda.Compiler.MAlonzo.Compiler
two	Agda.Utils.TestHelpers
Type
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Internal
3 (Type/Class)	Agda.Syntax.Internal
Type'	Agda.Syntax.Internal
TypeCheckingProblem	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
typeCheckMain	Agda.Interaction.Imports
TypeChecks	Agda.Interaction.Highlighting.Precise
TypeCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TypedAssign	Agda.Interaction.BasicOps
TypedBinding
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
TypedBinding'	Agda.Syntax.Concrete
TypedBindings
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Concrete
3 (Type/Class)	Agda.Syntax.Abstract
4 (Data Constructor)	Agda.Syntax.Abstract
TypedBindings'	Agda.Syntax.Concrete
typeDontCare	Agda.Syntax.Internal
TypeError
1 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
typeError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
typeError_	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TypeHH	Agda.TypeChecking.Rules.LHS.Unify
typeIn	Agda.Interaction.CommandLine
typeInCurrent	Agda.Interaction.BasicOps
typeInMeta	Agda.Interaction.BasicOps
typeInType	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
typeName	Agda.TypeChecking.Level
typeOf	Agda.Interaction.CommandLine
typeOfBV	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
typeOfBV'	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
typeOfConst	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
typeOfFlat	Agda.TypeChecking.Rules.Builtin.Coinduction
typeOfInf	Agda.TypeChecking.Rules.Builtin.Coinduction
typeOfMeta	Agda.Interaction.BasicOps
typeOfMeta'	Agda.Interaction.BasicOps
typeOfMetaMI	Agda.Interaction.BasicOps
typeOfSharp	Agda.TypeChecking.Rules.Builtin.Coinduction
TypeSig	Agda.Syntax.Concrete
TypeSignature
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
TypeSignatureOrInstanceBlock	Agda.Syntax.Concrete
typesOfHiddenMetas	Agda.Interaction.BasicOps
typesOfVisibleMetas	Agda.Interaction.BasicOps
Typing	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark