| T | Agda.Auto.Options |
| TACon | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Tactic | Agda.Syntax.Concrete |
| TacticAttr | Agda.Syntax.Abstract |
| TacticAttribute | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Attribute |
| tacticAttributes | Agda.Syntax.Concrete.Attribute |
| Tag | Agda.Utils.BiMap |
| tag | Agda.Utils.BiMap |
| tagFieldName | Agda.Interaction.JSON |
| TaggedObject | Agda.Interaction.JSON |
| tagInjectiveFor | Agda.Utils.BiMap |
| tagSingleConstructors | Agda.Interaction.JSON |
| TAGuard | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tail | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.List2 |
| tailMaybe | Agda.Utils.List |
| tails | Agda.Utils.List1 |
| tailWithDefault | Agda.Utils.List |
| take | Agda.Utils.List1 |
| takeAwakeConstraint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| takeAwakeConstraint' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| takeConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| takeP | Agda.Utils.Permutation |
| takeSizeConstraints | Agda.TypeChecking.SizedTypes |
| takeWhile | Agda.Utils.List1 |
| takeWhileJust | Agda.Utils.List |
| TALit | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tallyDef | Agda.TypeChecking.MetaVars.Occurs |
| TAlt | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TApp | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tAppView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Target | Agda.Termination.Monad |
| target | |
| 1 (Function) | Agda.Utils.BiMap |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph |
| TargetDef | Agda.Termination.Monad |
| targetNodes | |
| 1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Function) | Agda.Termination.CallGraph |
| TargetOther | Agda.Termination.Monad |
| TargetRecord | Agda.Termination.Monad |
| tbFinite | Agda.Syntax.Abstract |
| TBind | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| tbTacticAttr | Agda.Syntax.Abstract |
| tcargs | Agda.Auto.Typecheck |
| TCase | Agda.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 |
| TCErr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcErrClosErr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcErrLocation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcErrState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcErrString | Agda.TypeChecking.Errors |
| tcExec | Agda.TypeChecking.Unquote |
| tcExp | Agda.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 |
| TCMError | Agda.Interaction.ExitCode |
| TCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TCoerce | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TCon | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tcSearch | Agda.Auto.Typecheck |
| TCSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TCState | Agda.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 |
| tcWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcWarningCached | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcWarningLocation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcWarningOrigin | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcWarningPrintedWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcWarningRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| tcWarnings | Agda.TypeChecking.Warnings |
| tcWarningsToError | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| TDef | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Tel | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Pretty |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Pretty |
| Tele | Agda.Syntax.Internal |
| tele2NamedArgs | Agda.TypeChecking.Telescope |
| teleArgNames | Agda.TypeChecking.Telescope |
| teleArgs | Agda.TypeChecking.Telescope |
| teleDoms | Agda.TypeChecking.Telescope |
| teleElims | Agda.TypeChecking.Telescope |
| teleLam | Agda.TypeChecking.Substitute |
| teleNamedArgs | Agda.TypeChecking.Telescope |
| teleNames | Agda.TypeChecking.Telescope |
| TeleNoAbs | Agda.TypeChecking.Substitute |
| teleNoAbs | Agda.TypeChecking.Substitute |
| telePatterns | Agda.TypeChecking.Telescope |
| telePatterns' | Agda.TypeChecking.Telescope |
| telePi | Agda.TypeChecking.Substitute |
| telePi' | Agda.TypeChecking.Substitute |
| telePiPath | Agda.TypeChecking.Telescope.Path |
| telePiPath_ | Agda.TypeChecking.Telescope.Path |
| telePiVisible | Agda.TypeChecking.Substitute |
| telePi_ | Agda.TypeChecking.Substitute |
| Telescope | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Internal |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| Telescope1 | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| telFromList | Agda.Syntax.Internal |
| telFromList' | Agda.Syntax.Internal |
| tellDirty | Agda.Utils.Update |
| tellEmacsToJumpToError | Agda.Interaction.InteractionTop |
| tellEq | Agda.TypeChecking.Rewriting.NonLinMatch |
| tellSub | Agda.TypeChecking.Rewriting.NonLinMatch |
| tellToUpdateHighlighting | Agda.Interaction.InteractionTop |
| tellUnifyProof | Agda.TypeChecking.Rules.LHS.Unify.Types |
| tellUnifySubst | Agda.TypeChecking.Rules.LHS.Unify.Types |
| TelToArgs | Agda.Syntax.Internal |
| telToArgs | Agda.Syntax.Internal |
| telToList | Agda.Syntax.Internal |
| TelV | |
| 1 (Type/Class) | Agda.TypeChecking.Substitute |
| 2 (Data Constructor) | Agda.TypeChecking.Substitute |
| telVars | Agda.TypeChecking.Substitute |
| TelView | Agda.TypeChecking.Substitute |
| telView | Agda.TypeChecking.Telescope |
| telView' | Agda.TypeChecking.Substitute |
| telView'Path | Agda.TypeChecking.Telescope |
| telView'UpTo | Agda.TypeChecking.Substitute |
| telView'UpToPath | Agda.TypeChecking.Telescope |
| telViewPath | Agda.TypeChecking.Telescope |
| telViewPathBoundaryP | Agda.TypeChecking.Telescope |
| telViewUpTo | Agda.TypeChecking.Telescope |
| telViewUpTo' | Agda.TypeChecking.Telescope |
| telViewUpToPath | Agda.TypeChecking.Telescope |
| telViewUpToPathBoundary | Agda.TypeChecking.Telescope |
| telViewUpToPathBoundary' | Agda.TypeChecking.Telescope |
| telViewUpToPathBoundaryP | Agda.TypeChecking.Telescope |
| TempInstanceTable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Tentative | Agda.Syntax.Parser.Monad |
| TErased | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| terAsk | Agda.Termination.Monad |
| terAsks | Agda.Termination.Monad |
| terCurrent | Agda.Termination.Monad |
| terCutOff | Agda.Termination.Monad |
| terDelayed | Agda.Termination.Monad |
| TerEnv | |
| 1 (Type/Class) | Agda.Termination.Monad |
| 2 (Data Constructor) | Agda.Termination.Monad |
| terGetCurrent | Agda.Termination.Monad |
| terGetCutOff | Agda.Termination.Monad |
| terGetDelayed | Agda.Termination.Monad |
| terGetGuarded | Agda.Termination.Monad |
| terGetHaveInlinedWith | Agda.Termination.Monad |
| terGetMaskArgs | Agda.Termination.Monad |
| terGetMaskResult | Agda.Termination.Monad |
| terGetMutual | Agda.Termination.Monad |
| terGetPatterns | Agda.Termination.Monad |
| terGetSharp | Agda.Termination.Monad |
| terGetSizeSuc | Agda.Termination.Monad |
| terGetTarget | Agda.Termination.Monad |
| terGetUsableVars | Agda.Termination.Monad |
| terGetUseDotPatterns | Agda.Termination.Monad |
| terGetUserNames | Agda.Termination.Monad |
| terGetUseSizeLt | Agda.Termination.Monad |
| terGuarded | Agda.Termination.Monad |
| terHaveInlinedWith | Agda.Termination.Monad |
| terLocal | Agda.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 |
| terM | Agda.Termination.Monad |
| term | Agda.Compiler.MAlonzo.Compiler |
| terMaskArgs | Agda.Termination.Monad |
| terMaskResult | Agda.Termination.Monad |
| termC | Agda.TypeChecking.Serialise.Base |
| termD | Agda.TypeChecking.Serialise.Base |
| termDecl | Agda.Termination.TermCheck |
| termErrCalls | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| termErrFunctions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TermHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| terminates | Agda.Termination.Termination |
| terminatesFilter | Agda.Termination.Termination |
| Terminating | Agda.Syntax.Common |
| Termination | Agda.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 |
| terminationCheck | Agda.Syntax.Concrete.Definitions.Types |
| TerminationCheckPragma | Agda.Syntax.Concrete |
| terminationCheckPragma | Agda.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 |
| TerminationIssue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TerminationIssue_ | Agda.Interaction.Options.Warnings |
| TerminationMeasure | Agda.Syntax.Common |
| TerminationProblem | Agda.Interaction.Highlighting.Precise |
| TermLike | Agda.Syntax.Internal.Generic |
| termMutual | Agda.Termination.TermCheck |
| terModifyGuarded | Agda.Termination.Monad |
| terModifyUsableVars | Agda.Termination.Monad |
| terModifyUseSizeLt | Agda.Termination.Monad |
| TermPart | Agda.TypeChecking.Unquote |
| TermPosition | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical |
| TermSize | Agda.Syntax.Internal |
| termSize | Agda.Syntax.Internal |
| termsS | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse |
| TermSubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| TermToPattern | Agda.TypeChecking.Patterns.Internal |
| termToPattern | Agda.TypeChecking.Patterns.Internal |
| terMutual | Agda.Termination.Monad |
| terPatterns | Agda.Termination.Monad |
| terPatternsRaise | Agda.Termination.Monad |
| terRaise | Agda.Termination.Monad |
| TError | |
| 1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| terSetCurrent | Agda.Termination.Monad |
| terSetDelayed | Agda.Termination.Monad |
| terSetGuarded | Agda.Termination.Monad |
| terSetHaveInlinedWith | Agda.Termination.Monad |
| terSetMaskArgs | Agda.Termination.Monad |
| terSetMaskResult | Agda.Termination.Monad |
| terSetPatterns | Agda.Termination.Monad |
| TerSetSizeDepth | Agda.Termination.Monad |
| terSetSizeDepth | Agda.Termination.Monad |
| terSetTarget | Agda.Termination.Monad |
| terSetUsableVars | Agda.Termination.Monad |
| terSetUseDotPatterns | Agda.Termination.Monad |
| terSetUseSizeLt | Agda.Termination.Monad |
| terSharp | Agda.Termination.Monad |
| terSizeDepth | Agda.Termination.Monad |
| terSizeSuc | Agda.Termination.Monad |
| terTarget | Agda.Termination.Monad |
| terUnguarded | Agda.Termination.Monad |
| terUsableVars | Agda.Termination.Monad |
| terUseDotPatterns | Agda.Termination.Monad |
| terUserNames | Agda.Termination.Monad |
| terUseSizeLt | Agda.Termination.Monad |
| testLub | Agda.TypeChecking.SizedTypes.WarshallSolver |
| testSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| TexFileType | Agda.Syntax.Common |
| text | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| 3 (Function) | Agda.TypeChecking.Pretty |
| tgtNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| thd3 | Agda.Utils.Tuple |
| theBenchmark | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| theBlocker | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| theCallGraph | Agda.Termination.CallGraph |
| theConstraint | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| theCore | Agda.TypeChecking.Substitute |
| theCurrentFile | Agda.Interaction.Base |
| theDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| theEtaEquality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| theFixity | Agda.Syntax.Common |
| TheFlexRigMap | Agda.TypeChecking.Free.Lazy |
| theFlexRigMap | Agda.TypeChecking.Free.Lazy |
| TheInfo | Agda.TypeChecking.Coverage.SplitClause |
| theInteractionPoints | Agda.Interaction.Base |
| theKind | Agda.Syntax.Scope.Base |
| theMetaSet | Agda.TypeChecking.Free.Lazy |
| theNameRange | Agda.Syntax.Common |
| theNotation | Agda.Syntax.Common |
| thenReduce | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| thenTCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| theSize | Agda.Utils.Size |
| theSolution | Agda.TypeChecking.SizedTypes.Syntax |
| theTel | Agda.TypeChecking.Substitute |
| TheVarMap | Agda.TypeChecking.Free.Lazy |
| theVarMap | Agda.TypeChecking.Free.Lazy |
| TheVarMap' | Agda.TypeChecking.Free.Lazy |
| ThingsInScope | Agda.Syntax.Scope.Base |
| thingsInScope | Agda.Syntax.Scope.Base |
| ThingWithFixity | |
| 1 (Type/Class) | Agda.Syntax.Concrete, Agda.Syntax.Fixity |
| 2 (Data Constructor) | Agda.Syntax.Concrete, Agda.Syntax.Fixity |
| Three | |
| 1 (Type/Class) | Agda.Utils.Three |
| 2 (Data Constructor) | Agda.Utils.Three |
| throwImpossible | Agda.Utils.Impossible |
| throwMultipleFixityDecls | Agda.Syntax.Concrete.Fixity |
| throwMultiplePolarityPragmas | Agda.Syntax.Concrete.Fixity |
| tick | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics |
| tickICode | Agda.TypeChecking.Serialise.Base |
| tickMax | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics |
| tickN | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics |
| tIfThenElse | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TimeOut | |
| 1 (Type/Class) | Agda.Auto.Options |
| 2 (Data Constructor) | Agda.Auto.Options |
| Timings | Agda.Utils.Benchmark |
| timings | Agda.Utils.Benchmark |
| tInt | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TLam | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tLamView | Agda.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 |
| tLetView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TLit | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tlmodOf | Agda.Compiler.MAlonzo.Misc |
| TMAll | Agda.Auto.Convert |
| tMaybe | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| TMeta | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TMode | Agda.Auto.Convert |
| tmSort | Agda.Syntax.Internal |
| tmSSort | Agda.Syntax.Internal |
| tNegPlusK | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| to | Agda.Interaction.Highlighting.Range |
| toAbsN | Agda.TypeChecking.Names |
| toAbsName | Agda.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 |
| toAbstractWithoutImplicit | Agda.Syntax.Translation.ReflectedToAbstract |
| toAbstract_ | Agda.Syntax.Translation.ReflectedToAbstract |
| ToArgs | Agda.Interaction.JSON |
| toAscList | |
| 1 (Function) | Agda.Utils.BoolSet |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Utils.SmallSet |
| 4 (Function) | Agda.Utils.Trie |
| toAtoms | Agda.Interaction.Highlighting.Common |
| ToConcrete | Agda.Syntax.Translation.AbstractToConcrete |
| toConcrete | Agda.Syntax.Translation.AbstractToConcrete |
| toConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete |
| toConPatternInfo | Agda.Syntax.Internal |
| toCType | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| toDescList | Agda.Utils.VarSet |
| toDistinctAscendingLists | Agda.Utils.BiMap |
| toEncoding | Agda.Interaction.JSON |
| toEncoding1 | Agda.Interaction.JSON |
| toEncoding2 | Agda.Interaction.JSON |
| toEncodingList | Agda.Interaction.JSON |
| toFiniteList | Agda.Utils.IntSet.Infinite |
| toFinitePi | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| ToggleImplicitArgs | Agda.Interaction.Base |
| ToggleIrrelevantArgs | Agda.Interaction.Base |
| toIFile | Agda.Interaction.FindFile |
| toImpossible | Agda.Utils.Empty |
| ToJSON | Agda.Interaction.JSON |
| toJSON | Agda.Interaction.JSON |
| ToJSON1 | Agda.Interaction.JSON |
| toJSON1 | Agda.Interaction.JSON |
| ToJSON2 | Agda.Interaction.JSON |
| toJSON2 | Agda.Interaction.JSON |
| ToJSONKey | Agda.Interaction.JSON |
| toJSONKey | Agda.Interaction.JSON |
| ToJSONKeyFunction | Agda.Interaction.JSON |
| toJSONKeyList | Agda.Interaction.JSON |
| ToJSONKeyText | Agda.Interaction.JSON |
| ToJSONKeyValue | Agda.Interaction.JSON |
| toJSONList | Agda.Interaction.JSON |
| tok | Agda.Utils.Parser.MemoisedCPS |
| TokComment | Agda.Syntax.Parser.Tokens |
| TokDummy | Agda.Syntax.Parser.Tokens |
| Token | Agda.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 |
| tokenBased | Agda.Interaction.Highlighting.Precise |
| TokenLength | Agda.Syntax.Parser.Alex |
| tokensParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser |
| TokEOF | Agda.Syntax.Parser.Tokens |
| TokId | Agda.Syntax.Parser.Tokens |
| TokKeyword | Agda.Syntax.Parser.Tokens |
| TokLiteral | Agda.Syntax.Parser.Tokens |
| TokMarkup | Agda.Syntax.Parser.Tokens |
| TokQId | Agda.Syntax.Parser.Tokens |
| TokString | Agda.Syntax.Parser.Tokens |
| TokSymbol | Agda.Syntax.Parser.Tokens |
| TokTeX | Agda.Syntax.Parser.Tokens |
| toLazy | Agda.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.BiMap |
| 9 (Function) | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
| 10 (Function) | Agda.Utils.Favorites |
| 11 (Function) | Agda.Termination.CallMatrix |
| 12 (Function) | Agda.Termination.CallGraph |
| toList1 | Agda.Utils.List2 |
| toList1Either | Agda.Utils.List2 |
| toListOrderedBy | Agda.Utils.Trie |
| toLists | Agda.Termination.SparseMatrix |
| toLType | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| TOM | Agda.Auto.Convert |
| toMap | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
| tomy | Agda.Auto.Convert |
| tomyIneq | Agda.Auto.Convert |
| ToNLPat | Agda.TypeChecking.Rewriting.Clause |
| toNLPat | Agda.TypeChecking.Rewriting.Clause |
| TooFewArgumentsToPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TooManyFields | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TooManyFieldsWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TooManyFieldsWarning_ | Agda.Interaction.Options.Warnings |
| TooManyPolarities | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| toOrderings | Agda.Utils.PartialOrd |
| Top | Agda.TypeChecking.SizedTypes.Utils |
| tOp | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| top | Agda.TypeChecking.SizedTypes.Utils |
| topBlock | Agda.Syntax.Parser.Monad |
| topCohesion | Agda.Syntax.Common |
| TopCtx | Agda.Syntax.Fixity |
| TopK | Agda.Syntax.Concrete.Operators.Parser.Monad |
| TopLevel | |
| 1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract |
| 2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract |
| topLevelArg | Agda.TypeChecking.Injectivity |
| topLevelDecls | Agda.Syntax.Translation.ConcreteToAbstract |
| topLevelExpectedName | Agda.Syntax.Translation.ConcreteToAbstract |
| TopLevelInfo | |
| 1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract |
| 2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract |
| topLevelModuleDropper | Agda.TypeChecking.Errors |
| TopLevelModuleName | |
| 1 (Type/Class) | Agda.Syntax.TopLevelModuleName |
| 2 (Data Constructor) | Agda.Syntax.TopLevelModuleName |
| topLevelModuleName | |
| 1 (Function) | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Syntax.Translation.ConcreteToAbstract |
| 3 (Function) | Agda.Compiler.Common |
| TopLevelModuleNameParts | Agda.Syntax.TopLevelModuleName |
| topLevelModuleNameToQName | Agda.Syntax.TopLevelModuleName |
| topLevelPath | Agda.Syntax.Translation.ConcreteToAbstract |
| topLevelScope | Agda.Syntax.Translation.ConcreteToAbstract |
| topLevelTheThing | Agda.Syntax.Translation.ConcreteToAbstract |
| topModality | Agda.Syntax.Common |
| TopModule | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| TopOpenModule | Agda.Syntax.Scope.Monad |
| topoSort | Agda.Utils.Permutation |
| topoSortM | Agda.Utils.Permutation |
| topQuantity | Agda.Syntax.Common |
| topRelevance | Agda.Syntax.Common |
| topSearch | Agda.Auto.NarrowingSearch |
| topSort | Agda.Utils.Graph.TopSort |
| topVarOcc | Agda.TypeChecking.Free.Lazy |
| toSingleton | Agda.Utils.BoolSet |
| toSparseRows | Agda.Termination.SparseMatrix |
| toSplitPatterns | Agda.TypeChecking.Coverage.Match |
| toSplitPSubst | Agda.TypeChecking.Coverage.Match |
| toStrict | Agda.Utils.Maybe.Strict |
| toStringWithoutDotZero | Agda.Utils.Float |
| toSubscriptDigit | Agda.Utils.Suffix |
| total | |
| 1 (Function) | Agda.Utils.BoolSet |
| 2 (Function) | Agda.Utils.SmallSet |
| ToTerm | Agda.TypeChecking.Primitive |
| toTerm | Agda.TypeChecking.Primitive |
| toTermR | Agda.TypeChecking.Primitive |
| toTree | Agda.TypeChecking.Coverage.SplitTree |
| toTreeless | Agda.Compiler.Backend, Agda.Compiler.ToTreeless |
| toTrees | Agda.TypeChecking.Coverage.SplitTree |
| toVim | Agda.Interaction.Highlighting.Vim |
| toWeight | Agda.TypeChecking.SizedTypes.WarshallSolver |
| TPFn | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tPlusK | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TPOp | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TPrim | |
| 1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| trace | Agda.TypeChecking.SizedTypes.Utils |
| traceCall | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace |
| traceCallCPS | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace |
| traceCallM | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace |
| traceClosureCall | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace |
| traceDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| traceM | Agda.TypeChecking.SizedTypes.Utils |
| TraceS | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| traceS | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| traceSDoc | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| traceSLn | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| trailingWithPatterns | Agda.Syntax.Abstract.Pattern |
| trampoline | Agda.Utils.Function |
| trampolineM | Agda.Utils.Function |
| trampolineWhile | Agda.Utils.Function |
| trampolineWhileM | Agda.Utils.Function |
| transClos | Agda.TypeChecking.SizedTypes.WarshallSolver |
| transform | Agda.Compiler.Treeless.EliminateLiteralPatterns |
| transitiveClosure | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| transitiveReduction | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| translateBuiltins | Agda.Compiler.Treeless.Builtin |
| translateCompiledClauses | Agda.TypeChecking.RecordPatterns |
| translateRecordPatterns | Agda.TypeChecking.RecordPatterns |
| translateSplitTree | Agda.TypeChecking.RecordPatterns |
| TranspError | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| TranspOp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical |
| transpose | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 3 (Function) | Agda.Termination.SparseMatrix |
| transposeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| transpPathPTel' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| transpPathTel' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| transpSys | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| transpSysTel' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| transpTel | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| transpTel' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| Trav | Agda.Auto.NarrowingSearch |
| trav | Agda.Auto.NarrowingSearch |
| traverse' | Agda.Utils.Bag |
| traverseAPatternM | Agda.Syntax.Abstract.Pattern |
| traverseCPatternA | Agda.Syntax.Concrete.Pattern |
| traverseCPatternM | Agda.Syntax.Concrete.Pattern |
| traverseEither | Agda.Utils.Either |
| traverseExpr | |
| 1 (Function) | Agda.Syntax.Concrete.Generic |
| 2 (Function) | Agda.Syntax.Abstract.Views |
| TraverseExprFn | Agda.Syntax.Abstract.Views |
| TraverseExprRecFn | Agda.Syntax.Abstract.Views |
| traverseF | Agda.Utils.Functor |
| traversePatternM | Agda.Syntax.Internal.Pattern |
| traversePi | Agda.Auto.Typecheck |
| traverseTermM | Agda.Syntax.Internal.Generic |
| TravWith | Agda.Auto.NarrowingSearch |
| TrBr | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| treatAbstractly | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| treatAbstractly' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| treelessPrimName | Agda.Compiler.MAlonzo.Primitives |
| trFillPathPTel' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| trFillPathTel' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| trFillTel | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| trFillTel' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| Trie | |
| 1 (Type/Class) | Agda.Utils.Trie |
| 2 (Data Constructor) | Agda.Utils.Trie |
| TriedToCopyConstrainedPrim | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| trim | Agda.Utils.String |
| trimLineComment | Agda.Interaction.Library.Parse |
| trivial | Agda.TypeChecking.SizedTypes |
| trueCondition | Agda.TypeChecking.MetaVars |
| truncatedCallStack | Agda.Utils.CallStack |
| TruncateOffset | Agda.TypeChecking.SizedTypes.Syntax |
| truncateOffset | Agda.TypeChecking.SizedTypes.Syntax |
| tryCatch | Agda.Utils.Monad |
| tryConversion | Agda.TypeChecking.Conversion |
| tryConversion' | Agda.TypeChecking.Conversion |
| tryGetOpen | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open |
| tryMaybe | Agda.Utils.Monad |
| tryRecordType | Agda.TypeChecking.Records |
| tryResolveName | Agda.Syntax.Scope.Monad |
| trySizeUniv | Agda.TypeChecking.SizedTypes |
| tryStrengthen | Agda.Compiler.Treeless.Subst |
| tryTranspError | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| tset | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| tsize | Agda.Syntax.Internal |
| tSizeUniv | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| TSort | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TTerm | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TUnit | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| TUnreachable | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tUnreachable | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| tvaldecl | Agda.Compiler.MAlonzo.Compiler |
| TVar | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Two | Agda.Utils.Three |
| TwoElemArray | Agda.Interaction.JSON |
| TyApp | Agda.Utils.Haskell.Syntax |
| TyCon | Agda.Utils.Haskell.Syntax |
| TyForall | Agda.Utils.Haskell.Syntax |
| TyFun | Agda.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 |
| 6 (Type/Class) | Agda.Syntax.Abstract |
| Type' | Agda.Syntax.Internal |
| Type'' | Agda.Syntax.Internal |
| typeAnnotations | Agda.TypeChecking.Rules.LHS.Problem |
| typeArgsWithTel | Agda.TypeChecking.Substitute |
| typeArity | Agda.TypeChecking.Telescope |
| TypeCheck | Agda.Interaction.Imports |
| TypeCheckAction | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| typeCheckMain | Agda.Interaction.Imports |
| TypeChecks | Agda.Interaction.Highlighting.Precise |
| typeConArgsLeft | Agda.TypeChecking.Rules.LHS.Unify.Types |
| typeConArgsRight | Agda.TypeChecking.Rules.LHS.Unify.Types |
| typeConInjectAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
| TypeConInjectivity | Agda.TypeChecking.Rules.LHS.Unify.Types |
| typeConstructor | Agda.TypeChecking.Rules.LHS.Unify.Types |
| TypedAssign | Agda.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 |
| TypeDecl | Agda.Utils.Haskell.Syntax |
| typeElims | Agda.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 |
| 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 |
| typeError_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| typeInCurrent | Agda.Interaction.BasicOps |
| typeInMeta | Agda.Interaction.BasicOps |
| typeInType | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| TypeK | Agda.Compiler.MAlonzo.Misc |
| TypeLevelReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| typeLevelReductions | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| typeName | Agda.TypeChecking.Level |
| typeOfBV | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| typeOfConst | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| typeOfFlat | Agda.TypeChecking.Rules.Builtin.Coinduction |
| typeOfInf | Agda.TypeChecking.Rules.Builtin.Coinduction |
| typeOfMeta | Agda.Interaction.BasicOps |
| typeOfMeta' | Agda.Interaction.BasicOps |
| typeOfMetaMI | Agda.Interaction.BasicOps |
| typeOfSharp | Agda.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 |
| TypeSignatureOrInstanceBlock | Agda.Syntax.Concrete |
| typesOfHiddenMetas | Agda.Interaction.BasicOps |
| typesOfVisibleMetas | Agda.Interaction.BasicOps |
| Typing | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| TyVar | Agda.Utils.Haskell.Syntax |
| TyVarBind | Agda.Utils.Haskell.Syntax |