Agda-2.6.2.2.20221106: A dependently typed functional programming language and proof assistant

Index - U

U 
1 (Type/Class)Agda.TypeChecking.Serialise.Base
2 (Data Constructor)Agda.TypeChecking.Serialise.Base
UEAgda.TypeChecking.Coverage.SplitClause
uglyShowNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
UIdAgda.Auto.Syntax
umodifyIORefAgda.Auto.NarrowingSearch
unAbsAgda.Syntax.Internal
unAbsNAgda.TypeChecking.Names
unambiguousAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
unAmbQAgda.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
unArgAgda.Syntax.Common
unBindAgda.Syntax.Abstract
unbindVariableAgda.Syntax.Scope.Monad
UnBlockAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unblockDefAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockedTesterAgda.TypeChecking.MetaVars
unblockMetaAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnAllAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAllAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAllMetasAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAllMetasInAgda.Syntax.Internal.MetaVars
UnblockOnAnyAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAnyAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAnyMetaAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAnyMetaInAgda.Syntax.Internal.MetaVars
unblockOnBothAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnDefAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnDefAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnEitherAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnMetaAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnMetaAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnProblemAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnProblemAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockProblemAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unBlockTAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unBraveAgda.Syntax.Internal
unBruijnAgda.TypeChecking.CompiledClause.Compile
UnconfirmedReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
uncons 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List
unConstVAgda.TypeChecking.Level
uncurry3Agda.Utils.Tuple
uncurry4Agda.Utils.Tuple
uncurrysAgda.Utils.TypeLevel
unDeepSizeViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
UndefinedAgda.Compiler.JS.Syntax
underAbsAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
underAbstractionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
underAbstraction'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
underAbstractionAbsAgda.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
UnderappliedAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
underBinderAgda.TypeChecking.Free.Lazy
underBinder'Agda.TypeChecking.Free.Lazy
UnderComposition 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
underConstructorAgda.TypeChecking.Free.Lazy
underFlexRigAgda.TypeChecking.Free.Lazy
UnderInfAgda.TypeChecking.Positivity.Occurrence
UnderLambda 
1 (Type/Class)Agda.Compiler.Treeless.Subst
2 (Data Constructor)Agda.Compiler.Treeless.Subst
underLambdaAgda.Compiler.Treeless.Subst
underLambdasAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
underlyingRangeAgda.TypeChecking.Serialise.Instances.Common
underModalityAgda.TypeChecking.Free.Lazy
underRelevanceAgda.TypeChecking.Free.Lazy
Underscore 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
underscoreAgda.Syntax.Common
UndoAgda.Auto.NarrowingSearch
unDomAgda.Syntax.Internal
unDropAgda.Utils.Permutation
unElAgda.Syntax.Internal
unequalAgda.Auto.Typecheck
UnequalBecauseOfUniverseConflictAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnequalCohesionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnequalFinitenessAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnequalHidingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnequalLevelAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnequalQuantityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnequalRelevanceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unequalsAgda.Auto.Typecheck
UnequalSortsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnequalTermsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnequalTypesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unescapeAgda.Compiler.JS.Pretty
unescapesAgda.Compiler.JS.Pretty
UnexpectedWithPatternsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unExprViewAgda.Syntax.Concrete.Operators.Parser
unflattenTelAgda.TypeChecking.Telescope
unflattenTel'Agda.TypeChecking.Telescope
unfold 
1 (Function)Agda.Utils.List1
2 (Function)Agda.TypeChecking.MetaVars.Occurs
unfoldBAgda.TypeChecking.MetaVars.Occurs
unfoldCorecursionAgda.TypeChecking.Reduce
unfoldCorecursionEAgda.TypeChecking.Reduce
unfoldDefinitionEAgda.TypeChecking.Reduce
unfoldDefinitionStepAgda.TypeChecking.Reduce
unfoldInlinedAgda.TypeChecking.Reduce
unfoldrAgda.Utils.List1
UnfoldStrategyAgda.TypeChecking.MetaVars.Occurs
UnFreezeMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
unfreezeMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
unfreezeMetasAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
UnguardedAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
unguardedRecordAgda.TypeChecking.Records
UnGuardedRhsAgda.Utils.Haskell.Syntax
unguardedVarsAgda.TypeChecking.Free
UnicodeOkAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options
UnicodeOrAsciiAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options
UnicodeSubscriptAgda.Syntax.Concrete, Agda.Syntax.Abstract.Name, Agda.Syntax.Concrete.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
UnificationFailureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnificationResultAgda.TypeChecking.Rules.LHS.Unify
UnificationResult'Agda.TypeChecking.Rules.LHS.Unify
UnificationStepAgda.TypeChecking.Rules.LHS.Unify.Types
UnificationStuckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnifiesAgda.TypeChecking.Rules.LHS.Unify
UnifiesToAgda.Auto.CaseSplit
UnifyAgda.Auto.CaseSplit
unifyAgda.Auto.CaseSplit
unify'Agda.Auto.CaseSplit
UnifyBlockedAgda.TypeChecking.Rules.LHS.Unify
UnifyConflictAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnifyCycleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unifyElimsAgda.TypeChecking.IApplyConfluence
unifyElimsMetaAgda.TypeChecking.IApplyConfluence
UnifyEquivAgda.TypeChecking.Coverage.SplitClause
unifyexpAgda.Auto.CaseSplit
UnifyIndicesAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
unifyIndicesAgda.TypeChecking.Rules.LHS.Unify
unifyIndices'Agda.TypeChecking.Rules.LHS.Unify
UnifyIndicesNotVarsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnifyLogAgda.TypeChecking.Rules.LHS.Unify.Types
UnifyLog'Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyLogEntryAgda.TypeChecking.Rules.LHS.Unify.Types
UnifyLogTAgda.TypeChecking.Rules.LHS.Unify.Types
UnifyOutput 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Unify.Types
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Unify.Types
unifyProofAgda.TypeChecking.Rules.LHS.Unify.Types
UnifyRecursiveEqAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnifyReflexiveEqAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnifyStateAgda.TypeChecking.Rules.LHS.Unify.Types
UnifyStepAgda.TypeChecking.Rules.LHS.Unify.Types
UnifyStepTAgda.TypeChecking.Rules.LHS.Unify.Types
UnifyStuckAgda.TypeChecking.Rules.LHS.Unify
unifySubstAgda.TypeChecking.Rules.LHS.Unify.Types
UnifyUnusableModalityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unifyVarAgda.Auto.CaseSplit
UninstantiatedDotPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.JS.Substitution
9 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
10 (Function)Agda.Utils.Favorites
11 (Function)Agda.Termination.CallMatrix
12 (Function)Agda.Termination.CallGraph
unionBuiltinAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unionComparedAgda.Utils.Favorites
unionMaybeWith 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
unionPreconditionAgda.Utils.BiMap
unions 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionSignaturesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
unionsMaybeWithAgda.Utils.Maybe
unionsWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
unionWith 
1 (Function)Agda.Utils.Trie
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
uniqOnAgda.Utils.List
uniqueIntAgda.Utils.Graph.AdjacencyMap.Unidirectional
unitCohesionAgda.Syntax.Common
unitComposeAgda.TypeChecking.SizedTypes.Utils
unitModalityAgda.Syntax.Common
unitQuantityAgda.Syntax.Common
unitRelevanceAgda.Syntax.Common
unit_conAgda.Utils.Haskell.Syntax
univarAgda.Auto.SearchControl
UniverseCheckAgda.Syntax.Common
universeCheckAgda.Syntax.Concrete.Definitions.Types
universeCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
UnivSortAgda.Syntax.Internal
univSortAgda.TypeChecking.Substitute
univSort'Agda.TypeChecking.Substitute
UnkindedVarAgda.Utils.Haskell.Syntax
Unknown 
1 (Data Constructor)Agda.Interaction.Options.Warnings
2 (Data Constructor)Agda.Termination.Order
3 (Data Constructor)Agda.Syntax.Reflected
unknownAgda.Termination.Order
UnknownErrorAgda.Interaction.ExitCode
UnknownFieldAgda.Interaction.Library.Base
UnknownFixityInMixfixDeclAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UnknownFixityInMixfixDecl_Agda.Interaction.Options.Warnings
unknownFreeVariablesAgda.Syntax.Common
UnknownFVsAgda.Syntax.Common
UnknownHeadAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnknownNameAgda.Syntax.Scope.Base
UnknownNamesInFixityDeclAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UnknownNamesInFixityDecl_Agda.Interaction.Options.Warnings
UnknownNamesInPolarityPragmasAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UnknownNamesInPolarityPragmas_Agda.Interaction.Options.Warnings
UnknownSAgda.Syntax.Reflected
UnknownSortAgda.Auto.Syntax
unlabelPatVarsAgda.Syntax.Internal.Pattern
unlamViewAgda.TypeChecking.Substitute
unlessAgda.Utils.Monad
unlessDebugPrintingAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unlessMAgda.Utils.Monad
unlessNull 
1 (Function)Agda.Utils.Null
2 (Function)Agda.Utils.List1
unlessNullMAgda.Utils.Null
unLevelAgda.TypeChecking.Level
unlevelWithKitAgda.TypeChecking.Level
unlistenToMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
unLvlAgda.TypeChecking.Primitive
unMAgda.Termination.SparseMatrix
unmapListTAgda.Utils.ListT
unMaxViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
unNameAgda.TypeChecking.Names
unnamedAgda.Syntax.Common
unnamedArgAgda.Syntax.Common
unNatAgda.TypeChecking.Primitive
unNiceAgda.Syntax.Concrete.Definitions.Monad
unNLMAgda.TypeChecking.Rewriting.NonLinMatch
unnumberPatVarsAgda.Syntax.Internal.Pattern
unpackUnquoteMAgda.TypeChecking.Unquote
unPiViewAgda.Syntax.Abstract.Views
unPlusVAgda.TypeChecking.Level
unPMAgda.Syntax.Parser
unProjViewAgda.TypeChecking.ProjectionLike
unPureConversionTAgda.TypeChecking.Conversion.Pure
unqhnameAgda.Compiler.MAlonzo.Misc
UnQualAgda.Utils.Haskell.Syntax
unqualifyAgda.Syntax.Concrete, Agda.Syntax.Concrete.Name
Unquote 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Type/Class)Agda.TypeChecking.Unquote
unquoteAgda.TypeChecking.Unquote
UnquoteData 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
UnquoteDataSAgda.Syntax.Abstract
UnquoteDecl 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
UnquoteDeclSAgda.Syntax.Abstract
UnquoteDef 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
UnquoteDefRequiresSignatureAgda.Syntax.Concrete.Definitions.Errors
UnquoteDefSAgda.Syntax.Abstract
UnquoteErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnquoteFailedAgda.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
UnquoteMAgda.TypeChecking.Unquote
unquoteMAgda.TypeChecking.Rules.Term
unquoteNAgda.TypeChecking.Unquote
unquoteNormaliseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unquoteNStringAgda.TypeChecking.Unquote
UnquotePanicAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnquoteResAgda.TypeChecking.Unquote
UnquoteStateAgda.TypeChecking.Unquote
unquoteStringAgda.TypeChecking.Unquote
UnquoteTacticAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unquoteTacticAgda.TypeChecking.Rules.Term
unquoteTCMAgda.TypeChecking.Unquote
unquoteTopAgda.TypeChecking.Rules.Decl
unrangedAgda.Syntax.Common
Unreachable 
1 (Data Constructor)Agda.Utils.Impossible
2 (Type/Class)Agda.Syntax.Treeless, Agda.Compiler.Backend
UnreachableClausesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnreachableClauses_Agda.Interaction.Options.Warnings
unReduceMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnrelatedAgda.Syntax.Common
unsafeCoerceModAgda.Compiler.MAlonzo.Misc
unsafeDeclarationWarningAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
unsafeDeclarationWarning'Agda.Syntax.Concrete.Definitions.Errors
unsafeEscapeContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
unsafeInTopContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
unsafeModifyContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
unsafePragmaOptionsAgda.Interaction.Options
unsafeSetUnicodeOrAsciiAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
unsafeTopLevelModuleNameAgda.Syntax.TopLevelModuleName
unScopeAgda.Syntax.Abstract.Views
unSingleLevelAgda.TypeChecking.Level
unSingleLevelsAgda.TypeChecking.Level
unSizeExprAgda.TypeChecking.SizedTypes.Solve
unSizeViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
UnsolvedConstraintAgda.Interaction.Highlighting.Precise
UnsolvedConstraintsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnsolvedConstraints_Agda.Interaction.Options.Warnings
UnsolvedInteractionMetasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnsolvedInteractionMetas_Agda.Interaction.Options.Warnings
UnsolvedMetaAgda.Interaction.Highlighting.Precise
UnsolvedMetaVariablesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnsolvedMetaVariables_Agda.Interaction.Options.Warnings
unsolvedWarningsAgda.Interaction.Options.Warnings
unSpineAgda.Syntax.Internal
unSpine'Agda.Syntax.Internal
UnsupportedAttributeAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
UnsupportedAttribute_Agda.Interaction.Options.Warnings
UnsupportedCxtAgda.TypeChecking.Rules.LHS.Unify, Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
UnsupportedIndexedMatchAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnsupportedIndexedMatch_Agda.Interaction.Options.Warnings
UnsupportedYetAgda.TypeChecking.Rules.LHS.Unify, Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
UntaggedValueAgda.Interaction.JSON
unTCMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UnusedAgda.TypeChecking.Positivity.Occurrence
unusedVarAgda.Termination.Monad
UnusedVariableInPatternSynonymAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
unVersionViewAgda.Interaction.Library
unviewProjectedVarAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
unwrapUnaryRecordsAgda.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
unzipWithAgda.Utils.List
update 
1 (Function)Agda.Utils.BiMap
2 (Function)Agda.Utils.AssocList
update1Agda.Utils.Update
update2Agda.Utils.Update
updateAllowedReductionsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
updateAt 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.AssocList
updateBenchmarkAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateBenchmarkingStatusAgda.TypeChecking.Monad.Benchmark
updateCompiledClausesAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
updateCoveringAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateDefArgOccurrencesAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateDefBlockedAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateDefCompiledRepAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateDefCopatternLHSAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateDefinitionAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateDefinitionsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateDefPolarityAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateDefTypeAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateEtaForRecordAgda.TypeChecking.Records
updateFunClausesAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateHeadAgda.Utils.List
updateHeadsAgda.TypeChecking.Injectivity
updateInstanceDefsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateInteractionPointsAfterAgda.Interaction.InteractionTop
updateLastAgda.Utils.List
updateMetaVarAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
updateMetaVarRangeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
updateMetaVarTCMAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
updateNamedArgAgda.Syntax.Common
updateNamedArgAAgda.Syntax.Common
updatePersistentStateAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updatePreconditionAgda.Utils.BiMap
updateProblemRestAgda.TypeChecking.Rules.LHS.ProblemRest
updatePtrAgda.Utils.Pointer
updatePtrMAgda.Utils.Pointer
UpdaterAgda.Utils.Update
Updater1Agda.Utils.Update
updater1Agda.Utils.Update
Updater2Agda.Utils.Update
updater2Agda.Utils.Update
UpdaterTAgda.Utils.Update
updates1Agda.Utils.Update
updates2Agda.Utils.Update
updateScopeLocalsAgda.Syntax.Scope.Base
updateScopeNameSpacesAgda.Syntax.Scope.Base
updateScopeNameSpacesMAgda.Syntax.Scope.Base
updateTheDefAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
updateVarsToBindAgda.Syntax.Scope.Base
upperBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
ureadIORefAgda.Auto.NarrowingSearch
ureadmodifyIORefAgda.Auto.NarrowingSearch
UsableAtModAgda.Interaction.Base
UsableAtModalityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
usableAtModalityAgda.TypeChecking.Irrelevance
usableAtModality'Agda.TypeChecking.Irrelevance
usableCohesionAgda.Syntax.Common
usableModAgda.TypeChecking.Irrelevance
usableModAbsAgda.TypeChecking.Irrelevance
UsableModalityAgda.TypeChecking.Irrelevance
usableModalityAgda.Syntax.Common
usableQuantityAgda.Syntax.Common
usableRelAgda.TypeChecking.Irrelevance
UsableRelevanceAgda.TypeChecking.Irrelevance
usableRelevanceAgda.Syntax.Common
UsableSizeVarsAgda.Termination.Monad
usableSizeVarsAgda.Termination.Monad
usageAgda.Interaction.Options
usageWarningAgda.Interaction.Options.Warnings
useAgda.Utils.Lens
useConcreteNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
usedArgumentsAgda.Compiler.Treeless.Unused
useDefaultFixityAgda.Syntax.Notation
UseEverythingAgda.Syntax.Common
UseForceAgda.Interaction.Base
useInjectivityAgda.TypeChecking.Injectivity
UselessAbstractAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessAbstract_Agda.Interaction.Options.Warnings
UselessHidingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UselessHiding_Agda.Interaction.Options.Warnings
UselessInlineAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UselessInline_Agda.Interaction.Options.Warnings
UselessInstanceAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessInstance_Agda.Interaction.Options.Warnings
UselessPatternDeclarationForRecordAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UselessPatternDeclarationForRecord_Agda.Interaction.Options.Warnings
UselessPrivateAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessPrivate_Agda.Interaction.Options.Warnings
UselessPublicAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UselessPublic_Agda.Interaction.Options.Warnings
useNamesFromPatternAgda.TypeChecking.Rules.LHS.ProblemRest
useNamesFromProblemEqsAgda.TypeChecking.Rules.LHS.ProblemRest
useOriginFromAgda.TypeChecking.Rules.LHS.ProblemRest
usePatOriginAgda.TypeChecking.Substitute
usePatternInfoAgda.TypeChecking.Substitute
useRAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
userNamedAgda.Syntax.Common
UserWarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UserWarning_Agda.Interaction.Options.Warnings
UserWrittenAgda.Syntax.Common
UsesAgda.Compiler.JS.Syntax
usesAgda.Compiler.JS.Syntax
usesCopatternsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
useScopeAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
UsesFloat 
1 (Type/Class)Agda.Compiler.MAlonzo.Compiler
2 (Data Constructor)Agda.Compiler.MAlonzo.Compiler
UseShowInstanceAgda.Interaction.Base
useTCAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
useTerPragmaAgda.TypeChecking.Rules.Def
Using 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Syntax.Concrete
usingAgda.Syntax.Common
Using'Agda.Syntax.Common
UsingOnlyAgda.Syntax.Scope.Base
UsingOrHidingAgda.Syntax.Scope.Base
usingOrHidingAgda.Syntax.Scope.Base
UStateAgda.TypeChecking.Rules.LHS.Unify.Types
usualWarningsAgda.Interaction.Options.Warnings
uwriteIORefAgda.Auto.NarrowingSearch