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	Agda.Compiler.Epic.AuxAST
takeConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
takeEqualities	Agda.TypeChecking.Rules.LHS.Unify
takeI	Agda.Syntax.Position, Agda.Interaction.GhciTop
takenNameStr	Agda.Interaction.GhciTop
takeP	Agda.Utils.Permutation
takeTele	Agda.Compiler.Epic.Forcing
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
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, Agda.Interaction.GhciTop
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.Syntax.Internal
teleNames	Agda.TypeChecking.Telescope
telePi	Agda.TypeChecking.Substitute
telePi_	Agda.TypeChecking.Substitute
telePos	Agda.Compiler.Epic.Forcing
Telescope
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Internal
3 (Type/Class)	Agda.Syntax.Abstract
telFromList	Agda.Syntax.Internal
tellEmacsToJumpToError	Agda.Interaction.GhciTop
telToList	Agda.Syntax.Internal
TelV	Agda.TypeChecking.Substitute
telVars	Agda.TypeChecking.Substitute
TelView	Agda.TypeChecking.Substitute
telView	Agda.TypeChecking.Telescope
telView'	Agda.TypeChecking.Substitute
telViewM	Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
telViewUpTo	Agda.TypeChecking.Telescope
Term
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
3 (Type/Class)	Agda.Syntax.Internal
term	Agda.Compiler.MAlonzo.Compiler
term'	Agda.Compiler.MAlonzo.Compiler
TermConf	Agda.TypeChecking.Test.Generators
TermConfiguration	Agda.TypeChecking.Test.Generators
termDecls	Agda.Termination.TermCheck
TermFreqs
1 (Type/Class)	Agda.TypeChecking.Test.Generators
2 (Data Constructor)	Agda.TypeChecking.Test.Generators
termFreqs	Agda.TypeChecking.Test.Generators
TermFunDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TermHead	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
terminates	Agda.Termination.Termination
TerminationCheckFailed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
TerminationProblem	Agda.Interaction.Highlighting.Precise
terminationProblems	Agda.Interaction.Imports
TermLike	Agda.Syntax.Internal.Generic
Testable	Agda.Utils.QuickCheck
tests
1 (Function)	Agda.Utils.FileName, Agda.Interaction.FindFile
2 (Function)	Agda.Syntax.Position, Agda.Interaction.GhciTop
3 (Function)	Agda.Utils.List
4 (Function)	Agda.Interaction.Options
5 (Function)	Agda.Interaction.Highlighting.Range
6 (Function)	Agda.Interaction.Highlighting.Precise
7 (Function)	Agda.Syntax.Parser.Parser
8 (Function)	Agda.Termination.Semiring
9 (Function)	Agda.Termination.SparseMatrix
10 (Function)	Agda.Termination.CallGraph
11 (Function)	Agda.Termination.Matrix
12 (Function)	Agda.Utils.Either
13 (Function)	Agda.Termination.Lexicographic
14 (Function)	Agda.Termination.Termination
15 (Function)	Agda.Utils.Warshall
16 (Function)	Agda.TypeChecking.Tests
17 (Function)	Agda.Interaction.Highlighting.Generate
18 (Function)	Agda.Interaction.Highlighting.Emacs
19 (Function)	Agda.Compiler.MAlonzo.Encode
testSuite	Agda.Tests
text
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
TextDetails	Agda.Utils.Pretty
theCurrentFile	Agda.Interaction.GhciTop
theDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
theFixity	Agda.Syntax.Fixity
theInteractionPoints	Agda.Interaction.GhciTop
theNotation	Agda.Syntax.Fixity
theState	Agda.Interaction.GhciTop
theTCState	Agda.Interaction.GhciTop
theTelescope	Agda.Compiler.Epic.Forcing
ThingsInScope	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
thingsInScope	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
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
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, Agda.Interaction.GhciTop
toAbstract	Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
ToConcrete	Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
toConcrete	Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
toConcreteCtx	Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
toggleImplicitArgs	Agda.Interaction.GhciTop
toIFile	Agda.Interaction.FindFile
TokComment	Agda.Syntax.Parser.Tokens
TokDummy	Agda.Syntax.Parser.Tokens
Token	Agda.Syntax.Parser.Tokens
token	Agda.Syntax.Parser.LexActions
TokenLength	Agda.Syntax.Parser.Alex
tokensParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser, Agda.Interaction.GhciTop
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.Interaction.Highlighting.Range
2 (Function)	Agda.Termination.CallGraph
toLists
1 (Function)	Agda.Termination.SparseMatrix
2 (Function)	Agda.Termination.Matrix
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
topBindings	Agda.Compiler.Epic.CompileState
topContext	Agda.Syntax.Parser.Monad
TopCtx	Agda.Syntax.Fixity
TopLevel
1 (Type/Class)	Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)	Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
topLevelDecls	Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
TopLevelInfo
1 (Type/Class)	Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
2 (Data Constructor)	Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
TopLevelModuleName
1 (Type/Class)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
topLevelModuleName
1 (Function)	Agda.Syntax.Concrete
2 (Function)	Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
topoSort	Agda.Utils.Permutation
topSearch	Agda.Auto.NarrowingSearch
top_command'	Agda.Interaction.GhciTop
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, Agda.Interaction.GhciTop
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
traceCall_	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
traceFun	Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
traceFun'	Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
transitiveClosure	Agda.Utils.Graph
translateCase	Agda.Compiler.Epic.Primitive
translatedClause	Agda.Syntax.Internal
translateDefn	Agda.Compiler.Epic.FromAgda
translateRecordPatterns	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
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
tryOpen	Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
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
TypeAndDef	Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
typeCheck	Agda.Interaction.Imports
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
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
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
typeOfSizeInf	Agda.TypeChecking.Rules.Builtin
typeOfSizeSuc	Agda.TypeChecking.Rules.Builtin
typeOfVar	Agda.TypeChecking.Coverage
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