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

Index - T

TAgda.Mimer.Options
TAConAgda.Syntax.Treeless, Agda.Compiler.Backend
TacticAgda.Syntax.Concrete
TacticAttribute 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Concrete.Attribute
4 (Type/Class)Agda.Syntax.Abstract
TacticAttribute'Agda.Syntax.Concrete
TacticAttributeNotAllowedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
tails1Agda.Utils.List1
tailWithDefaultAgda.Utils.List
takeAgda.Utils.List1
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
takeOptionsPragmasAgda.Syntax.Parser.Helpers
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
target 
1 (Function)Agda.Utils.BiMap
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
TargetDefAgda.Termination.Monad
targetNodes 
1 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)Agda.Termination.CallGraph
TargetOtherAgda.Termination.Monad
TargetRecordAgda.Termination.Monad
tbFiniteAgda.Syntax.Abstract
TBind 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
tbTacticAttrAgda.Syntax.Abstract
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
tcErrLocationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrStringAgda.TypeChecking.Errors
tcExecAgda.TypeChecking.Unquote
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
TCMErrorAgda.Interaction.ExitCode
TCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCoerceAgda.Syntax.Treeless, Agda.Compiler.Backend
TConAgda.Syntax.Treeless, Agda.Compiler.Backend
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
tcWarningLocationAgda.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.Monad.Base, Agda.TypeChecking.Warnings, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
tell1Agda.Utils.Monad
tellDirtyAgda.Utils.Update
tellEmacsToJumpToErrorAgda.Interaction.InteractionTop
tellEqAgda.TypeChecking.Rewriting.NonLinMatch
tellSubAgda.TypeChecking.Rewriting.NonLinMatch
tellToUpdateHighlightingAgda.Interaction.InteractionTop
tellUnifyProofAgda.TypeChecking.Rules.LHS.Unify.Types
tellUnifySubstAgda.TypeChecking.Rules.LHS.Unify.Types
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
TentativeAgda.Syntax.Parser.Monad
TErasedAgda.Syntax.Treeless, Agda.Compiler.Backend
terAskAgda.Termination.Monad
terAsksAgda.Termination.Monad
terCurrentAgda.Termination.Monad
terCutOffAgda.Termination.Monad
TerEnv 
1 (Type/Class)Agda.Termination.Monad
2 (Data Constructor)Agda.Termination.Monad
terGetCurrentAgda.Termination.Monad
terGetCutOffAgda.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.Syntax.Internal
2 (Type/Class)Agda.Syntax.Reflected
terMAgda.Termination.Monad
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
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.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.Syntax.Common.Aspect, Agda.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.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
TermSizeAgda.Syntax.Internal
termSizeAgda.Syntax.Internal
termsSAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
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
terSetGuardedAgda.Termination.Monad
terSetHaveInlinedWithAgda.Termination.Monad
terSetMaskArgsAgda.Termination.Monad
terSetMaskResultAgda.Termination.Monad
terSetPatternsAgda.Termination.Monad
TerSetSizeDepthAgda.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.Syntax.Common.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
tgtNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
thd3Agda.Utils.Tuple
theAttrAgda.Syntax.Parser.Helpers
theBenchmarkAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theBlockerAgda.Syntax.Internal.Blockers, Agda.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
theEtaEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theFixityAgda.Syntax.Common
TheFlexRigMapAgda.TypeChecking.Free.Lazy
theFlexRigMapAgda.TypeChecking.Free.Lazy
TheInfoAgda.TypeChecking.Coverage.SplitClause
theInteractionPointsAgda.Interaction.Base
theKindAgda.Syntax.Scope.Base
theMetaSetAgda.TypeChecking.Free.Lazy
theNameRangeAgda.Syntax.Common
theNotationAgda.Syntax.Common
thenReduceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
thenTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theSizeAgda.Utils.Size
theSmallSetAgda.Utils.SmallSet
theSolutionAgda.TypeChecking.SizedTypes.Syntax
theTacticAttributeAgda.Syntax.Concrete
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
throwDecodeAgda.Interaction.JSON
throwDecode'Agda.Interaction.JSON
throwDecodeStrictAgda.Interaction.JSON
throwDecodeStrict'Agda.Interaction.JSON
throwDecodeStrictTextAgda.Interaction.JSON
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
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
tLevelUnivAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
TLitAgda.Syntax.Treeless, Agda.Compiler.Backend
tlmodOfAgda.Compiler.MAlonzo.Misc
tMaybeAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
TMetaAgda.Syntax.Treeless, Agda.Compiler.Backend
tmSortAgda.Syntax.Internal
tmSSortAgda.Syntax.Internal
tNegPlusKAgda.Syntax.Treeless, Agda.Compiler.Backend
toAgda.Interaction.Highlighting.Range
toAbsNAgda.TypeChecking.Names
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.BoolSet
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.SmallSet
4 (Function)Agda.Utils.Trie
toAtomsAgda.Interaction.Highlighting.Common
toAttributeAgda.Syntax.Parser.Helpers
toBoolAgda.Utils.Boolean
ToConcreteAgda.Syntax.Translation.AbstractToConcrete
toConcreteAgda.Syntax.Translation.AbstractToConcrete
toConcreteCtxAgda.Syntax.Translation.AbstractToConcrete
toConPatternInfoAgda.Syntax.Internal
toCTypeAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
toDescListAgda.Utils.VarSet
toDistinctAscendingListsAgda.Utils.BiMap
toEncodingAgda.Interaction.JSON
toEncoding1Agda.Interaction.JSON
toEncoding2Agda.Interaction.JSON
toEncodingListAgda.Interaction.JSON
toExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
toFiniteListAgda.Utils.IntSet.Infinite
toFinitePiAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
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
Token 
1 (Type/Class)Agda.Syntax.Parser.Tokens
2 (Type/Class)Agda.Mimer.Options
token 
1 (Function)Agda.Utils.Parser.MemoisedCPS
2 (Function)Agda.Syntax.Parser.LexActions
TokenBased 
1 (Type/Class)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
tokenBasedAgda.Syntax.Common.Aspect, Agda.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.List1, Agda.Utils.List2
2 (Function)Agda.Utils.VarSet
3 (Function)Agda.Utils.HashTable
4 (Function)Agda.Utils.BoolSet
5 (Function)Agda.Utils.Bag
6 (Function)Agda.Utils.SmallSet
7 (Function)Agda.Utils.Trie
8 (Function)Agda.Utils.Favorites
9 (Function)Agda.Utils.BiMap
10 (Function)Agda.Termination.CallMatrix
11 (Function)Agda.Termination.CallGraph
12 (Function)Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
toList'Agda.Utils.List1
toList1Agda.Utils.List2
toList1EitherAgda.Utils.List2
toListOrderedByAgda.Utils.Trie
toListsAgda.Termination.SparseMatrix
toLTypeAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
toMapAgda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
ToNLPatAgda.TypeChecking.Rewriting.Clause
toNLPatAgda.TypeChecking.Rewriting.Clause
TooFewArgumentsToPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyArgumentsToLeveledSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyArgumentsToUnivOmegaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyFields 
1 (Data Constructor)Agda.TypeChecking.Monad.Base.Warning
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyFields_Agda.Interaction.Options.Warnings
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
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 (Data Constructor)Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
2 (Type/Class)Agda.Syntax.TopLevelModuleName
topLevelModuleName 
1 (Function)Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)Agda.Syntax.Translation.ConcreteToAbstract
3 (Function)Agda.Compiler.Common
TopLevelModuleName'Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
TopLevelModuleNamePartsAgda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
topLevelModuleNameToQNameAgda.Syntax.TopLevelModuleName
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
topSortAgda.Utils.Graph.TopSort
topVarOccAgda.TypeChecking.Free.Lazy
toReduceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
toSingletonAgda.Utils.BoolSet
toSparseRowsAgda.Termination.SparseMatrix
toSplitPatternsAgda.TypeChecking.Coverage.Match
toSplitPSubstAgda.TypeChecking.Coverage.Match
toStrictAgda.Utils.Maybe.Strict
toStringWithoutDotZeroAgda.Utils.Float
toSubscriptDigitAgda.Utils.Suffix
total 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.SmallSet
ToTermAgda.TypeChecking.Primitive
toTermAgda.TypeChecking.Primitive
toTermRAgda.TypeChecking.Primitive
toTreeAgda.TypeChecking.Coverage.SplitTree
toTreelessAgda.Compiler.ToTreeless, Agda.Compiler.Backend
toTreelessWithAgda.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.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
transitiveReductionAgda.Utils.Graph.AdjacencyMap.Unidirectional
translateBuiltinsAgda.Compiler.Treeless.Builtin
translateCompiledClausesAgda.TypeChecking.RecordPatterns
translateRecordPatternsAgda.TypeChecking.RecordPatterns
translateSplitTreeAgda.TypeChecking.RecordPatterns
TransparentDefAgda.Syntax.Common
TranspErrorAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
TranspOpAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpose 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Function)Agda.Termination.SparseMatrix
transposeEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
transpPathPTel'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpPathTel'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpSysAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpSysTel'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpTelAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpTel'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
traverse'Agda.Utils.Bag
traverseAPatternMAgda.Syntax.Abstract.Pattern
traverseCPatternAAgda.Syntax.Concrete.Pattern
traverseCPatternMAgda.Syntax.Concrete.Pattern
TraverseDeclAgda.Syntax.Concrete.Generic
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
traverseTermMAgda.Syntax.Internal.Generic
treelessPrimNameAgda.Compiler.MAlonzo.Primitives
trFillPathPTel'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
trFillPathTel'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
trFillTelAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
trFillTel'Agda.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
trueAgda.Utils.Boolean
trueConditionAgda.TypeChecking.MetaVars
truncatedCallStackAgda.Utils.CallStack
TruncateOffsetAgda.TypeChecking.SizedTypes.Syntax
truncateOffsetAgda.TypeChecking.SizedTypes.Syntax
tryAddBoundaryAgda.TypeChecking.MetaVars
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
tryTranspErrorAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
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 (Type/Class)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Internal
4 (Type/Class)Agda.Syntax.Reflected
5 (Type/Class)Agda.Syntax.Abstract
Type'Agda.Syntax.Internal
Type''Agda.Syntax.Internal
typeAndFacesInMetaAgda.Interaction.BasicOps
typeAnnotationsAgda.TypeChecking.Rules.LHS.Problem
typeArgsWithTelAgda.TypeChecking.Substitute
typeArityAgda.TypeChecking.Telescope
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.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
TypeclassAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
typeConArgsLeftAgda.TypeChecking.Rules.LHS.Unify.Types
typeConArgsRightAgda.TypeChecking.Rules.LHS.Unify.Types
typeConInjectAtAgda.TypeChecking.Rules.LHS.Unify.Types
TypeConInjectivityAgda.TypeChecking.Rules.LHS.Unify.Types
typeConstructorAgda.TypeChecking.Rules.LHS.Unify.Types
TypedAssignAgda.Interaction.Base
TypedBinding 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
TypedBinding'Agda.Syntax.Concrete
TypedBindingInfo 
1 (Type/Class)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Abstract
TypeDeclAgda.Utils.Haskell.Syntax
TypeDoesNotEndInSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
typeError'_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeError_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeInCurrentAgda.Interaction.BasicOps
typeInMetaAgda.Interaction.BasicOps
typeInTypeAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TypeKAgda.Compiler.MAlonzo.Misc
TypeLevelReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeLevelReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeNameAgda.TypeChecking.Level
TypeOfAgda.Syntax.Internal
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
typeSigAgda.Syntax.Parser.Helpers
TypeSignature 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
TypeSignatureOrInstanceBlockAgda.Syntax.Concrete
TypeSigsRHSAgda.Syntax.Parser.Helpers
typesOfHiddenMetasAgda.Interaction.BasicOps
typesOfVisibleMetasAgda.Interaction.BasicOps
TypingAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TypstFileTypeAgda.Syntax.Common
TyVarAgda.Utils.Haskell.Syntax
TyVarBindAgda.Utils.Haskell.Syntax