| ucheck | Idris.Core.Constraints |
| UConstraint | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| uconstraints | Idris.Core.Evaluate |
| UCs | Idris.Core.TT |
| UExp | Idris.Core.TT |
| UImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ULE | Idris.Core.TT |
| ULT | Idris.Core.TT |
| UN | Idris.Core.TT |
| unApply | Idris.Core.TT |
| Unchecked | Idris.Core.Evaluate |
| Unconditional | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| underline | Idris.Colours |
| Undo | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| undo | Idris.Core.Elaborate |
| unIdiom | Idris.DSL |
| unified | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifiedD | Idris.PartialEval |
| unify | Idris.Core.Unify |
| unifyLog | |
| 1 (Function) | Idris.Core.Elaborate |
| 2 (Function) | Idris.ParseExpr, Idris.Parser |
| unifylog | Idris.Core.ProofState, Idris.Core.Elaborate |
| UnifyProblems | Idris.Core.ProofState, Idris.Core.Elaborate |
| unifyProblems | Idris.Core.Elaborate |
| UnifyScope | Idris.Core.TT |
| uniqueBinders | Idris.Core.TT |
| uniqueName | Idris.Core.TT |
| uniqueNameCtxt | Idris.Core.Evaluate |
| uniqueNameFrom | Idris.Core.TT |
| unique_hole | Idris.Core.Elaborate |
| unique_hole' | Idris.Core.Elaborate |
| unitCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unitDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unitOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unitTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UniverseError | Idris.Core.TT |
| Universes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Unknown | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unList | Idris.Core.TT |
| unlit | Idris.Unlit |
| UnmatchedCase | Idris.Core.CaseTree |
| UnsetOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unusedpos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| unwrapFC | Idris.Core.TT |
| upd | Idris.Coverage |
| UPDATE | IRTS.Bytecode |
| updateAux | Idris.Core.Elaborate |
| updateContext | Idris.AbsSyntax |
| updateDef | Idris.Core.TT |
| updateN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| updateNs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| update_term | Idris.Core.Elaborate |
| Usage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| UseCodegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| used | Idris.UnusedArgs |
| usedArg | IRTS.Lang, IRTS.Defunctionalise |
| usedIn | IRTS.Lang, IRTS.Defunctionalise |
| usedNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| usedns | Idris.Core.ProofState, Idris.Core.Elaborate |
| 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 |
| UVal | Idris.Core.TT |
| UVar | Idris.Core.TT |