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

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
takenNameStr	Agda.Interaction.InteractionTop
takeP	Agda.Utils.Permutation
takeRelevant	Agda.TypeChecking.MetaVars.Occurs
takeTele	Agda.Compiler.Epic.Forcing
tallyDef	Agda.TypeChecking.MetaVars.Occurs
target	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
tcSearch	Agda.Auto.Typecheck
TCSt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TCState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
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
TelHH	Agda.TypeChecking.Rules.LHS.Unify
tellEmacsToJumpToError	Agda.Interaction.InteractionTop
tellToUpdateHighlighting	Agda.Interaction.InteractionTop
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
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
TermConf	Agda.TypeChecking.Test.Generators
TermConfiguration	Agda.TypeChecking.Test.Generators
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
TerminationCheckFailed	Agda.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
TerminationProblem	Agda.Interaction.Highlighting.Precise
terminationProblems	Agda.TypeChecking.Errors
TermLike	Agda.Syntax.Internal.Generic
Testable	Agda.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
testSplitTreePrinting	Agda.TypeChecking.Coverage.SplitTree
testSuite	Agda.Tests
text
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
TextDetails	Agda.Utils.Pretty
thd3	Agda.Utils.Tuple
theConstraint	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theCurrentFile	Agda.Interaction.InteractionTop
theDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theFixity	Agda.Syntax.Fixity
theInteractionPoints	Agda.Interaction.InteractionTop
theNotation	Agda.Syntax.Fixity
thenTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
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
tlmname	Agda.Compiler.MAlonzo.Misc
tlmodOf	Agda.Compiler.MAlonzo.Misc
TMAll	Agda.Auto.Convert
TMode	Agda.Auto.Convert
TNoBind
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
to	Agda.Interaction.Highlighting.Range
ToAbstract	Agda.Syntax.Translation.ConcreteToAbstract
toAbstract	Agda.Syntax.Translation.ConcreteToAbstract
ToConcrete	Agda.Syntax.Translation.AbstractToConcrete
toConcrete	Agda.Syntax.Translation.AbstractToConcrete
toConcreteCtx	Agda.Syntax.Translation.AbstractToConcrete
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
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
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
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
TooFewFields	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooManyArgumentsInLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TooManyFields	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Top	Agda.TypeChecking.MetaVars.Occurs
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
topoSort	Agda.Utils.Permutation
topSearch	Agda.Auto.NarrowingSearch
topSort	Agda.Syntax.Internal
toSubscriptDigit	Agda.Utils.Suffix
ToTerm	Agda.TypeChecking.Primitive
toTerm	Agda.TypeChecking.Primitive
toTopLevelModuleName
1 (Function)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
toTree	Agda.TypeChecking.Coverage.SplitTree
toTrees	Agda.TypeChecking.Coverage.SplitTree
toVim	Agda.Interaction.Highlighting.Vim
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
traceCall_	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceFun	Agda.TypeChecking.Reduce
traceFun'	Agda.TypeChecking.Reduce
trailingImplicits	Agda.TypeChecking.Rules.Def
transitiveClosure	Agda.Utils.Graph
transitiveClosure1	Agda.Utils.Graph
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
Trav	Agda.Auto.NarrowingSearch
traverse	Agda.Auto.NarrowingSearch
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
trivial	Agda.TypeChecking.SizedTypes
trivialHH	Agda.TypeChecking.Rules.LHS.Unify
trueCondition	Agda.TypeChecking.MetaVars
tryOpen	Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
trySizeUniv	Agda.TypeChecking.SizedTypes
tset	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
typeCheck	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
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
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
typeFromProblem	Agda.TypeChecking.Rules.LHS.ProblemRest
TypeHH	Agda.TypeChecking.Rules.LHS.Unify
typeIn	Agda.Interaction.CommandLine.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.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
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
typesOfHiddenMetas	Agda.Interaction.BasicOps
typesOfVisibleMetas	Agda.Interaction.BasicOps