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

Index - T

TAgda.Auto.Options
TAConAgda.Syntax.Treeless, Agda.Compiler.Backend
Tactic 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
TacticAttrAgda.Syntax.Abstract
TacticAttribute 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete.Attribute
tacticAttributesAgda.Syntax.Concrete.Attribute
TAGuardAgda.Syntax.Treeless, Agda.Compiler.Backend
tailMaybeAgda.Utils.List
tailWithDefaultAgda.Utils.List
takeAwakeConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
takeAwakeConstraint'Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
takeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
takePAgda.Utils.Permutation
takeSizeConstraintsAgda.TypeChecking.SizedTypes
takeWhileJustAgda.Utils.List
TALitAgda.Syntax.Treeless, Agda.Compiler.Backend
tallyDefAgda.TypeChecking.MetaVars.Occurs
TAltAgda.Syntax.Treeless, Agda.Compiler.Backend
TAppAgda.Syntax.Treeless, Agda.Compiler.Backend
tAppViewAgda.Syntax.Treeless, Agda.Compiler.Backend
TargetAgda.Termination.Monad
targetAgda.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
tcargsAgda.Auto.Typecheck
TCaseAgda.Syntax.Treeless, Agda.Compiler.Backend
TCEnv 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrClosErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrStringAgda.TypeChecking.Errors
tcExpAgda.Auto.Typecheck
TCM 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCoerceAgda.Syntax.Treeless, Agda.Compiler.Backend
TConAgda.Syntax.Treeless, Agda.Compiler.Backend
tcSearchAgda.Auto.Typecheck
TCStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCWarning 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningCachedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningOriginAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningPrintedWarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningsAgda.TypeChecking.Warnings
tcWarningsToErrorAgda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
TDefAgda.Syntax.Treeless, Agda.Compiler.Backend
Tel 
1 (Type/Class)Agda.Syntax.Concrete.Pretty
2 (Data Constructor)Agda.Syntax.Concrete.Pretty
TelCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TeleAgda.Syntax.Internal
tele2NamedArgsAgda.TypeChecking.Telescope
teleArgNamesAgda.TypeChecking.Telescope
teleArgsAgda.TypeChecking.Telescope
teleDomsAgda.TypeChecking.Telescope
teleElimsAgda.TypeChecking.Telescope
teleLamAgda.TypeChecking.Substitute
teleNamedArgsAgda.TypeChecking.Telescope
teleNamesAgda.TypeChecking.Telescope
TeleNoAbsAgda.TypeChecking.Substitute
teleNoAbsAgda.TypeChecking.Substitute
telePatternsAgda.TypeChecking.Telescope
telePatterns'Agda.TypeChecking.Telescope
telePiAgda.TypeChecking.Substitute
telePi'Agda.TypeChecking.Substitute
telePiPathAgda.TypeChecking.Telescope.Path
telePiVisibleAgda.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.Syntax.Internal
telFromList'Agda.Syntax.Internal
tellDirtyAgda.Utils.Update
tellEmacsToJumpToErrorAgda.Interaction.InteractionTop
tellEqAgda.TypeChecking.Rewriting.NonLinMatch
tellSubAgda.TypeChecking.Rewriting.NonLinMatch
tellToUpdateHighlightingAgda.Interaction.InteractionTop
TelToArgsAgda.Syntax.Internal
telToArgsAgda.Syntax.Internal
telToListAgda.Syntax.Internal
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
telView'PathAgda.TypeChecking.Telescope
telView'UpToAgda.TypeChecking.Substitute
telView'UpToPathAgda.TypeChecking.Telescope
telViewPathAgda.TypeChecking.Telescope
telViewPathBoundaryPAgda.TypeChecking.Telescope
telViewUpToAgda.TypeChecking.Telescope
telViewUpTo'Agda.TypeChecking.Telescope
telViewUpToPathAgda.TypeChecking.Telescope
telViewUpToPathBoundaryAgda.TypeChecking.Telescope
telViewUpToPathBoundary'Agda.TypeChecking.Telescope
telViewUpToPathBoundaryPAgda.TypeChecking.Telescope
TempInstanceTableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TErasedAgda.Syntax.Treeless, Agda.Compiler.Backend
terAskAgda.Termination.Monad
terAsksAgda.Termination.Monad
terCurrentAgda.Termination.Monad
terCutOffAgda.Termination.Monad
terDelayedAgda.Termination.Monad
TerEnv 
1 (Type/Class)Agda.Termination.Monad
2 (Data Constructor)Agda.Termination.Monad
terGetCurrentAgda.Termination.Monad
terGetCutOffAgda.Termination.Monad
terGetDelayedAgda.Termination.Monad
terGetGuardedAgda.Termination.Monad
terGetHaveInlinedWithAgda.Termination.Monad
terGetMaskArgsAgda.Termination.Monad
terGetMaskResultAgda.Termination.Monad
terGetMutualAgda.Termination.Monad
terGetPatternsAgda.Termination.Monad
terGetSharpAgda.Termination.Monad
terGetSizeSucAgda.Termination.Monad
terGetTargetAgda.Termination.Monad
terGetUsableVarsAgda.Termination.Monad
terGetUseDotPatternsAgda.Termination.Monad
terGetUserNamesAgda.Termination.Monad
terGetUseSizeLtAgda.Termination.Monad
terGuardedAgda.Termination.Monad
terHaveInlinedWithAgda.Termination.Monad
terLocalAgda.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
4 (Type/Class)Agda.Syntax.Reflected
terMAgda.Termination.Monad
termAgda.Compiler.MAlonzo.Compiler
terMaskArgsAgda.Termination.Monad
terMaskResultAgda.Termination.Monad
termCAgda.TypeChecking.Serialise.Base
termDAgda.TypeChecking.Serialise.Base
termDeclAgda.Termination.TermCheck
termErrCallsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
termErrFunctionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TermHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
terminatesAgda.Termination.Termination
terminatesFilterAgda.Termination.Termination
TerminatingAgda.Syntax.Common
TerminationAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TerminationCheck 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
TerminationCheckPragmaAgda.Syntax.Concrete
TerminationError 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TerminationIssueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TerminationIssue_Agda.Interaction.Options.Warnings
TerminationMeasureAgda.Syntax.Common
TerminationProblemAgda.Interaction.Highlighting.Precise
TermLikeAgda.Syntax.Internal.Generic
termMutualAgda.Termination.TermCheck
terModifyGuardedAgda.Termination.Monad
terModifyUsableVarsAgda.Termination.Monad
terModifyUseSizeLtAgda.Termination.Monad
TermPartAgda.TypeChecking.Unquote
TermPositionAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
TermSizeAgda.Syntax.Internal
termSizeAgda.Syntax.Internal
TermToPatternAgda.TypeChecking.Patterns.Internal
termToPatternAgda.TypeChecking.Patterns.Internal
terMutualAgda.Termination.Monad
terPatternsAgda.Termination.Monad
terPatternsRaiseAgda.Termination.Monad
terRaiseAgda.Termination.Monad
TError 
1 (Type/Class)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor)Agda.Syntax.Treeless, Agda.Compiler.Backend
terSetCurrentAgda.Termination.Monad
terSetDelayedAgda.Termination.Monad
terSetGuardedAgda.Termination.Monad
terSetHaveInlinedWithAgda.Termination.Monad
terSetMaskArgsAgda.Termination.Monad
terSetMaskResultAgda.Termination.Monad
terSetPatternsAgda.Termination.Monad
terSetSizeDepthAgda.Termination.Monad
terSetTargetAgda.Termination.Monad
terSetUsableVarsAgda.Termination.Monad
terSetUseDotPatternsAgda.Termination.Monad
terSetUseSizeLtAgda.Termination.Monad
terSharpAgda.Termination.Monad
terSizeDepthAgda.Termination.Monad
terSizeSucAgda.Termination.Monad
terTargetAgda.Termination.Monad
terUnguardedAgda.Termination.Monad
terUsableVarsAgda.Termination.Monad
terUseDotPatternsAgda.Termination.Monad
terUserNamesAgda.Termination.Monad
terUseSizeLtAgda.Termination.Monad
testLubAgda.TypeChecking.SizedTypes.WarshallSolver
testSuccsAgda.TypeChecking.SizedTypes.WarshallSolver
TexFileTypeAgda.Syntax.Common
text 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
textCAgda.TypeChecking.Serialise.Base
textDAgda.TypeChecking.Serialise.Base
textEAgda.TypeChecking.Serialise.Base
tgtNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
thd3Agda.Utils.Tuple
theBenchmarkAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theBlockingMetaAgda.Syntax.Internal
theCallGraphAgda.Termination.CallGraph
theConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theCoreAgda.TypeChecking.Substitute
theCurrentFileAgda.Interaction.Base
theDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theDefLensAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theEtaEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theFixityAgda.Syntax.Common
TheFlexRigMapAgda.TypeChecking.Free.Lazy
theFlexRigMapAgda.TypeChecking.Free.Lazy
theInteractionPointsAgda.Interaction.Base
theMetaSetAgda.TypeChecking.Free.Lazy
theNameRangeAgda.Syntax.Common
theNotationAgda.Syntax.Common
thenTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theSizeAgda.Utils.Size
theSolutionAgda.TypeChecking.SizedTypes.Syntax
theTelAgda.TypeChecking.Substitute
TheVarMapAgda.TypeChecking.Free.Lazy
theVarMapAgda.TypeChecking.Free.Lazy
TheVarMap'Agda.TypeChecking.Free.Lazy
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
Three 
1 (Type/Class)Agda.Utils.Three
2 (Data Constructor)Agda.Utils.Three
throwErrorAgda.Utils.Except
throwImpossibleAgda.Utils.Impossible
throwMultipleFixityDeclsAgda.Syntax.Concrete.Fixity
throwMultiplePolarityPragmasAgda.Syntax.Concrete.Fixity
tickAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tickICodeAgda.TypeChecking.Serialise.Base
tickMaxAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tickNAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tIfThenElseAgda.Syntax.Treeless, Agda.Compiler.Backend
TimeOut 
1 (Type/Class)Agda.Auto.Options
2 (Data Constructor)Agda.Auto.Options
TimingsAgda.Utils.Benchmark
timingsAgda.Utils.Benchmark
tIntAgda.Syntax.Treeless, Agda.Compiler.Backend
TLamAgda.Syntax.Treeless, Agda.Compiler.Backend
tLamViewAgda.Syntax.Treeless, Agda.Compiler.Backend
TLet 
1 (Data Constructor)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
tLetViewAgda.Syntax.Treeless, Agda.Compiler.Backend
TLitAgda.Syntax.Treeless, Agda.Compiler.Backend
tlmodOfAgda.Compiler.MAlonzo.Misc
TMAllAgda.Auto.Convert
TModeAgda.Auto.Convert
tmSortAgda.Syntax.Internal
tNegPlusKAgda.Syntax.Treeless, Agda.Compiler.Backend
toAgda.Interaction.Highlighting.Range
toAbsNameAgda.TypeChecking.Serialise.Instances.Abstract
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
toAbstractPatsAgda.Syntax.Translation.ReflectedToAbstract
toAbstractWithoutImplicitAgda.Syntax.Translation.ReflectedToAbstract
toAbstract_Agda.Syntax.Translation.ReflectedToAbstract
toAscList 
1 (Function)Agda.Utils.Bag
2 (Function)Agda.Utils.SmallSet
3 (Function)Agda.Utils.Trie
toAtomsAgda.Interaction.Highlighting.Common
ToConcreteAgda.Syntax.Translation.AbstractToConcrete
toConcreteAgda.Syntax.Translation.AbstractToConcrete
toConcreteCtxAgda.Syntax.Translation.AbstractToConcrete
toConPatternInfoAgda.Syntax.Internal
toCTypeAgda.TypeChecking.Rules.Data
toDescListAgda.Utils.VarSet
toFiniteListAgda.Utils.IntSet.Infinite
ToggleImplicitArgsAgda.Interaction.Base
toIFileAgda.Interaction.FindFile
toImpossibleAgda.Utils.Empty
tokAgda.Utils.Parser.MemoisedCPS
TokCommentAgda.Syntax.Parser.Tokens
TokDummyAgda.Syntax.Parser.Tokens
TokenAgda.Syntax.Parser.Tokens
token 
1 (Function)Agda.Utils.Parser.MemoisedCPS
2 (Function)Agda.Syntax.Parser.LexActions
TokenBased 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
tokenBasedAgda.Interaction.Highlighting.Precise
TokenLengthAgda.Syntax.Parser.Alex
tokensParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser
tokenStreamAgda.Interaction.Highlighting.HTML
TokEOFAgda.Syntax.Parser.Tokens
TokIdAgda.Syntax.Parser.Tokens
TokKeywordAgda.Syntax.Parser.Tokens
TokLiteralAgda.Syntax.Parser.Tokens
TokMarkupAgda.Syntax.Parser.Tokens
TokPropNAgda.Syntax.Parser.Tokens
TokQIdAgda.Syntax.Parser.Tokens
TokSetNAgda.Syntax.Parser.Tokens
TokStringAgda.Syntax.Parser.Tokens
TokSymbolAgda.Syntax.Parser.Tokens
TokTeXAgda.Syntax.Parser.Tokens
toLazyAgda.Utils.Maybe.Strict
toList 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.BiMap
3 (Function)Agda.Utils.Bag
4 (Function)Agda.Utils.SmallSet
5 (Function)Agda.Utils.Trie
6 (Function)Agda.Utils.Favorites
7 (Function)Agda.Termination.CallMatrix
8 (Function)Agda.Termination.CallGraph
toListOrderedByAgda.Utils.Trie
toListsAgda.Termination.SparseMatrix
toLTypeAgda.TypeChecking.Rules.Data
TOMAgda.Auto.Convert
toMapAgda.Interaction.Highlighting.Precise
tomyAgda.Auto.Convert
tomyIneqAgda.Auto.Convert
ToNLPatAgda.TypeChecking.Rewriting.Clause
toNLPatAgda.TypeChecking.Rewriting.Clause
TooFewArgumentsToPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyPolaritiesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
toOrderingsAgda.Utils.PartialOrd
TopAgda.TypeChecking.SizedTypes.Utils
tOpAgda.Syntax.Treeless, Agda.Compiler.Backend
topAgda.TypeChecking.SizedTypes.Utils
topCohesionAgda.Syntax.Common
topContextAgda.Syntax.Parser.Monad
TopCtxAgda.Syntax.Fixity
TopKAgda.Syntax.Concrete.Operators.Parser.Monad
TopLevel 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract
topLevelArgAgda.TypeChecking.Injectivity
topLevelDeclsAgda.Syntax.Translation.ConcreteToAbstract
topLevelExpectedNameAgda.Syntax.Translation.ConcreteToAbstract
TopLevelInfo 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract
topLevelModuleDropperAgda.TypeChecking.Errors
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
topLevelPathAgda.Syntax.Translation.ConcreteToAbstract
topLevelScopeAgda.Syntax.Translation.ConcreteToAbstract
topLevelTheThingAgda.Syntax.Translation.ConcreteToAbstract
topModalityAgda.Syntax.Common
TopModuleAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TopOpenModuleAgda.Syntax.Scope.Monad
topoSortAgda.Utils.Permutation
topQuantityAgda.Syntax.Common
topRelevanceAgda.Syntax.Common
topSearchAgda.Auto.NarrowingSearch
topSort 
1 (Function)Agda.Utils.Graph.TopSort
2 (Function)Agda.Syntax.Internal
topVarOccAgda.TypeChecking.Free.Lazy
toSparseRowsAgda.Termination.SparseMatrix
toSplitPatternsAgda.TypeChecking.Coverage.Match
toSplitPSubstAgda.TypeChecking.Coverage.Match
toStrictAgda.Utils.Maybe.Strict
toStringWithoutDotZeroAgda.Utils.Float
toSubscriptDigitAgda.Utils.Suffix
totalAgda.Utils.SmallSet
ToTermAgda.TypeChecking.Primitive
toTermAgda.TypeChecking.Primitive
toTermRAgda.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, Agda.Compiler.Backend
toTreeAgda.TypeChecking.Coverage.SplitTree
toTreelessAgda.Compiler.ToTreeless, Agda.Compiler.Backend
toTreesAgda.TypeChecking.Coverage.SplitTree
toVimAgda.Interaction.Highlighting.Vim
toWeightAgda.TypeChecking.SizedTypes.WarshallSolver
TPFnAgda.Syntax.Treeless, Agda.Compiler.Backend
tPlusKAgda.Syntax.Treeless, Agda.Compiler.Backend
TPOpAgda.Syntax.Treeless, Agda.Compiler.Backend
TPrim 
1 (Type/Class)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor)Agda.Syntax.Treeless, Agda.Compiler.Backend
traceAgda.TypeChecking.SizedTypes.Utils
traceCallAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceCallCPSAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceCallMAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceClosureCallAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceDebugMessageAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceMAgda.TypeChecking.SizedTypes.Utils
TraceSAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceSAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceSDocAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceSLnAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
trailingWithPatternsAgda.Syntax.Abstract.Pattern
trampolineAgda.Utils.Function
trampolineMAgda.Utils.Function
trampolineWhileAgda.Utils.Function
trampolineWhileMAgda.Utils.Function
transClosAgda.TypeChecking.SizedTypes.WarshallSolver
transformAgda.Compiler.Treeless.EliminateLiteralPatterns
transitiveClosureAgda.Utils.Graph.AdjacencyMap.Unidirectional
translateBuiltinsAgda.Compiler.Treeless.Builtin
translateCompiledClausesAgda.TypeChecking.RecordPatterns
translateRecordPatternsAgda.TypeChecking.RecordPatterns
translateSplitTreeAgda.TypeChecking.RecordPatterns
TranspOrHCompAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpose 
1 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)Agda.Termination.SparseMatrix
transposeEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
transpTelAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
TravAgda.Auto.NarrowingSearch
travAgda.Auto.NarrowingSearch
traverse'Agda.Utils.Bag
traverseAPatternMAgda.Syntax.Abstract.Pattern
traverseCPatternAAgda.Syntax.Concrete.Pattern
traverseCPatternMAgda.Syntax.Concrete.Pattern
traverseEitherAgda.Utils.Either
traverseExpr 
1 (Function)Agda.Syntax.Concrete.Generic
2 (Function)Agda.Syntax.Abstract.Views
traverseFAgda.Utils.Functor
traversePatternMAgda.Syntax.Internal.Pattern
traversePiAgda.Auto.Typecheck
traverseTermMAgda.Syntax.Internal.Generic
TrBr 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
treatAbstractlyAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
treatAbstractly'Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
treelessPrimNameAgda.Compiler.MAlonzo.Primitives
trFillTelAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Trie 
1 (Type/Class)Agda.Utils.Trie
2 (Data Constructor)Agda.Utils.Trie
TriedToCopyConstrainedPrimAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
trimAgda.Utils.String
trimLineCommentAgda.Interaction.Library.Parse
trivialAgda.TypeChecking.SizedTypes
trueConditionAgda.TypeChecking.MetaVars
TruncateOffsetAgda.TypeChecking.SizedTypes.Syntax
truncateOffsetAgda.TypeChecking.SizedTypes.Syntax
tryCatchAgda.Utils.Monad
tryConversionAgda.TypeChecking.Conversion
tryConversion'Agda.TypeChecking.Conversion
tryGetOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tryMaybeAgda.Utils.Monad
tryRecordTypeAgda.TypeChecking.Records
tryResolveNameAgda.Syntax.Scope.Monad
trySizeUnivAgda.TypeChecking.SizedTypes
tryStrengthenAgda.Compiler.Treeless.Subst
tsetAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
tsizeAgda.Syntax.Internal
tSizeUnivAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
TSortAgda.Syntax.Treeless, Agda.Compiler.Backend
TTermAgda.Syntax.Treeless, Agda.Compiler.Backend
TUnitAgda.Syntax.Treeless, Agda.Compiler.Backend
TUnreachableAgda.Syntax.Treeless, Agda.Compiler.Backend
tUnreachableAgda.Syntax.Treeless, Agda.Compiler.Backend
tvaldeclAgda.Compiler.MAlonzo.Compiler
TVarAgda.Syntax.Treeless, Agda.Compiler.Backend
TwoAgda.Utils.Three
TyAppAgda.Utils.Haskell.Syntax
TyConAgda.Utils.Haskell.Syntax
TyForallAgda.Utils.Haskell.Syntax
TyFunAgda.Utils.Haskell.Syntax
Type 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Auto.Syntax
3 (Data Constructor)Agda.Syntax.Internal
4 (Type/Class)Agda.Syntax.Internal
5 (Type/Class)Agda.Syntax.Reflected
Type'Agda.Syntax.Internal
Type''Agda.Syntax.Internal
typeArgsWithTelAgda.TypeChecking.Substitute
typeArityAgda.TypeChecking.Telescope
TypeCheckAgda.Interaction.Imports
typeCheckAgda.Interaction.Imports
TypeCheckActionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TypeCheckingProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeCheckMainAgda.Interaction.Imports
TypeChecksAgda.Interaction.Highlighting.Precise
TypedAssignAgda.Interaction.Base
TypedBinding 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
TypedBinding'Agda.Syntax.Concrete
TypeDeclAgda.Utils.Haskell.Syntax
typeElimsAgda.TypeChecking.Records
TypeError 
1 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeError_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeInAgda.Interaction.CommandLine
typeInCurrentAgda.Interaction.BasicOps
typeInMetaAgda.Interaction.BasicOps
typeInTypeAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TypeLevelReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeLevelReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeNameAgda.TypeChecking.Level
typeOfAgda.Interaction.CommandLine
typeOfBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeOfConstAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeOfFlatAgda.TypeChecking.Rules.Builtin.Coinduction
typeOfInfAgda.TypeChecking.Rules.Builtin.Coinduction
typeOfMetaAgda.Interaction.BasicOps
typeOfMeta'Agda.Interaction.BasicOps
typeOfMetaMIAgda.Interaction.BasicOps
typeOfSharpAgda.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
TypeSignatureOrInstanceBlockAgda.Syntax.Concrete
typesOfHiddenMetasAgda.Interaction.BasicOps
typesOfVisibleMetasAgda.Interaction.BasicOps
TypingAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TyVarAgda.Utils.Haskell.Syntax
TyVarBindAgda.Utils.Haskell.Syntax