| 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 | |
| 1 (Function) | Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract.Views |
| unArg | Agda.Syntax.Common |
| unBind | Agda.Syntax.Abstract |
| unbindVariable | Agda.Syntax.Scope.Monad |
| UnBlock | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unblockedTester | Agda.TypeChecking.MetaVars |
| unblockMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| UnblockOnAll | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockOnAll | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockOnAllMetas | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockOnAllMetasIn | Agda.Syntax.Internal.MetaVars |
| UnblockOnAny | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockOnAny | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockOnAnyMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockOnAnyMetaIn | Agda.Syntax.Internal.MetaVars |
| unblockOnEither | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| UnblockOnMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockOnMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| UnblockOnProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockOnProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unblockProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| unBlockT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unBrave | Agda.Syntax.Internal |
| unBruijn | Agda.TypeChecking.CompiledClause.Compile |
| UnconfirmedReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| uncons | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.List |
| unConstV | Agda.TypeChecking.Level |
| uncurry3 | Agda.Utils.Tuple |
| uncurry4 | Agda.Utils.Tuple |
| uncurrys | Agda.Utils.TypeLevel |
| unDeepSizeView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| Undefined | Agda.Compiler.JS.Syntax |
| underAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| underAbstraction | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| underAbstraction' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| underAbstractionAbs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| underAbstractionAbs' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| underAbstraction_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| UnderAddition | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| Underapplied | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| underBinder | Agda.TypeChecking.Free.Lazy |
| underBinder' | Agda.TypeChecking.Free.Lazy |
| UnderComposition | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| UnequalCohesion | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnequalLevel | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnequalQuantity | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnequalRelevance | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unequals | Agda.Auto.Typecheck |
| UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnequalTypes | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unescape | Agda.Compiler.JS.Pretty |
| unescapes | Agda.Compiler.JS.Pretty |
| UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unExprView | Agda.Syntax.Concrete.Operators.Parser |
| unflattenTel | Agda.TypeChecking.Telescope |
| unfold | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | 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 |
| unfoldr | Agda.Utils.List1 |
| UnfoldStrategy | Agda.TypeChecking.MetaVars.Occurs |
| UnFreezeMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| unfreezeMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| unfreezeMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| unglueTranspGlue | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| Unguarded | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| unguardedRecord | Agda.TypeChecking.Records |
| UnGuardedRhs | Agda.Utils.Haskell.Syntax |
| unguardedVars | Agda.TypeChecking.Free |
| UnicodeOk | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options |
| UnicodeOrAscii | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options |
| UnicodeSubscript | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| UnificationFailure | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnificationResult | Agda.TypeChecking.Rules.LHS.Unify |
| UnificationResult' | Agda.TypeChecking.Rules.LHS.Unify |
| UnificationStuck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Unifies | Agda.TypeChecking.Rules.LHS.Unify |
| UnifiesTo | Agda.Auto.CaseSplit |
| Unify | Agda.Auto.CaseSplit |
| unify | Agda.Auto.CaseSplit |
| unify' | Agda.Auto.CaseSplit |
| UnifyBlocked | Agda.TypeChecking.Rules.LHS.Unify |
| UnifyConflict | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnifyCycle | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| UnifyRecursiveEq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnifyReflexiveEq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnifyStuck | Agda.TypeChecking.Rules.LHS.Unify |
| UnifyUnusableModality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unifyVar | Agda.Auto.CaseSplit |
| UninstantiatedDotPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| union | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Utils.SmallSet |
| 4 (Function) | Agda.Utils.Trie |
| 5 (Function) | Agda.Utils.List1 |
| 6 (Function) | Agda.Utils.BiMap |
| 7 (Function) | Agda.Compiler.JS.Substitution |
| 8 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 9 (Function) | Agda.Utils.Favorites |
| 10 (Function) | Agda.Termination.CallMatrix |
| 11 (Function) | Agda.Termination.CallGraph |
| unionCompared | Agda.Utils.Favorites |
| unionMaybeWith | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| unionPrecondition | Agda.Utils.BiMap |
| unions | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| unionSignatures | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| 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 |
| uniqueInt | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| unitCohesion | Agda.Syntax.Common |
| unitCompose | Agda.TypeChecking.SizedTypes.Utils |
| unitModality | Agda.Syntax.Common |
| unitQuantity | Agda.Syntax.Common |
| unitRelevance | Agda.Syntax.Common |
| unit_con | Agda.Utils.Haskell.Syntax |
| univar | Agda.Auto.SearchControl |
| UniverseCheck | Agda.Syntax.Common |
| universeCheck | Agda.Syntax.Concrete.Definitions.Types |
| universeCheckPragma | Agda.Syntax.Concrete.Definitions.Monad |
| UnivSort | Agda.Syntax.Internal |
| univSort | Agda.TypeChecking.Substitute |
| univSort' | Agda.TypeChecking.Substitute |
| UnkindedVar | Agda.Utils.Haskell.Syntax |
| Unknown | |
| 1 (Data Constructor) | Agda.Interaction.Options.Warnings |
| 2 (Data Constructor) | Agda.Termination.Order |
| 3 (Data Constructor) | Agda.Syntax.Reflected |
| unknown | Agda.Termination.Order |
| UnknownError | Agda.Interaction.ExitCode |
| UnknownField | Agda.Interaction.Library.Base |
| UnknownFixityInMixfixDecl | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| UnknownFixityInMixfixDecl_ | Agda.Interaction.Options.Warnings |
| unknownFreeVariables | Agda.Syntax.Common |
| UnknownFVs | Agda.Syntax.Common |
| UnknownHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnknownName | Agda.Syntax.Scope.Base |
| UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| UnknownNamesInFixityDecl_ | Agda.Interaction.Options.Warnings |
| UnknownNamesInPolarityPragmas | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| UnknownNamesInPolarityPragmas_ | Agda.Interaction.Options.Warnings |
| UnknownS | Agda.Syntax.Reflected |
| UnknownSort | Agda.Auto.Syntax |
| unlabelPatVars | Agda.Syntax.Internal.Pattern |
| unlamView | Agda.TypeChecking.Substitute |
| unless | Agda.Utils.Monad |
| unlessDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unlessM | Agda.Utils.Monad |
| unlessNull | |
| 1 (Function) | Agda.Utils.Null |
| 2 (Function) | Agda.Utils.List1 |
| unlessNullM | Agda.Utils.Null |
| unLevel | Agda.TypeChecking.Level |
| unlevelWithKit | Agda.TypeChecking.Level |
| unlistenToMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| unLvl | Agda.TypeChecking.Primitive |
| unM | Agda.Termination.SparseMatrix |
| unmapListT | Agda.Utils.ListT |
| unMaxView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| unName | Agda.TypeChecking.Names |
| unnamed | Agda.Syntax.Common |
| unnamedArg | Agda.Syntax.Common |
| unNat | Agda.TypeChecking.Primitive |
| unNice | Agda.Syntax.Concrete.Definitions.Monad |
| unNLM | Agda.TypeChecking.Rewriting.NonLinMatch |
| 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.Errors |
| UnquoteError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnquoteFailed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnquoteFlags | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnquoteM | Agda.TypeChecking.Unquote |
| unquoteM | Agda.TypeChecking.Rules.Term |
| unquoteN | Agda.TypeChecking.Unquote |
| unquoteNormalise | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unquoteNString | Agda.TypeChecking.Unquote |
| UnquotePanic | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnquoteRes | Agda.TypeChecking.Unquote |
| UnquoteState | Agda.TypeChecking.Unquote |
| unquoteString | Agda.TypeChecking.Unquote |
| UnquoteTactic | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| UnreachableClauses_ | Agda.Interaction.Options.Warnings |
| unReduceM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Unrelated | Agda.Syntax.Common |
| unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc |
| unsafeDeclarationWarning | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| unsafeDeclarationWarning' | Agda.Syntax.Concrete.Definitions.Errors |
| unsafeEscapeContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| unsafeInTopContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| unsafeModifyContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| unsafePragmaOptions | Agda.Interaction.Options |
| unsafeSetUnicodeOrAscii | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
| unScope | Agda.Syntax.Abstract.Views |
| unSingleLevel | Agda.TypeChecking.Level |
| unSingleLevels | Agda.TypeChecking.Level |
| unSizeExpr | Agda.TypeChecking.SizedTypes.Solve |
| unSizeView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| UnsolvedConstraint | Agda.Interaction.Highlighting.Precise |
| UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnsolvedConstraints_ | Agda.Interaction.Options.Warnings |
| UnsolvedInteractionMetas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnsolvedInteractionMetas_ | Agda.Interaction.Options.Warnings |
| UnsolvedMeta | Agda.Interaction.Highlighting.Precise |
| UnsolvedMetaVariables | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UnsolvedMetaVariables_ | Agda.Interaction.Options.Warnings |
| unsolvedWarnings | Agda.Interaction.Options.Warnings |
| unSpine | Agda.Syntax.Internal |
| unSpine' | Agda.Syntax.Internal |
| UnsupportedAttribute | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| UnsupportedAttribute_ | Agda.Interaction.Options.Warnings |
| UntaggedValue | Agda.Interaction.JSON |
| unTCM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Unused | Agda.TypeChecking.Positivity.Occurrence |
| unusedVar | Agda.Termination.Monad |
| UnusedVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| unVersionView | Agda.Interaction.Library |
| unviewProjectedVar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| unwrapUnaryRecords | Agda.Interaction.JSON |
| unzip | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| unzipMaybe | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| unzipWith | Agda.Utils.List |
| update | |
| 1 (Function) | Agda.Utils.BiMap |
| 2 (Function) | Agda.Utils.AssocList |
| update1 | Agda.Utils.Update |
| update2 | Agda.Utils.Update |
| updateAllowedReductions | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| updateAt | |
| 1 (Function) | Agda.Utils.List |
| 2 (Function) | Agda.Utils.AssocList |
| updateBenchmark | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateBenchmarkingStatus | Agda.TypeChecking.Monad.Benchmark |
| updateCompiledClauses | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| updateCovering | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateDefArgOccurrences | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateDefBlocked | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateDefCompiledRep | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateDefCopatternLHS | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateDefinition | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateDefinitions | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateDefPolarity | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateDefType | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateFunClauses | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateHead | Agda.Utils.List |
| updateHeads | Agda.TypeChecking.Injectivity |
| updateInstanceDefs | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updateInteractionPointsAfter | Agda.Interaction.InteractionTop |
| updateLast | Agda.Utils.List |
| updateMetaVar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| updateMetaVarRange | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| updateMetaVarTCM | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| updateNamedArg | Agda.Syntax.Common |
| updateNamedArgA | Agda.Syntax.Common |
| updatePersistentState | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| updatePrecondition | Agda.Utils.BiMap |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| updateVarsToBind | Agda.Syntax.Scope.Base |
| upperBounds | Agda.TypeChecking.SizedTypes.WarshallSolver |
| ureadIORef | Agda.Auto.NarrowingSearch |
| ureadmodifyIORef | Agda.Auto.NarrowingSearch |
| UsableAtMod | Agda.Interaction.Base |
| UsableAtModality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| usableAtModality | Agda.TypeChecking.Irrelevance |
| usableCohesion | Agda.Syntax.Common |
| usableMod | Agda.TypeChecking.Irrelevance |
| usableModAbs | 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Errors, Agda.Syntax.Concrete.Definitions |
| UselessAbstract_ | Agda.Interaction.Options.Warnings |
| UselessHiding | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UselessHiding_ | Agda.Interaction.Options.Warnings |
| UselessInline | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UselessInline_ | Agda.Interaction.Options.Warnings |
| UselessInstance | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| UselessInstance_ | Agda.Interaction.Options.Warnings |
| UselessPatternDeclarationForRecord | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UselessPatternDeclarationForRecord_ | Agda.Interaction.Options.Warnings |
| UselessPrivate | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| UselessPrivate_ | Agda.Interaction.Options.Warnings |
| UselessPublic | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| userNamed | Agda.Syntax.Common |
| UserWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UserWarning_ | Agda.Interaction.Options.Warnings |
| UserWritten | Agda.Syntax.Common |
| Uses | Agda.Compiler.JS.Syntax |
| uses | Agda.Compiler.JS.Syntax |
| usesCopatterns | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| useScope | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| UsesFloat | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler |
| UseShowInstance | Agda.Interaction.Base |
| useTC | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |