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

U
1 (Type/Class)	Agda.TypeChecking.Serialise.Base
2 (Data Constructor)	Agda.TypeChecking.Serialise.Base
uhcBackendEnabled	Agda.Compiler.UHC.Bridge
UId	Agda.Auto.Syntax
umodifyIORef	Agda.Auto.NarrowingSearch
unAbs	Agda.Syntax.Internal
unAmbQ	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract
unAppView	Agda.Syntax.Abstract.Views
unArg	Agda.Syntax.Common
UnBlock	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unblockedTester	Agda.TypeChecking.MetaVars
uncons	Agda.Utils.List
uncurry3	Agda.Utils.Tuple
uncurry4	Agda.Utils.Tuple
unDeepSizeView	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
Undefined	Agda.Compiler.JS.Syntax
underAbs	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
underAbstraction	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
underAbstraction_
1 (Function)	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
2 (Function)	Agda.TypeChecking.Reduce.Monad
Underapplied	Agda.Syntax.Internal
underConstructor	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
1 (Function)	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
2 (Function)	Agda.Compiler.Treeless.DelayCoinduction
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.Common
unDrop	Agda.Utils.Permutation
unEl	Agda.Syntax.Internal
unequal	Agda.Auto.Typecheck
UnequalBecauseOfUniverseConflict	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalHiding	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
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.Reduce
unfoldCorecursionE	Agda.TypeChecking.Reduce
unfoldDefinition	Agda.TypeChecking.Reduce
unfoldDefinition'	Agda.TypeChecking.Reduce
unfoldDefinitionE	Agda.TypeChecking.Reduce
unfoldDefinitionStep	Agda.TypeChecking.Reduce
UnfoldStrategy	Agda.TypeChecking.MetaVars.Occurs
UnFreezeMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unfreezeMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unfreezeMetas	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unfreezeMetas'	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
Unguarded
1 (Data Constructor)	Agda.TypeChecking.Free.Lazy
2 (Data Constructor)	Agda.TypeChecking.Free.Old
3 (Data Constructor)	Agda.TypeChecking.Free
unguardedRecord	Agda.TypeChecking.Records
UnGuardedRhs	Agda.Utils.Haskell.Syntax
unguardedVars
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
UnicodeTest	Agda.Utils.Char
unicodeTests	Agda.Utils.Char
unifiable	Agda.Compiler.Epic.Injection
UnificationRecursiveEq	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnificationResult	Agda.TypeChecking.Rules.LHS.Unify
UnificationResult'	Agda.TypeChecking.Rules.LHS.Unify
UnificationStuck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Unifies	Agda.TypeChecking.Rules.LHS.Unify
unify	Agda.Compiler.Epic.Injection
UnifyConflict	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnifyCycle	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unifyexp	Agda.Auto.CaseSplit
unifyI	Agda.Compiler.Epic.Forcing
UnifyIndices	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
unifyIndices	Agda.TypeChecking.Rules.LHS.Unify
UnifyIndicesNotVars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unifyIndices_	Agda.TypeChecking.Rules.LHS.Unify
unifyPointers	Agda.TypeChecking.Conversion
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.HashMap
3 (Function)	Agda.Utils.BiMap
4 (Function)	Agda.Utils.Bag
5 (Function)	Agda.Utils.Favorites
6 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
7 (Function)	Agda.Utils.Trie
8 (Function)	Agda.Termination.CallMatrix
9 (Function)	Agda.Termination.CallGraph
10 (Function)	Agda.Compiler.JS.Substitution
unionCompared	Agda.Utils.Favorites
unionConstraints	Agda.Compiler.Epic.Injection
unionMaybeWith
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
unions
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.Bag
4 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionSignatures	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
unionsWith	Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionWith
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Function)	Agda.Utils.Trie
unionWithKey	Agda.Utils.HashMap
unionWithM	Agda.Utils.Map
uniqOn	Agda.Utils.List
UNIT	Agda.Compiler.Epic.AuxAST
unitCompose	Agda.TypeChecking.SizedTypes.Utils
unit_con	Agda.Utils.Haskell.Syntax
univar	Agda.Auto.SearchControl
UnkindedVar	Agda.Utils.Haskell.Syntax
Unknown
1 (Data Constructor)	Agda.Termination.Order
2 (Data Constructor)	Agda.Syntax.Reflected
3 (Data Constructor)	Agda.TypeChecking.Positivity.Occurrence
unknown	Agda.Termination.Order
UnknownName	Agda.Syntax.Scope.Monad
UnknownNamesInFixityDecl	Agda.Syntax.Concrete.Definitions
UnknownNamesInPolarityPragmas	Agda.Syntax.Concrete.Definitions
UnknownS	Agda.Syntax.Reflected
UnknownSort	Agda.Auto.Syntax
unlabelPatVars	Agda.Syntax.Internal.Pattern
unless	Agda.Utils.Monad
unlessM	Agda.Utils.Monad
unlessNull	Agda.Utils.Null
unlessNullM	Agda.Utils.Null
unless_	Agda.Utils.Monad
unLevel	Agda.TypeChecking.Level
unLevelAtom	Agda.TypeChecking.Substitute
unlevelWithKit	Agda.TypeChecking.Level
unlistenToMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unLvl	Agda.TypeChecking.Primitive
unM	Agda.Termination.SparseMatrix
unMaxView	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
unnamed	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
unqhname	Agda.Compiler.MAlonzo.Misc
unqname	Agda.Compiler.Epic.CompileState
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
UnquoteFailed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnquoteFlags
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnquoteM	Agda.TypeChecking.Unquote
unquoteM	Agda.TypeChecking.Rules.Term
unquoteN	Agda.TypeChecking.Unquote
unquoteNormalise	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unquoteNString	Agda.TypeChecking.Unquote
UnquotePanic	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnquoteRes	Agda.TypeChecking.Unquote
UnquoteState	Agda.TypeChecking.Unquote
unquoteString	Agda.TypeChecking.Unquote
UnquoteTactic	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unquoteTactic	Agda.TypeChecking.Rules.Term
unquoteTCM	Agda.TypeChecking.Unquote
unquoteTop	Agda.TypeChecking.Rules.Decl
unranged	Agda.Syntax.Common
Unreachable	Agda.Syntax.Treeless
UnreachableClauses	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnreducedLevel	Agda.Syntax.Internal
unReduceM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Unrelated	Agda.Syntax.Fixity
unsafeCoerceMod	Agda.Compiler.MAlonzo.Misc
unsafePragmaOptions	Agda.Interaction.Options
unScope	Agda.Syntax.Abstract.Views
unserialize	Agda.Compiler.UHC.Bridge
unshadowName	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
unSizeExpr	Agda.TypeChecking.SizedTypes.Solve
unSizeView	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
UnsolvedConstraint	Agda.Interaction.Highlighting.Precise
UnsolvedConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnsolvedInteractionMetas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnsolvedMeta	Agda.Interaction.Highlighting.Precise
UnsolvedMetaVariables	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unSpine	Agda.Syntax.Internal
unSpine'	Agda.Syntax.Internal
unStr	Agda.Utils.String
unTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unusableRelevance	Agda.Syntax.Common
Unused
1 (Data Constructor)	Agda.TypeChecking.Positivity.Occurrence
2 (Data Constructor)	Agda.TypeChecking.Free.Old
3 (Data Constructor)	Agda.TypeChecking.Free
UnusedArg	Agda.Syntax.Common
unusedVar	Agda.Termination.Monad
UnusedVariableInPatternSynonym	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unusedVars
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
unzip
1 (Function)	Agda.Utils.Map
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
unzip3	Agda.Utils.Map
unzipMaybe
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
update
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.AssocList
update1	Agda.Utils.Update
update2	Agda.Utils.Update
updateAllowedReductions	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
updateAt
1 (Function)	Agda.Utils.List
2 (Function)	Agda.Utils.AssocList
updateBenchmark	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateBenchmarkingStatus	Agda.TypeChecking.Monad.Benchmark
updateCompiledClauses	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefArgOccurrences	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefCompiledRep	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefinition	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefinitions	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefPolarity	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefType	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateFunClauses	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateHead	Agda.Utils.List
updateInPatterns	Agda.TypeChecking.Rules.LHS
updateInstanceDefs	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateLast	Agda.Utils.List
updateMetaVar	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateMetaVarRange	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateModuleParameters	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
updateNamedArg	Agda.Syntax.Common
updatePersistentState	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateProblemRest	Agda.TypeChecking.Rules.LHS.ProblemRest
updateProblemRest_	Agda.TypeChecking.Rules.LHS.ProblemRest
updatePtr	Agda.Utils.Pointer, Agda.Syntax.Internal
updatePtrM	Agda.Utils.Pointer, Agda.Syntax.Internal
Updater	Agda.Utils.Update
Updater1	Agda.Utils.Update
updater1	Agda.Utils.Update
Updater2	Agda.Utils.Update
updater2	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
updateShared	Agda.Syntax.Internal
updateSharedFM	Agda.Syntax.Internal
updateSharedM	Agda.Syntax.Internal
updateSharedTerm	Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateSharedTermF	Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateSharedTermT	Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateTheDef	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
upperBounds	Agda.TypeChecking.SizedTypes.WarshallSolver
ureadIORef	Agda.Auto.NarrowingSearch
ureadmodifyIORef	Agda.Auto.NarrowingSearch
UsableSizeVars	Agda.Termination.Monad
usableSizeVars	Agda.Termination.Monad
usage	Agda.Interaction.Options
use	Agda.Utils.Lens
usedArguments	Agda.Compiler.Treeless.Unused
useDefaultFixity	Agda.Syntax.Fixity
UseEverything	Agda.Syntax.Common
useInjectivity	Agda.TypeChecking.Injectivity
UselessAbstract	Agda.Syntax.Concrete.Definitions
UselessInstance	Agda.Syntax.Concrete.Definitions
UselessPrivate	Agda.Syntax.Concrete.Definitions
useNamesFromPattern	Agda.TypeChecking.Rules.LHS.ProblemRest
useOriginFrom	Agda.TypeChecking.Rules.LHS.ProblemRest
UserWritten	Agda.Syntax.Common
Uses	Agda.Compiler.JS.Syntax
uses	Agda.Compiler.JS.Syntax
usesCopatterns	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
UseShowInstance	Agda.Interaction.BasicOps
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
UsingOrHiding	Agda.Syntax.Scope.Base
usingOrHiding	Agda.Syntax.Scope.Base
uwriteIORef	Agda.Auto.NarrowingSearch