| ucheck | Idris.Core.Constraints |
| UConstraint | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| uconstraint | Idris.Core.TT |
| UCs | Idris.Core.TT |
| UExp | Idris.Core.TT |
| ufc | Idris.Core.TT |
| UImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ULE | Idris.Core.TT |
| ULT | Idris.Core.TT |
| UN | Idris.Core.TT |
| unApply | Idris.Core.TT |
| unApplyRaw | Idris.Reflection |
| unboundPi | Idris.Parser.Expr, Idris.Parser |
| unboundPiNoConstraint | Idris.Parser.Expr, Idris.Parser |
| Unchecked | |
| 1 (Data Constructor) | Idris.Docstrings |
| 2 (Data Constructor) | Idris.Core.Evaluate |
| Undefine | Idris.REPL.Commands |
| underline | Idris.Colours |
| UnderlineText | Idris.Core.TT |
| Undo | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| undo | Idris.Core.Elaborate |
| Unfocus | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unfold | Idris.Core.Evaluate |
| Unguarded | Idris.Termination |
| unIdiom | Idris.DSL |
| unified | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifiedD | Idris.PartialEval |
| Unify | Idris.Core.Unify |
| unify | Idris.Core.Unify |
| UnifyAll | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifyGoal | Idris.Core.ProofState, Idris.Core.Elaborate |
| unifyGoal | Idris.Core.Elaborate |
| unifyLog | |
| 1 (Function) | Idris.Core.Elaborate |
| 2 (Function) | Idris.Parser.Expr, Idris.Parser |
| unifylog | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifyProblems | Idris.Core.ProofState, Idris.Core.Elaborate |
| unifyProblems | Idris.Core.Elaborate |
| UnifyScope | Idris.Core.TT |
| UnifyTerms | Idris.Core.ProofState, Idris.Core.Elaborate |
| unifyTerms | Idris.Core.Elaborate |
| unify_all | Idris.Core.Elaborate |
| uniqueBinders | Idris.Core.TT |
| uniqueBindersCtxt | Idris.Core.Evaluate |
| UniqueError | Idris.Core.TT |
| UniqueKindError | Idris.Core.TT |
| uniqueName | Idris.Core.TT |
| uniqueNameCtxt | Idris.Core.Evaluate |
| uniqueNameFrom | Idris.Core.TT |
| uniqueNameSet | Idris.Core.TT |
| UniquenessTypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UniqueType | Idris.Core.TT |
| UniqueUse | Idris.Core.Typecheck |
| unique_hole | Idris.Core.Elaborate |
| unique_hole' | Idris.Core.Elaborate |
| unitCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unitTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Universe | Idris.Core.TT |
| UniverseError | Idris.Core.TT |
| Universes | Idris.REPL.Commands |
| Unknown | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UnknownImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UnknownImplicit | Idris.Core.TT |
| unList | Idris.Core.TT |
| unlit | Idris.Unlit |
| UnmatchedCase | Idris.Core.CaseTree |
| unquote | Idris.Parser.Expr, Idris.Parser |
| unrecoverable | Idris.Core.Unify |
| UnsetOpt | Idris.REPL.Commands |
| unwrapFC | Idris.Core.TT |
| upairCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| upairTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Updatable | Idris.Core.CaseTree |
| UPDATE | IRTS.Bytecode |
| updateAux | Idris.Core.Elaborate |
| updateContext | Idris.AbsSyntax |
| updateDef | Idris.Core.TT |
| updateIMethods | Idris.AbsSyntax |
| updateIState | Idris.AbsSyntax |
| updateN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| updateNs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| updatePS | Idris.Core.Elaborate |
| updateSolved | Idris.Core.ProofTerm |
| updateSolvedTerm | Idris.Core.ProofTerm |
| updateSolvedTerm' | Idris.Core.ProofTerm |
| updateSynMatch | Idris.Parser.Expr, Idris.Parser |
| updateSyntaxRules | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| update_term | Idris.Core.Elaborate |
| updsubst | Idris.Core.ProofTerm |
| UsageReason | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UseCodegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UseConsoleWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usedArg | IRTS.Lang, IRTS.Defunctionalise |
| usedIn | IRTS.Lang, IRTS.Defunctionalise |
| usedNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usedns | Idris.Core.ProofState, Idris.Core.Elaborate |
| usedpos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| useREPL | Idris.AbsSyntax |
| UseUndef | Idris.Core.Evaluate |
| Using | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| using | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usingDecl | Idris.Parser |
| usingDeclList | Idris.Parser |
| using_ | Idris.Parser |
| UType | Idris.Core.TT |
| UVal | Idris.Core.TT |
| UVar | Idris.Core.TT |