| U | Agda.TypeChecking.Rules.LHS.Unify |
| UId | Agda.Auto.Syntax |
| umodifyIORef | Agda.Auto.NarrowingSearch |
| unAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| unAppView | Agda.Syntax.Abstract.Views |
| unArg | Agda.Syntax.Common |
| UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unblockedTester | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| unConName | Agda.TypeChecking.Test.Generators |
| uncurry3 | Agda.Utils.Tuple |
| unDefName | Agda.TypeChecking.Test.Generators |
| underAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| underAbstraction_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| Underscore | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| underscore | Agda.Syntax.Concrete.Pretty |
| Undo | Agda.Auto.NarrowingSearch |
| unEl | Agda.Syntax.Internal |
| unequal | Agda.Auto.Typecheck |
| UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unequals | Agda.Auto.Typecheck |
| UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalTelescopes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unExprView | Agda.Syntax.Concrete.Operators.Parser |
| unflattenTel | Agda.TypeChecking.Telescope |
| unfoldCorecursion | Agda.TypeChecking.CompiledClause.Match |
| unfoldDefinition | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| unGraph | Agda.Utils.Graph |
| uniConstr | Agda.TypeChecking.Rules.LHS.Unify |
| unification | Agda.Compiler.Epic.Forcing |
| UnificationResult | Agda.TypeChecking.Rules.LHS.Unify |
| Unifies | Agda.TypeChecking.Rules.LHS.Unify |
| Unify | Agda.TypeChecking.Rules.LHS.Unify |
| UnifyException | Agda.TypeChecking.Rules.LHS.Unify |
| unifyexp | Agda.Auto.CaseSplit |
| unifyI | Agda.Compiler.Epic.Forcing |
| unifyIndices | Agda.TypeChecking.Rules.LHS.Unify |
| unifyIndices_ | Agda.TypeChecking.Rules.LHS.Unify |
| UnifyState | Agda.TypeChecking.Rules.LHS.Unify |
| UninstantiatedDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UninstantiatedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| union | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Utils.Trie |
| 3 (Function) | Agda.Termination.CallGraph |
| unions | Agda.Utils.Graph |
| unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| unionWithM | Agda.Utils.Map |
| uniSub | Agda.TypeChecking.Rules.LHS.Unify |
| UNIT | Agda.Compiler.Epic.AuxAST |
| univar | Agda.Auto.SearchControl |
| Unknown | Agda.TypeChecking.Positivity |
| unknown | Agda.Termination.CallGraph |
| UnknownName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions |
| UnknownSort | Agda.Auto.Syntax |
| unlessM | Agda.Utils.Monad |
| unLevelAtom | Agda.TypeChecking.Level |
| unLevelView | Agda.TypeChecking.Level |
| unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| unLvl | Agda.TypeChecking.Primitive |
| unnamed | Agda.Syntax.Common |
| unNat | Agda.TypeChecking.Primitive |
| unNoType | Agda.TypeChecking.Test.Generators |
| unqhname | Agda.Compiler.MAlonzo.Misc |
| unqname | Agda.Compiler.Epic.CompileState |
| unqualify | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc |
| unSizedList | Agda.TypeChecking.Test.Generators |
| unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unsolvedConstraints | Agda.Interaction.Imports |
| UnsolvedMeta | Agda.Interaction.Highlighting.Precise |
| UnsolvedMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unsolvedMetaVariables | Agda.Interaction.Imports |
| unStr | Agda.TypeChecking.Primitive |
| unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unUnify | Agda.TypeChecking.Rules.LHS.Unify |
| Unused | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unVarName | Agda.TypeChecking.Test.Generators |
| unYesType | Agda.TypeChecking.Test.Generators |
| updateMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| updatePtr | Agda.Utils.Pointer |
| updateWithConstructorRanges | Agda.TypeChecking.With |
| ureadIORef | Agda.Auto.NarrowingSearch |
| ureadmodifyIORef | Agda.Auto.NarrowingSearch |
| ureduce | Agda.TypeChecking.Rules.LHS.Unify |
| usage | Agda.Interaction.Options |
| usedSeed | Agda.Utils.QuickCheck |
| usedSize | Agda.Utils.QuickCheck |
| useInjectivity | Agda.TypeChecking.Injectivity |
| UseLit | Agda.TypeChecking.Test.Generators |
| useLitChar | Agda.TypeChecking.Test.Generators |
| UseLiterals | Agda.TypeChecking.Test.Generators |
| useLitFloat | Agda.TypeChecking.Test.Generators |
| useLitInt | Agda.TypeChecking.Test.Generators |
| useLitString | Agda.TypeChecking.Test.Generators |
| useNamesFromPattern | Agda.TypeChecking.Rules.LHS |
| Using | Agda.Syntax.Concrete |
| UsingOrHiding | Agda.Syntax.Concrete |
| usingOrHiding | Agda.Syntax.Concrete |
| USt | Agda.TypeChecking.Rules.LHS.Unify |
| uwriteIORef | Agda.Auto.NarrowingSearch |