A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
#
$
%
&
+
.
/
<
=
>
?
@
\
^
|
-
_
All

Index - U

UE	Agda.TypeChecking.Coverage.SplitClause
uglyShowName	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
UId	Agda.Auto.Syntax
ULarge	Agda.Syntax.Internal
umodifyIORef	Agda.Auto.NarrowingSearch
unAbs	Agda.Syntax.Internal
unAbsN	Agda.TypeChecking.Names
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.TypeChecking.Monad, Agda.Compiler.Backend
unblockDef	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
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
unblockOnBoth	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnDef	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnDef	Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
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.TypeChecking.Monad, Agda.Compiler.Backend
UnboundVariablesInPatternSynonym	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unBrave	Agda.Syntax.Internal
unBruijn	Agda.TypeChecking.CompiledClause.Compile
unBuiltinAccess	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnconfirmedReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.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
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
underOpaqueId	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
UnequalFiniteness	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
UnexpectedModalityAnnotationInParameter	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedParameter	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedTypeSignatureForParameter	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedWithPatterns	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unExprView	Agda.Syntax.Concrete.Operators.Parser
unflattenTel	Agda.TypeChecking.Telescope
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
unfoldDefinitionE	Agda.TypeChecking.Reduce
unfoldDefinitionStep	Agda.TypeChecking.Reduce
Unfolding	Agda.Syntax.Concrete
UnfoldingDecl	Agda.Syntax.Abstract
UnfoldingDeclS	Agda.Syntax.Abstract
UnfoldingOutsideOpaque	Agda.Syntax.Concrete.Definitions.Errors
unfoldInlined	Agda.TypeChecking.Reduce
unfoldr	Agda.Utils.List1
UnfoldStrategy	Agda.TypeChecking.MetaVars.Occurs
UnfoldTransparentName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnfoldTransparentName_	Agda.Interaction.Options.Warnings
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
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.TypeChecking.Monad, Agda.Compiler.Backend
UnificationResult	Agda.TypeChecking.Rules.LHS.Unify
UnificationResult'	Agda.TypeChecking.Rules.LHS.Unify
UnificationStep	Agda.TypeChecking.Rules.LHS.Unify.Types
UnificationStuck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
UnifyCycle	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unifyElims	Agda.TypeChecking.IApplyConfluence
unifyElimsMeta	Agda.TypeChecking.IApplyConfluence
UnifyEquiv	Agda.TypeChecking.Coverage.SplitClause
unifyexp	Agda.Auto.CaseSplit
UnifyIndices	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
unifyIndices	Agda.TypeChecking.Rules.LHS.Unify
unifyIndices'	Agda.TypeChecking.Rules.LHS.Unify
UnifyIndicesNotVars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyLog	Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyLog'	Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyLogEntry	Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyLogT	Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyOutput
1 (Type/Class)	Agda.TypeChecking.Rules.LHS.Unify.Types
2 (Data Constructor)	Agda.TypeChecking.Rules.LHS.Unify.Types
unifyProof	Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyRecursiveEq	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyReflexiveEq	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyState	Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyStep	Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyStepT	Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyStuck	Agda.TypeChecking.Rules.LHS.Unify
unifySubst	Agda.TypeChecking.Rules.LHS.Unify.Types
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.BoolSet
3 (Function)	Agda.Utils.Bag
4 (Function)	Agda.Utils.SmallSet
5 (Function)	Agda.Utils.Trie
6 (Function)	Agda.Utils.List1
7 (Function)	Agda.Utils.BiMap
8 (Function)	Agda.Utils.Favorites
9 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
10 (Function)	Agda.Termination.CallMatrix
11 (Function)	Agda.Termination.CallGraph
12 (Function)	Agda.Compiler.JS.Substitution
unionBuiltin	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.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
uniqueInt	Agda.Utils.Graph.AdjacencyMap.Unidirectional
UniqueOpaque	Agda.Syntax.Common
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
Univ
1 (Type/Class)	Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Internal
univar	Agda.Auto.SearchControl
univChecks	Agda.TypeChecking.Rules.Application
UniverseCheck	Agda.Syntax.Common
universeCheck	Agda.Syntax.Concrete.Definitions.Types
universeCheckPragma	Agda.Syntax.Concrete.Definitions.Monad
univFibrancy	Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
UnivSize	Agda.Syntax.Internal
UnivSort	Agda.Syntax.Internal
univSort	Agda.TypeChecking.Substitute
univSort'	Agda.TypeChecking.Substitute
univUniv	Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unLvl	Agda.TypeChecking.Primitive
unM	Agda.Termination.SparseMatrix
unmapListT	Agda.Utils.ListT
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
unNice	Agda.Syntax.Concrete.Definitions.Monad
unNLM	Agda.TypeChecking.Rewriting.NonLinMatch
unnumberPatVars	Agda.Syntax.Internal.Pattern
unpackUnquoteM	Agda.TypeChecking.Unquote
unPiView	Agda.Syntax.Abstract.Views
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
UnquoteData
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
UnquoteDataS	Agda.Syntax.Abstract
UnquoteDecl
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
UnquoteDeclS	Agda.Syntax.Abstract
UnquoteDef
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
UnquoteDefRequiresSignature	Agda.Syntax.Concrete.Definitions.Errors
UnquoteDefS	Agda.Syntax.Abstract
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
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.Errors, Agda.Syntax.Concrete.Definitions
unsafeDeclarationWarning'	Agda.Syntax.Concrete.Definitions.Errors
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
unsafePragma	Agda.Syntax.Concrete.Definitions.Errors
unsafePragmaOptions	Agda.Interaction.Options
unsafeSetUnicodeOrAscii	Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
unsafeTopLevelModuleName	Agda.Syntax.TopLevelModuleName
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.Syntax.Common.Aspect, 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.Syntax.Common.Aspect, 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
UnsupportedAttribute	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
UnsupportedAttribute_	Agda.Interaction.Options.Warnings
UnsupportedCxt	Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
UnsupportedIndexedMatch	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsupportedIndexedMatch_	Agda.Interaction.Options.Warnings
UnsupportedYet	Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
UntaggedValue	Agda.Interaction.JSON
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
unviewProjectedVar	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unwords	Agda.Utils.List1
unwords1	Agda.Utils.String
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.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
updateBlocker	Agda.TypeChecking.Constraints
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
updateEtaForRecord	Agda.TypeChecking.Records
updateFunClauses	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateHead
1 (Function)	Agda.Utils.List
2 (Function)	Agda.Utils.List1
updateHeads	Agda.TypeChecking.Injectivity
updateInstanceDefs	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateInteractionPointsAfter	Agda.Interaction.InteractionTop
updateLast
1 (Function)	Agda.Utils.List
2 (Function)	Agda.Utils.List1
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
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.TypeChecking.Monad, Agda.Compiler.Backend
updateVarsToBind	Agda.Syntax.Scope.Base
upperBounds	Agda.TypeChecking.SizedTypes.WarshallSolver
UProp	Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
ureadIORef	Agda.Auto.NarrowingSearch
ureadmodifyIORef	Agda.Auto.NarrowingSearch
UsableAtMod	Agda.Interaction.Base
UsableAtModality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
usableAtModality	Agda.TypeChecking.Irrelevance
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.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.Errors, Agda.Syntax.Concrete.Definitions
UselessAbstract_	Agda.Interaction.Options.Warnings
UselessHiding	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessHiding_	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.Errors, Agda.Syntax.Concrete.Definitions
UselessInstance_	Agda.Interaction.Options.Warnings
UselessOpaque	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessOpaque_	Agda.Interaction.Options.Warnings
UselessPatternDeclarationForRecord	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPatternDeclarationForRecord_	Agda.Interaction.Options.Warnings
UselessPragma	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPragma_	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.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
USmall	Agda.Syntax.Internal
USSet	Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
UState	Agda.TypeChecking.Rules.LHS.Unify.Types
usualWarnings	Agda.Interaction.Options.Warnings
UType	Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
uwriteIORef	Agda.Auto.NarrowingSearch