| U | Agda.TypeChecking.Rules.LHS.Unify |
| UId | Agda.Auto.Syntax |
| umodifyIORef | Agda.Auto.NarrowingSearch |
| unAbs | Agda.Syntax.Internal |
| 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 |
| undef | Agda.Compiler.JS.Parser |
| Undefined | Agda.Compiler.JS.Syntax |
| unDefName | Agda.TypeChecking.Test.Generators |
| underAbs | Agda.TypeChecking.MetaVars.Occurs |
| 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 |
| unElim | Agda.TypeChecking.Eliminators |
| unElimView | Agda.TypeChecking.Eliminators |
| 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 |
| unescape | Agda.Compiler.JS.Pretty |
| unescapes | Agda.Compiler.JS.Pretty |
| UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unExprView | Agda.Syntax.Concrete.Operators.Parser |
| unflattenTel | Agda.TypeChecking.Telescope |
| unfold | Agda.TypeChecking.MetaVars.Occurs |
| unfoldCorecursion | Agda.TypeChecking.CompiledClause.Match |
| unfoldDefinition | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| UnfoldStrategy | Agda.TypeChecking.MetaVars.Occurs |
| unfreezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| unGraph | Agda.Utils.Graph |
| uniConstr | Agda.TypeChecking.Rules.LHS.Unify |
| Unifiable | Agda.TypeChecking.Rules.LHS.Unify |
| unifiable | Agda.Compiler.Epic.Injection |
| UnificationResult | Agda.TypeChecking.Rules.LHS.Unify |
| Unifies | Agda.TypeChecking.Rules.LHS.Unify |
| Unify | Agda.TypeChecking.Rules.LHS.Unify |
| unify | Agda.Compiler.Epic.Injection |
| UnifyEnv | 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 |
| UnifyMayPostpone | Agda.TypeChecking.Rules.LHS.Unify |
| UnifyOutput | 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.VarSet |
| 2 (Function) | Agda.Utils.Graph |
| 3 (Function) | Agda.Utils.Trie |
| 4 (Function) | Agda.Compiler.JS.Substitution |
| 5 (Function) | Agda.Termination.CallGraph |
| unionConstraints | Agda.Compiler.Epic.Injection |
| unions | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.Graph |
| unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| unionWithM | Agda.Utils.Map |
| uniqBy | Agda.Utils.List |
| 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.Substitute |
| 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 |
| Unquote | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Type/Class) | Agda.TypeChecking.Quote |
| unquote | Agda.TypeChecking.Quote |
| unquoteFailed | Agda.TypeChecking.Quote |
| unquoteFailedGeneric | Agda.TypeChecking.Quote |
| unquoteH | Agda.TypeChecking.Quote |
| unquoteN | Agda.TypeChecking.Quote |
| UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnreducedLevel | Agda.Syntax.Internal |
| unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc |
| unsafePragmaOptions | Agda.Interaction.Options |
| unScope | Agda.TypeChecking.Rules.Term |
| 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 |
| unusableRelevance | Agda.TypeChecking.Irrelevance |
| 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 |
| ureadIORef | Agda.Auto.NarrowingSearch |
| ureadmodifyIORef | Agda.Auto.NarrowingSearch |
| UReduce | Agda.TypeChecking.Rules.LHS.Unify |
| ureduce | Agda.TypeChecking.Rules.LHS.Unify |
| usage | Agda.Interaction.Options |
| usedSeed | Agda.Utils.QuickCheck |
| usedSize | Agda.Utils.QuickCheck |
| useInjectivity | Agda.TypeChecking.Injectivity |
| UselessAbstract | Agda.Syntax.Concrete.Definitions |
| UselessPrivate | Agda.Syntax.Concrete.Definitions |
| 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 |
| Uses | Agda.Compiler.JS.Syntax |
| uses | Agda.Compiler.JS.Syntax |
| Using | Agda.Syntax.Concrete |
| UsingOrHiding | Agda.Syntax.Concrete |
| usingOrHiding | Agda.Syntax.Concrete |
| USt | Agda.TypeChecking.Rules.LHS.Unify |
| uwriteIORef | Agda.Auto.NarrowingSearch |