| U | |
| 1 (Type/Class) | Agda.TypeChecking.Serialise.Base |
| 2 (Data Constructor) | Agda.TypeChecking.Serialise.Base |
| uglyShowName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| UId | Agda.Auto.Syntax |
| umodifyIORef | Agda.Auto.NarrowingSearch |
| unAbs | Agda.Syntax.Internal |
| unambiguous | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| unAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| unAppView | Agda.Syntax.Abstract.Views |
| unArg | Agda.Syntax.Common |
| unBind | Agda.Syntax.Abstract |
| unbindVariable | Agda.Syntax.Scope.Monad |
| UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unblockedTester | Agda.TypeChecking.MetaVars |
| unBrave | Agda.Syntax.Internal |
| unBruijn | Agda.TypeChecking.CompiledClause.Compile |
| UnconfirmedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| uncons | Agda.Utils.List |
| unConstV | Agda.TypeChecking.Level |
| uncurry3 | Agda.Utils.Tuple |
| uncurry4 | Agda.Utils.Tuple |
| uncurrys | Agda.Utils.TypeLevel |
| unDeepSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Undefined | Agda.Compiler.JS.Syntax |
| underAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| underAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| underAbstraction' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| underAbstractionAbs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| underAbstractionAbs' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| underAbstraction_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Underapplied | Agda.Syntax.Internal |
| underBinder | Agda.TypeChecking.Free.Lazy |
| underBinder' | Agda.TypeChecking.Free.Lazy |
| underConstructor | Agda.TypeChecking.Free.Lazy |
| underFlexRig | Agda.TypeChecking.Free.Lazy |
| UnderInf | Agda.TypeChecking.Positivity.Occurrence |
| UnderLambda | |
| 1 (Type/Class) | Agda.Compiler.Treeless.Subst |
| 2 (Data Constructor) | Agda.Compiler.Treeless.Subst |
| underLambda | Agda.Compiler.Treeless.Subst |
| underLambdas | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| underlyingRange | Agda.TypeChecking.Serialise.Instances.Common |
| underModality | Agda.TypeChecking.Free.Lazy |
| underRelevance | Agda.TypeChecking.Free.Lazy |
| Underscore | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| underscore | Agda.Syntax.Common |
| Undo | Agda.Auto.NarrowingSearch |
| unDom | Agda.Syntax.Internal |
| unDrop | Agda.Utils.Permutation |
| unEl | Agda.Syntax.Internal |
| unequal | Agda.Auto.Typecheck |
| UnequalBecauseOfUniverseConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnequalCohesion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnequalLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnequalQuantity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnequalRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unequals | Agda.Auto.Typecheck |
| UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnequalTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unescape | Agda.Compiler.JS.Pretty |
| unescapes | Agda.Compiler.JS.Pretty |
| UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unExprView | Agda.Syntax.Concrete.Operators.Parser |
| unflattenTel | Agda.TypeChecking.Telescope |
| unfold | Agda.TypeChecking.MetaVars.Occurs |
| unfoldB | Agda.TypeChecking.MetaVars.Occurs |
| unfoldCorecursion | Agda.TypeChecking.Reduce |
| unfoldCorecursionE | Agda.TypeChecking.Reduce |
| unfoldDefinition | Agda.TypeChecking.Reduce |
| unfoldDefinition' | Agda.TypeChecking.Reduce |
| unfoldDefinitionE | Agda.TypeChecking.Reduce |
| unfoldDefinitionStep | Agda.TypeChecking.Reduce |
| unfoldInlined | Agda.TypeChecking.Reduce |
| UnfoldStrategy | Agda.TypeChecking.MetaVars.Occurs |
| UnFreezeMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unfreezeMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unfreezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unfreezeMetas' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unglueTranspGlue | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| Unguarded | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| unguardedRecord | Agda.TypeChecking.Records |
| UnGuardedRhs | Agda.Utils.Haskell.Syntax |
| unguardedVars | Agda.TypeChecking.Free |
| UnicodeOk | Agda.Interaction.Options.IORefs |
| UnicodeOrAscii | Agda.Interaction.Options.IORefs |
| unicodeOrAscii | Agda.Interaction.Options.IORefs |
| UnificationFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnificationResult | Agda.TypeChecking.Rules.LHS.Unify |
| UnificationResult' | Agda.TypeChecking.Rules.LHS.Unify |
| UnificationStuck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Unifies | Agda.TypeChecking.Rules.LHS.Unify |
| Unify | Agda.Auto.CaseSplit |
| unify | Agda.Auto.CaseSplit |
| unify' | Agda.Auto.CaseSplit |
| UnifyConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnifyCycle | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unifyElims | Agda.TypeChecking.IApplyConfluence |
| unifyElimsMeta | Agda.TypeChecking.IApplyConfluence |
| unifyexp | Agda.Auto.CaseSplit |
| UnifyIndices | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| unifyIndices | Agda.TypeChecking.Rules.LHS.Unify |
| UnifyIndicesNotVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnifyRecursiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnifyReflexiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnifyUnusableModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unifyVar | Agda.Auto.CaseSplit |
| UninstantiatedDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| union | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.BiMap |
| 3 (Function) | Agda.Utils.Bag |
| 4 (Function) | Agda.Utils.SmallSet |
| 5 (Function) | Agda.Utils.Trie |
| 6 (Function) | Agda.Compiler.JS.Substitution |
| 7 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 8 (Function) | Agda.Utils.Favorites |
| 9 (Function) | Agda.Termination.CallMatrix |
| 10 (Function) | Agda.Termination.CallGraph |
| unionCompared | Agda.Utils.Favorites |
| unionMaybeWith | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| unions | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unionsMaybeWith | Agda.Utils.Maybe |
| unionsWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| unionWith | |
| 1 (Function) | Agda.Utils.Trie |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| uniqOn | Agda.Utils.List |
| unitCompose | Agda.TypeChecking.SizedTypes.Utils |
| unit_con | Agda.Utils.Haskell.Syntax |
| univar | Agda.Auto.SearchControl |
| UniverseCheck | Agda.Syntax.Common |
| univInf | Agda.TypeChecking.Substitute |
| UnivSort | Agda.Syntax.Internal |
| univSort | Agda.TypeChecking.Substitute |
| univSort' | Agda.TypeChecking.Substitute |
| UnkindedVar | Agda.Utils.Haskell.Syntax |
| Unknown | |
| 1 (Data Constructor) | Agda.Termination.Order |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| unknown | Agda.Termination.Order |
| UnknownField | Agda.Interaction.Library.Parse |
| UnknownFixityInMixfixDecl | Agda.Syntax.Concrete.Definitions |
| UnknownFixityInMixfixDecl_ | Agda.Interaction.Options.Warnings |
| unknownFreeVariables | Agda.Syntax.Common |
| UnknownFVs | Agda.Syntax.Common |
| UnknownHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnknownName | Agda.Syntax.Scope.Base |
| UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions |
| UnknownNamesInFixityDecl_ | Agda.Interaction.Options.Warnings |
| UnknownNamesInPolarityPragmas | Agda.Syntax.Concrete.Definitions |
| UnknownNamesInPolarityPragmas_ | Agda.Interaction.Options.Warnings |
| UnknownS | Agda.Syntax.Reflected |
| UnknownSort | Agda.Auto.Syntax |
| unlabelPatVars | Agda.Syntax.Internal.Pattern |
| unless | Agda.Utils.Monad |
| unlessDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unlessM | Agda.Utils.Monad |
| unlessNull | Agda.Utils.Null |
| unlessNullM | Agda.Utils.Null |
| unLevel | Agda.TypeChecking.Level |
| unLevelAtom | Agda.TypeChecking.Substitute |
| unlevelWithKit | Agda.TypeChecking.Level |
| unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unLvl | Agda.TypeChecking.Primitive |
| unM | Agda.Termination.SparseMatrix |
| unMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unName | Agda.TypeChecking.Names |
| unnamed | Agda.Syntax.Common |
| unnamedArg | Agda.Syntax.Common |
| unNat | Agda.TypeChecking.Primitive |
| unnumberPatVars | Agda.Syntax.Internal.Pattern |
| unpackUnquoteM | Agda.TypeChecking.Unquote |
| unPlusV | Agda.TypeChecking.Level |
| unPM | Agda.Syntax.Parser |
| unProjView | Agda.TypeChecking.ProjectionLike |
| unPureConversionT | Agda.TypeChecking.Conversion.Pure |
| unqhname | Agda.Compiler.MAlonzo.Misc |
| UnQual | Agda.Utils.Haskell.Syntax |
| 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.Unquote |
| unquote | Agda.TypeChecking.Unquote |
| UnquoteDecl | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| UnquoteDef | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| UnquoteDefRequiresSignature | Agda.Syntax.Concrete.Definitions |
| UnquoteError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnquoteFailed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnquoteFlags | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnquoteM | Agda.TypeChecking.Unquote |
| unquoteM | Agda.TypeChecking.Rules.Term |
| unquoteN | Agda.TypeChecking.Unquote |
| unquoteNormalise | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unquoteNString | Agda.TypeChecking.Unquote |
| UnquotePanic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnquoteRes | Agda.TypeChecking.Unquote |
| UnquoteState | Agda.TypeChecking.Unquote |
| unquoteString | Agda.TypeChecking.Unquote |
| UnquoteTactic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unquoteTactic | Agda.TypeChecking.Rules.Term |
| unquoteTCM | Agda.TypeChecking.Unquote |
| unquoteTop | Agda.TypeChecking.Rules.Decl |
| unranged | Agda.Syntax.Common |
| Unreachable | |
| 1 (Data Constructor) | Agda.Utils.Impossible |
| 2 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnreachableClauses_ | Agda.Interaction.Options.Warnings |
| UnreducedLevel | Agda.Syntax.Internal |
| unreducedLevel | Agda.Syntax.Internal |
| unReduceM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Unrelated | Agda.Syntax.Common |
| unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc |
| unsafeDeclarationWarning | Agda.Syntax.Concrete.Definitions |
| unsafeEscapeContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unsafeInTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unsafeModifyContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unsafePragmaOptions | Agda.Interaction.Options |
| unScope | Agda.Syntax.Abstract.Views |
| unSingleLevel | Agda.TypeChecking.Level |
| unSingleLevels | Agda.TypeChecking.Level |
| unSizeExpr | Agda.TypeChecking.SizedTypes.Solve |
| unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnsolvedConstraint | Agda.Interaction.Highlighting.Precise |
| UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnsolvedConstraints_ | Agda.Interaction.Options.Warnings |
| UnsolvedInteractionMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnsolvedInteractionMetas_ | Agda.Interaction.Options.Warnings |
| UnsolvedMeta | Agda.Interaction.Highlighting.Precise |
| UnsolvedMetaVariables | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UnsolvedMetaVariables_ | Agda.Interaction.Options.Warnings |
| unsolvedWarnings | Agda.Interaction.Options.Warnings |
| unSpine | Agda.Syntax.Internal |
| unSpine' | Agda.Syntax.Internal |
| unStr | Agda.Utils.String |
| unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Unused | Agda.TypeChecking.Positivity.Occurrence |
| unusedVar | Agda.Termination.Monad |
| UnusedVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| unVersionView | Agda.Interaction.Library |
| unzip | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| unzipMaybe | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| unzipWith | Agda.Utils.List |
| update | Agda.Utils.AssocList |
| update1 | Agda.Utils.Update |
| update2 | Agda.Utils.Update |
| updateAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateAt | |
| 1 (Function) | Agda.Utils.List |
| 2 (Function) | Agda.Utils.AssocList |
| updateBenchmark | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateBenchmarkingStatus | Agda.TypeChecking.Monad.Benchmark |
| updateCompiledClauses | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateCovering | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateDefArgOccurrences | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateDefBlocked | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateDefCompiledRep | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateDefCopatternLHS | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateDefinitions | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateDefPolarity | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateDefType | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateFunClauses | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateHead | Agda.Utils.List |
| updateHeads | Agda.TypeChecking.Injectivity |
| updateInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateInteractionPointsAfter | Agda.Interaction.InteractionTop |
| updateLast | Agda.Utils.List |
| updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateMetaVarTCM | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateNamedArg | Agda.Syntax.Common |
| updateNamedArgA | Agda.Syntax.Common |
| updatePersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateProblemRest | Agda.TypeChecking.Rules.LHS.ProblemRest |
| updatePtr | Agda.Utils.Pointer |
| updatePtrM | Agda.Utils.Pointer |
| Updater | Agda.Utils.Update |
| Updater1 | Agda.Utils.Update |
| updater1 | Agda.Utils.Update |
| Updater2 | Agda.Utils.Update |
| updater2 | Agda.Utils.Update |
| UpdaterT | Agda.Utils.Update |
| updates1 | Agda.Utils.Update |
| updates2 | Agda.Utils.Update |
| updateScopeLocals | Agda.Syntax.Scope.Base |
| updateScopeNameSpaces | Agda.Syntax.Scope.Base |
| updateScopeNameSpacesM | Agda.Syntax.Scope.Base |
| updateTheDef | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| updateVarsToBind | Agda.Syntax.Scope.Base |
| upperBounds | Agda.TypeChecking.SizedTypes.WarshallSolver |
| ureadIORef | Agda.Auto.NarrowingSearch |
| ureadmodifyIORef | Agda.Auto.NarrowingSearch |
| usableCohesion | Agda.Syntax.Common |
| usableMod | Agda.TypeChecking.Irrelevance |
| UsableModality | Agda.TypeChecking.Irrelevance |
| usableModality | Agda.Syntax.Common |
| usableQuantity | Agda.Syntax.Common |
| usableRel | Agda.TypeChecking.Irrelevance |
| UsableRelevance | Agda.TypeChecking.Irrelevance |
| usableRelevance | Agda.Syntax.Common |
| UsableSizeVars | Agda.Termination.Monad |
| usableSizeVars | Agda.Termination.Monad |
| usage | Agda.Interaction.Options |
| usageWarning | Agda.Interaction.Options.Warnings |
| use | Agda.Utils.Lens |
| useConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| usedArguments | Agda.Compiler.Treeless.Unused |
| useDefaultFixity | Agda.Syntax.Notation |
| UseEverything | Agda.Syntax.Common |
| UseForce | Agda.Interaction.Base |
| useInjectivity | Agda.TypeChecking.Injectivity |
| UselessAbstract | Agda.Syntax.Concrete.Definitions |
| UselessAbstract_ | Agda.Interaction.Options.Warnings |
| UselessInline | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UselessInline_ | Agda.Interaction.Options.Warnings |
| UselessInstance | Agda.Syntax.Concrete.Definitions |
| UselessInstance_ | Agda.Interaction.Options.Warnings |
| UselessPrivate | Agda.Syntax.Concrete.Definitions |
| UselessPrivate_ | Agda.Interaction.Options.Warnings |
| UselessPublic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UselessPublic_ | Agda.Interaction.Options.Warnings |
| useNamesFromPattern | Agda.TypeChecking.Rules.LHS.ProblemRest |
| useNamesFromProblemEqs | Agda.TypeChecking.Rules.LHS.ProblemRest |
| useOriginFrom | Agda.TypeChecking.Rules.LHS.ProblemRest |
| usePatOrigin | Agda.TypeChecking.Substitute |
| usePatternInfo | Agda.TypeChecking.Substitute |
| useR | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| userNamed | Agda.Syntax.Common |
| UserWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UserWarning_ | Agda.Interaction.Options.Warnings |
| UserWritten | Agda.Syntax.Common |
| Uses | Agda.Compiler.JS.Syntax |
| uses | Agda.Compiler.JS.Syntax |
| usesCopatterns | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| useScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| UseShowInstance | Agda.Interaction.Base |
| useTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| useTerPragma | Agda.TypeChecking.Rules.Def |
| Using | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| using | Agda.Syntax.Common |
| Using' | Agda.Syntax.Common |
| UsingOnly | Agda.Syntax.Scope.Base |
| UsingOrHiding | Agda.Syntax.Scope.Base |
| usingOrHiding | Agda.Syntax.Scope.Base |
| usualWarnings | Agda.Interaction.Options.Warnings |
| uwriteIORef | Agda.Auto.NarrowingSearch |