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

Index - T

TAgda.Auto.Options
TAConAgda.Syntax.Treeless, Agda.Compiler.Backend
TacticAgda.Syntax.Concrete
TacticAttrAgda.Syntax.Abstract
TacticAttribute 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete.Attribute
tacticAttributesAgda.Syntax.Concrete.Attribute
TagAgda.Utils.BiMap
tagAgda.Utils.BiMap
tagFieldNameAgda.Interaction.JSON
TaggedObjectAgda.Interaction.JSON
tagInjectiveForAgda.Utils.BiMap
tagSingleConstructorsAgda.Interaction.JSON
TAGuardAgda.Syntax.Treeless, Agda.Compiler.Backend
tail 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List2
tailMaybeAgda.Utils.List
tailsAgda.Utils.List1
tailWithDefaultAgda.Utils.List
takeAgda.Utils.List1
takeAwakeConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
takeAwakeConstraint'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
takeConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
takePAgda.Utils.Permutation
takeSizeConstraintsAgda.TypeChecking.SizedTypes
takeWhileAgda.Utils.List1
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.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TCErrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcErrClosErrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcErrLocationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcErrStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcErrStringAgda.TypeChecking.Errors
tcExecAgda.TypeChecking.Unquote
tcExpAgda.Auto.Typecheck
TCM 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TCMErrorAgda.Interaction.ExitCode
TCMTAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TCoerceAgda.Syntax.Treeless, Agda.Compiler.Backend
TConAgda.Syntax.Treeless, Agda.Compiler.Backend
tcSearchAgda.Auto.Typecheck
TCStAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TCStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TCWarning 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningCachedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningLocationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningOriginAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningPrintedWarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningRangeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
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
telePiPath_Agda.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
Telescope1 
1 (Type/Class)Agda.Syntax.Concrete
2 (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.Compiler.Backend, Agda.TypeChecking.Monad
TentativeAgda.Syntax.Parser.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
termErrFunctionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TermHeadAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
3 (Type/Class)Agda.Syntax.Concrete.Definitions.Types
terminationCheckAgda.Syntax.Concrete.Definitions.Types
TerminationCheckPragmaAgda.Syntax.Concrete
terminationCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
TerminationError 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TerminationIssueAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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, Agda.TypeChecking.Primitive.Cubical
TermSizeAgda.Syntax.Internal
termSizeAgda.Syntax.Internal
TermSubstAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
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.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
tgtNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
thd3Agda.Utils.Tuple
theBenchmarkAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theBlockerAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
theCallGraphAgda.Termination.CallGraph
theConstraintAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theCoreAgda.TypeChecking.Substitute
theCurrentFileAgda.Interaction.Base
theDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theDefLensAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theEtaEqualityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theFixityAgda.Syntax.Common
TheFlexRigMapAgda.TypeChecking.Free.Lazy
theFlexRigMapAgda.TypeChecking.Free.Lazy
theInteractionPointsAgda.Interaction.Base
theKindAgda.Syntax.Scope.Base
theMetaSetAgda.TypeChecking.Free.Lazy
theNameRangeAgda.Syntax.Common
theNotationAgda.Syntax.Common
thenReduceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
thenTCMTAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
throwImpossibleAgda.Utils.Impossible
throwMultipleFixityDeclsAgda.Syntax.Concrete.Fixity
throwMultiplePolarityPragmasAgda.Syntax.Concrete.Fixity
tickAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
tickICodeAgda.TypeChecking.Serialise.Base
tickMaxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
tickNAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
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
tMaybeAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
TMetaAgda.Syntax.Treeless, Agda.Compiler.Backend
TModeAgda.Auto.Convert
tmSortAgda.Syntax.Internal
tmSSortAgda.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
toAbstractWithoutImplicitAgda.Syntax.Translation.ReflectedToAbstract
toAbstract_Agda.Syntax.Translation.ReflectedToAbstract
ToArgsAgda.Interaction.JSON
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
toDistinctAscendingListsAgda.Utils.BiMap
toEncodingAgda.Interaction.JSON
toEncoding1Agda.Interaction.JSON
toEncoding2Agda.Interaction.JSON
toEncodingListAgda.Interaction.JSON
toFiniteListAgda.Utils.IntSet.Infinite
ToggleImplicitArgsAgda.Interaction.Base
ToggleIrrelevantArgsAgda.Interaction.Base
toIFileAgda.Interaction.FindFile
toImpossibleAgda.Utils.Empty
ToJSONAgda.Interaction.JSON
toJSONAgda.Interaction.JSON
ToJSON1Agda.Interaction.JSON
toJSON1Agda.Interaction.JSON
ToJSON2Agda.Interaction.JSON
toJSON2Agda.Interaction.JSON
ToJSONKeyAgda.Interaction.JSON
toJSONKeyAgda.Interaction.JSON
ToJSONKeyFunctionAgda.Interaction.JSON
toJSONKeyListAgda.Interaction.JSON
ToJSONKeyTextAgda.Interaction.JSON
ToJSONKeyValueAgda.Interaction.JSON
toJSONListAgda.Interaction.JSON
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
TokEOFAgda.Syntax.Parser.Tokens
TokIdAgda.Syntax.Parser.Tokens
TokKeywordAgda.Syntax.Parser.Tokens
TokLiteralAgda.Syntax.Parser.Tokens
TokMarkupAgda.Syntax.Parser.Tokens
TokQIdAgda.Syntax.Parser.Tokens
TokStringAgda.Syntax.Parser.Tokens
TokSymbolAgda.Syntax.Parser.Tokens
TokTeXAgda.Syntax.Parser.Tokens
toLazyAgda.Utils.Maybe.Strict
toList 
1 (Function)Agda.Utils.List2
2 (Function)Agda.Utils.List1
3 (Function)Agda.Utils.VarSet
4 (Function)Agda.Utils.Bag
5 (Function)Agda.Utils.SmallSet
6 (Function)Agda.Utils.Trie
7 (Function)Agda.Utils.BiMap
8 (Function)Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
9 (Function)Agda.Utils.Favorites
10 (Function)Agda.Termination.CallMatrix
11 (Function)Agda.Termination.CallGraph
toList1Agda.Utils.List2
toListOrderedByAgda.Utils.Trie
toListsAgda.Termination.SparseMatrix
toLTypeAgda.TypeChecking.Rules.Data
TOMAgda.Auto.Convert
toMapAgda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
tomyAgda.Auto.Convert
tomyIneqAgda.Auto.Convert
ToNLPatAgda.TypeChecking.Rewriting.Clause
toNLPatAgda.TypeChecking.Rewriting.Clause
TooFewArgumentsToPatternSynonymAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TooManyFieldsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TooManyFieldsWarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TooManyFieldsWarning_Agda.Interaction.Options.Warnings
TooManyPolaritiesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
toOrderingsAgda.Utils.PartialOrd
TopAgda.TypeChecking.SizedTypes.Utils
tOpAgda.Syntax.Treeless, Agda.Compiler.Backend
topAgda.TypeChecking.SizedTypes.Utils
topBlockAgda.Syntax.Parser.Monad
topCohesionAgda.Syntax.Common
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
topoSortMAgda.Utils.Permutation
topQuantityAgda.Syntax.Common
topRelevanceAgda.Syntax.Common
topSearchAgda.Auto.NarrowingSearch
topSortAgda.Utils.Graph.TopSort
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.Backend, Agda.Compiler.ToTreeless
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
traceCallCPSAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
traceCallMAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
traceClosureCallAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
traceDebugMessageAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
traceMAgda.TypeChecking.SizedTypes.Utils
TraceSAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
traceSAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
traceSDocAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
traceSLnAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
transitiveReductionAgda.Utils.Graph.AdjacencyMap.Unidirectional
translateBuiltinsAgda.Compiler.Treeless.Builtin
translateCompiledClausesAgda.TypeChecking.RecordPatterns
translateRecordPatternsAgda.TypeChecking.RecordPatterns
translateSplitTreeAgda.TypeChecking.RecordPatterns
TranspOrHCompAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
transpose 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Function)Agda.Termination.SparseMatrix
transposeEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
transpTelAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
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
TraverseExprFnAgda.Syntax.Abstract.Views
TraverseExprRecFnAgda.Syntax.Abstract.Views
traverseFAgda.Utils.Functor
traversePatternMAgda.Syntax.Internal.Pattern
traversePiAgda.Auto.Typecheck
traverseTermMAgda.Syntax.Internal.Generic
TravWithAgda.Auto.NarrowingSearch
TrBr 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
treatAbstractlyAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
treatAbstractly'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
treelessPrimNameAgda.Compiler.MAlonzo.Primitives
trFillTelAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
Trie 
1 (Type/Class)Agda.Utils.Trie
2 (Data Constructor)Agda.Utils.Trie
TriedToCopyConstrainedPrimAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
trimAgda.Utils.String
trimLineCommentAgda.Interaction.Library.Parse
trivialAgda.TypeChecking.SizedTypes
trueConditionAgda.TypeChecking.MetaVars
truncatedCallStackAgda.Utils.CallStack
TruncateOffsetAgda.TypeChecking.SizedTypes.Syntax
truncateOffsetAgda.TypeChecking.SizedTypes.Syntax
tryCatchAgda.Utils.Monad
tryConversionAgda.TypeChecking.Conversion
tryConversion'Agda.TypeChecking.Conversion
tryGetOpenAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open
tryMaybeAgda.Utils.Monad
tryRecordTypeAgda.TypeChecking.Records
tryResolveNameAgda.Syntax.Scope.Monad
trySizeUnivAgda.TypeChecking.SizedTypes
tryStrengthenAgda.Compiler.Treeless.Subst
tsetAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
tsizeAgda.Syntax.Internal
tSizeUnivAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
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
TwoElemArrayAgda.Interaction.JSON
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
typeAnnotationsAgda.TypeChecking.Rules.LHS.Problem
typeArgsWithTelAgda.TypeChecking.Substitute
typeArityAgda.TypeChecking.Telescope
TypeCheckAgda.Interaction.Imports
TypeCheckActionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TypeCheckingProblemAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeError'Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeError'_Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeError_Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeInCurrentAgda.Interaction.BasicOps
typeInMetaAgda.Interaction.BasicOps
typeInTypeAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TypeKAgda.Compiler.MAlonzo.Misc
TypeLevelReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeLevelReductionsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
typeNameAgda.TypeChecking.Level
typeOfBVAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
typeOfConstAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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