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

TACon	Agda.Syntax.Treeless
Tactic
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
Tag
1 (Type/Class)	Agda.Compiler.Epic.Interface
2 (Data Constructor)	Agda.Compiler.Epic.Interface
TagEq	Agda.Compiler.Epic.Injection
Tags
1 (Type/Class)	Agda.Compiler.Epic.Injection
2 (Data Constructor)	Agda.Compiler.Epic.Injection
TAGuard	Agda.Syntax.Treeless
takeAwakeConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
takeI	Agda.Syntax.Position
takeP	Agda.Utils.Permutation
takeRelevant	Agda.TypeChecking.MetaVars.Occurs
takeTele	Agda.Compiler.Epic.Forcing
takeWhileJust	Agda.Utils.List
TALit	Agda.Syntax.Treeless
tallyDef	Agda.TypeChecking.MetaVars.Occurs
TAlt	Agda.Syntax.Treeless
TApp	Agda.Syntax.Treeless
tAppView	Agda.Syntax.Treeless
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
TCase	Agda.Syntax.Treeless
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
tcErrClosErr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcErrState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcErrString	Agda.TypeChecking.Errors
tcExp	Agda.Auto.Typecheck
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
TCon	Agda.Syntax.Treeless
tcSearch	Agda.Auto.Typecheck
TCSt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCWarning
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcWarning	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcWarningClosure	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcWarningState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
tcWarningsToError	Agda.TypeChecking.Errors
TDef	Agda.Syntax.Treeless
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
tele2NamedArgs	Agda.TypeChecking.Telescope
teleArgNames	Agda.TypeChecking.Telescope
teleArgs	Agda.TypeChecking.Telescope
teleLam	Agda.TypeChecking.Substitute
teleNamedArgs	Agda.TypeChecking.Telescope
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.Internal
3 (Type/Class)	Agda.Syntax.Abstract
telFromList	Agda.TypeChecking.Substitute
telFromList'	Agda.TypeChecking.Substitute
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
telView'UpTo	Agda.TypeChecking.Substitute
telViewUpTo	Agda.TypeChecking.Telescope
telViewUpTo'	Agda.TypeChecking.Telescope
TempInstanceTable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TErased	Agda.Syntax.Treeless
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.Syntax.Reflected
2 (Type/Class)	Agda.Syntax.Internal
3 (Type/Class)	Agda.Auto.NarrowingSearch
4 (Data Constructor)	Agda.Auto.NarrowingSearch
terM	Agda.Termination.Monad
term	Agda.Compiler.MAlonzo.Compiler
terMaskArgs	Agda.Termination.Monad
terMaskResult	Agda.Termination.Monad
termC	Agda.TypeChecking.Serialise.Base
termD	Agda.TypeChecking.Serialise.Base
TermDBP	Agda.Termination.Monad
termDecl	Agda.Termination.TermCheck
termErrCalls	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
termErrFunctions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermHead	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
TerminationIssue	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TerminationMeasure	Agda.Syntax.Common
TerminationProblem	Agda.Interaction.Highlighting.Precise
TermLike	Agda.Syntax.Internal.Generic
termMutual	Agda.Termination.TermCheck
terModifyGuarded	Agda.Termination.Monad
terModifyUsableVars	Agda.Termination.Monad
terModifyUseSizeLt	Agda.Termination.Monad
TermPart	Agda.TypeChecking.Unquote
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
TError
1 (Type/Class)	Agda.Syntax.Treeless
2 (Data Constructor)	Agda.Syntax.Treeless
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
testChar	Agda.Utils.Char
testLub	Agda.TypeChecking.SizedTypes.WarshallSolver
testSuccs	Agda.TypeChecking.SizedTypes.WarshallSolver
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
theDefLens	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theFixity	Agda.Syntax.Fixity
theInteractionPoints	Agda.Interaction.InteractionTop
theNameRange	Agda.Syntax.Fixity
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
throwError	Agda.Utils.Except
throwException	Agda.TypeChecking.Monad.Exception
throwImpossible	Agda.Utils.Impossible
tick	Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
tickICode	Agda.TypeChecking.Serialise.Base
tickMax	Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
tickN	Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
tIfThenElse	Agda.Syntax.Treeless
Timings	Agda.Utils.Benchmark
timings	Agda.Utils.Benchmark
tInt	Agda.Syntax.Treeless
TLam	Agda.Syntax.Treeless
tLamView	Agda.Syntax.Treeless
TLet
1 (Data Constructor)	Agda.Syntax.Treeless
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Syntax.Abstract
tLetView	Agda.Syntax.Treeless
TLit	Agda.Syntax.Treeless
tlmodOf	Agda.Compiler.MAlonzo.Misc
TMAll	Agda.Auto.Convert
TMode	Agda.Auto.Convert
tNegPlusK	Agda.Syntax.Treeless
to	Agda.Interaction.Highlighting.Range
ToAbstract
1 (Type/Class)	Agda.Syntax.Translation.ReflectedToAbstract
2 (Type/Class)	Agda.Syntax.Translation.ConcreteToAbstract
toAbstract
1 (Function)	Agda.Syntax.Translation.ReflectedToAbstract
2 (Function)	Agda.Syntax.Translation.ConcreteToAbstract
toAbstractPats	Agda.Syntax.Translation.ReflectedToAbstract
toAbstractWithoutImplicit	Agda.Syntax.Translation.ReflectedToAbstract
toAbstract_	Agda.Syntax.Translation.ReflectedToAbstract
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
toConPatternInfo	Agda.Syntax.Internal
toDescList	Agda.Utils.VarSet
ToggleImplicitArgs	Agda.Interaction.InteractionTop
toIFile	Agda.Interaction.FindFile
tok
1 (Function)	Agda.Utils.Parser.MemoisedCPS
2 (Function)	Agda.Syntax.Concrete.Operators.Parser.Monad
TokComment	Agda.Syntax.Parser.Tokens
TokDummy	Agda.Syntax.Parser.Tokens
Token	Agda.Syntax.Parser.Tokens
token
1 (Function)	Agda.Utils.Parser.MemoisedCPS
2 (Function)	Agda.Syntax.Concrete.Operators.Parser.Monad
3 (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.HashMap
3 (Function)	Agda.Utils.BiMap
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
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
TooManyPolarities	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.Syntax.Treeless
top	Agda.TypeChecking.SizedTypes.Utils
topBindings	Agda.Compiler.Epic.CompileState
topContext	Agda.Syntax.Parser.Monad
TopCtx	Agda.Syntax.Fixity
TopK	Agda.Syntax.Concrete.Operators.Parser.Monad
TopLevel
1 (Type/Class)	Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)	Agda.Syntax.Translation.ConcreteToAbstract
topLevelDecls	Agda.Syntax.Translation.ConcreteToAbstract
topLevelExpectedName	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
3 (Function)	Agda.Compiler.Common
topLevelPath	Agda.Syntax.Translation.ConcreteToAbstract
topLevelScope	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
toSparseRows	Agda.Termination.SparseMatrix
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.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract
toTree	Agda.TypeChecking.Coverage.SplitTree
toTreeless	Agda.Compiler.ToTreeless
toTrees	Agda.TypeChecking.Coverage.SplitTree
toVim	Agda.Interaction.Highlighting.Vim
toWeight	Agda.TypeChecking.SizedTypes.WarshallSolver
tPlusK	Agda.Syntax.Treeless
TPrim
1 (Type/Class)	Agda.Syntax.Treeless
2 (Data Constructor)	Agda.Syntax.Treeless
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
transform
1 (Function)	Agda.Compiler.Treeless.DelayCoinduction
2 (Function)	Agda.Compiler.Treeless.EliminateLiteralPatterns
translateBuiltins	Agda.Compiler.Treeless.Builtin
translateCase	Agda.Compiler.Epic.Primitive
translateCompiledClauses	Agda.TypeChecking.RecordPatterns
translateCopatternClauses	Agda.Syntax.Abstract.Copatterns
translateDefn
1 (Function)	Agda.Compiler.Epic.FromAgda
2 (Function)	Agda.Compiler.UHC.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
treelessPrimName	Agda.Compiler.MAlonzo.Primitives
Trie	Agda.Utils.Trie
trim	Agda.Utils.String
trivial	Agda.TypeChecking.SizedTypes
trueCondition	Agda.TypeChecking.MetaVars
TruncateOffset	Agda.TypeChecking.SizedTypes.Syntax
truncateOffset	Agda.TypeChecking.SizedTypes.Syntax
tryConversion	Agda.TypeChecking.Conversion
tryConversion'	Agda.TypeChecking.Conversion
tryMaybe	Agda.Utils.Monad
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
TSort	Agda.Syntax.Treeless
TT	Agda.Compiler.UHC.FromAgda
TTEnv
1 (Type/Class)	Agda.Compiler.UHC.FromAgda
2 (Data Constructor)	Agda.Compiler.UHC.FromAgda
TTerm	Agda.Syntax.Treeless
TUnit	Agda.Syntax.Treeless
TUnreachable	Agda.Syntax.Treeless
tUnreachable	Agda.Syntax.Treeless
tvaldecl	Agda.Compiler.MAlonzo.Compiler
TVar	Agda.Syntax.Treeless
TyApp	Agda.Utils.Haskell.Syntax
TyCon	Agda.Utils.Haskell.Syntax
TyForall	Agda.Utils.Haskell.Syntax
TyFun	Agda.Utils.Haskell.Syntax
Type
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Type/Class)	Agda.Syntax.Reflected
3 (Data Constructor)	Agda.Syntax.Internal
4 (Type/Class)	Agda.Syntax.Internal
5 (Data Constructor)	Agda.Auto.Syntax
Type'	Agda.Syntax.Internal
typeCheck	Agda.Interaction.Imports
TypeCheckAction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
TypeDecl	Agda.Utils.Haskell.Syntax
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
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
1 (Function)	Agda.TypeChecking.Abstract
2 (Function)	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
1 (Data Constructor)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
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
TyVar	Agda.Utils.Haskell.Syntax
TyVarBind	Agda.Utils.Haskell.Syntax