| T | IRTS.Bytecode |
| table | Idris.Parser.Ops, Idris.Parser |
| TacImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tacimpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tacN | Idris.Reflection |
| Tactic | Idris.Core.ProofState, Idris.Core.Elaborate |
| tactic | Idris.Parser.Expr, Idris.Parser |
| TacticArg | Idris.Parser.Expr, Idris.Parser |
| tactics | Idris.Parser.Expr, Idris.Parser |
| tacticsExpr | Idris.Parser.Expr, Idris.Parser |
| TAILCALL | IRTS.Bytecode |
| TargetCPU | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| targetCPU | |
| 1 (Function) | IRTS.CodegenCommon |
| 2 (Function) | Idris.AbsSyntax |
| TargetTriple | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| targetTriple | |
| 1 (Function) | IRTS.CodegenCommon |
| 2 (Function) | Idris.AbsSyntax |
| TC | Idris.Core.TT |
| TCheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TCImplementation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tcimplementation | Idris.Core.TT |
| tclift | Idris.Error |
| tcliftAt | Idris.Error |
| tcname | Idris.Core.TT |
| TCon | Idris.Core.TT |
| tcRecoverable | Idris.Elab.Term |
| tcReducible | Idris.Core.Evaluate |
| tctry | Idris.Error |
| tc_dictionary | Idris.Core.Evaluate |
| TDocStr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tempfile | Util.System |
| Term | Idris.Core.TT |
| TermElab | Idris.IdeMode |
| terminator | Idris.Parser.Helpers, Idris.Parser |
| TermNoImplicits | Idris.IdeMode |
| TermNormalise | Idris.IdeMode |
| TermPart | Idris.Core.TT |
| TermShowImplicits | Idris.IdeMode |
| TermSize | Idris.Core.TT |
| termsize | Idris.Core.TT |
| termSmallerThan | Idris.Core.TT |
| TermSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TestInline | Idris.REPL.Commands |
| testLib | Idris.Package |
| testPkg | Idris.Package |
| TEval | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TextFormatting | Idris.Core.TT |
| TextPart | Idris.Core.TT |
| TFail | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tfail | Idris.Core.TT |
| thead | Idris.Core.TT |
| TheWorld | Idris.Core.TT |
| thname | Idris.Core.ProofState, Idris.Core.Elaborate |
| throwError | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TI | Idris.Core.TT |
| TIData | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TIPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TISolution | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tldeclared | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Tmp | IRTS.Bytecode |
| tnull | Idris.Core.TT |
| toAlist | Idris.Core.TT |
| toBC | |
| 1 (Function) | IRTS.Bytecode |
| 2 (Function) | IRTS.BCImp |
| toCons | IRTS.Defunctionalise |
| toConsA | IRTS.Defunctionalise |
| toEither | Idris.AbsSyntax |
| toIBCFile | Idris.Package |
| TooManyArgs | Idris.Core.TT |
| TooManyArguments | Idris.Core.TT |
| TOPBASE | IRTS.Bytecode |
| Toplevel | Idris.Termination |
| toplevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| toplevelWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| toplevel_imp | Idris.Core.TT |
| toSExp | Idris.IdeMode |
| toTable | Idris.Parser.Ops, Idris.Parser |
| Total | Idris.Core.Evaluate |
| TotalFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Totality | Idris.Core.Evaluate |
| totality | Idris.Parser |
| TotCheck | Idris.REPL.Commands |
| totcheck | Idris.AbsSyntax |
| toValue | Idris.Core.Evaluate |
| TRACE | IRTS.CodegenCommon |
| traceWhen | Idris.Core.TT |
| transform | Idris.Parser |
| transformErr | Idris.Core.Elaborate |
| TransformInfo | Idris.REPL.Commands |
| transformPats | Idris.Transforms |
| transformPatsWith | Idris.Transforms |
| Trivial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| trivial | Idris.ProofSearch |
| trivial' | Idris.Elab.Term |
| trivialHoles | Idris.ProofSearch |
| trivialHoles' | Idris.Elab.Term |
| Try | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| try | Idris.Core.Elaborate |
| try' | Idris.Core.Elaborate |
| tryAll | Idris.Core.Elaborate |
| tryAll' | Idris.Core.Elaborate |
| tryCatch | Idris.Core.Elaborate |
| tryFullExpr | Idris.Parser.Expr, Idris.Parser |
| TryImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| tryLoadFn | Util.DynamicLinker |
| tryLoadLib | Util.DynamicLinker |
| tryWhen | Idris.Core.Elaborate |
| TSearch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TSeq | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TT | Idris.Core.TT |
| TTDecl | Idris.Core.Evaluate |
| ttDecls | IRTS.CodegenCommon |
| TType | Idris.Core.TT |
| tt_ctxt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| txt | Idris.Core.TT |
| TyDecl | Idris.Core.Evaluate |
| tyOptDeclList | Idris.Parser.Expr, Idris.Parser |
| Type | Idris.Core.TT |
| type1Doc | Idris.AbsSyntax |
| TypeCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TypeColour | Idris.Colours |
| typeColour | Idris.Colours |
| typeDeclList | Idris.Parser.Expr, Idris.Parser |
| typeDescription | Idris.AbsSyntax |
| typeExpr | Idris.Parser.Expr, Idris.Parser |
| TypeInfo | Idris.Core.TT |
| TypeInType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| typeInType | Idris.AbsSyntax |
| TypeOf | Idris.IdeMode |
| TypeOrTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| TypeOutput | Idris.Core.TT |
| TypeProviders | Idris.AbsSyntaxTree, Idris.AbsSyntax |