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

Index - U

UAgda.Mimer.Options
UEAgda.TypeChecking.Coverage.SplitClause
uglyShowNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
ULargeAgda.Syntax.Internal
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
UnboundVariablesInPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unBraveAgda.Syntax.Internal
unBruijnAgda.TypeChecking.CompiledClause.Compile
unBuiltinAccessAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnconfirmedReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
uncons 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List
unConstVAgda.TypeChecking.Level
uncurry3Agda.Utils.Tuple
uncurry4Agda.Utils.Tuple
uncurrysAgda.Utils.TypeLevel
unDeepSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UndefinedAgda.Compiler.JS.Syntax
underAbstractionAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
underAbstraction'Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
underAbstractionAbsAgda.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
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
underlyingRangeAgda.TypeChecking.Serialise.Instances.Common
underModalityAgda.TypeChecking.Free.Lazy
underOpaqueIdAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
underQuantityAgda.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
unDomAgda.Syntax.Internal
unDropAgda.Utils.Permutation
unElAgda.Syntax.Internal
UnequalBecauseOfUniverseConflictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalCohesionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalFinitenessAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalHidingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalQuantityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalSortsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalTermsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalTypesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unescapeAgda.Compiler.JS.Pretty
unescapesAgda.Compiler.JS.Pretty
UnexpectedModalityAnnotationInParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedTypeSignatureForParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedWithPatternsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
UnfoldingAgda.Syntax.Concrete
UnfoldingDeclAgda.Syntax.Abstract
UnfoldingDeclSAgda.Syntax.Abstract
UnfoldingOutsideOpaqueAgda.Syntax.Concrete.Definitions.Errors
unfoldInlinedAgda.TypeChecking.Reduce
unfoldrAgda.Utils.List1
UnfoldStrategyAgda.TypeChecking.MetaVars.Occurs
UnfoldTransparentNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnfoldTransparentName_Agda.Interaction.Options.Warnings
UnFreezeMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unfreezeMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unfreezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ungatherRecordDirectivesAgda.Syntax.Concrete
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.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
UnificationFailureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnificationMetaAgda.Syntax.Info
UnificationResultAgda.TypeChecking.Rules.LHS.Unify
UnificationResult'Agda.TypeChecking.Rules.LHS.Unify
UnificationStepAgda.TypeChecking.Rules.LHS.Unify.Types
UnificationStuckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifiesAgda.TypeChecking.Rules.LHS.Unify
UnifyBlockedAgda.TypeChecking.Rules.LHS.Unify
UnifyConflictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyCycleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unifyElimsAgda.TypeChecking.IApplyConfluence
unifyElimsMetaAgda.TypeChecking.IApplyConfluence
UnifyEquivAgda.TypeChecking.Coverage.SplitClause
UnifyIndicesAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
unifyIndicesAgda.TypeChecking.Rules.LHS.Unify
unifyIndices'Agda.TypeChecking.Rules.LHS.Unify
UnifyIndicesNotVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
UnifyReflexiveEqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
UninstantiatedDotPatternAgda.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.Favorites
8 (Function)Agda.Utils.BiMap
9 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
10 (Function)Agda.Termination.CallMatrix
11 (Function)Agda.Termination.CallGraph
12 (Function)Agda.Compiler.JS.Substitution
unionBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
UniqueOpaqueAgda.Syntax.Common
unitCohesionAgda.Syntax.Common
unitComposeAgda.TypeChecking.SizedTypes.Utils
unitModalityAgda.Syntax.Common
unitQuantityAgda.Syntax.Common
unitRelevanceAgda.Syntax.Common
unit_conAgda.Utils.Haskell.Syntax
Univ 
1 (Type/Class)Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
univChecksAgda.TypeChecking.Rules.Application
UniverseCheckAgda.Syntax.Common
universeCheckAgda.Syntax.Concrete.Definitions.Types
universeCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
univFibrancyAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
UnivSizeAgda.Syntax.Internal
UnivSortAgda.Syntax.Internal
univSortAgda.TypeChecking.Substitute
univSort'Agda.TypeChecking.Substitute
univUnivAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
UnkindedVarAgda.Utils.Haskell.Syntax
unKleisliAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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
unlabelPatVarsAgda.Syntax.Internal.Pattern
unlamViewAgda.TypeChecking.Substitute
unlessAgda.Utils.Monad
unlessDebugPrintingAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unlessMAgda.Utils.Monad
unlessNull 
1 (Function)Agda.Utils.Null
2 (Function)Agda.Utils.List1
unlessNullMAgda.Utils.Null
unLevelAgda.TypeChecking.Level
unlevelWithKitAgda.TypeChecking.Level
unlistenToMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unLvlAgda.TypeChecking.Primitive
unMAgda.Termination.SparseMatrix
unmapListTAgda.Utils.ListT
unMaxViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unNameAgda.TypeChecking.Names
unnamedAgda.Syntax.Common
unnamedArgAgda.Syntax.Common
unNatAgda.TypeChecking.Primitive
unNiceAgda.Syntax.Concrete.Definitions.Monad
unNLMAgda.TypeChecking.Rewriting.NonLinMatch
unNoSubstAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
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
UnqualifiedAgda.Mimer.Options
unqualifyAgda.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
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.TypeChecking.Monad, Agda.Compiler.Backend
UnquoteFailedAgda.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
UnquoteMAgda.TypeChecking.Unquote
unquoteMAgda.TypeChecking.Rules.Term
unquoteNAgda.TypeChecking.Unquote
unquoteNormaliseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unquoteNStringAgda.TypeChecking.Unquote
UnquotePanicAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnquoteResAgda.TypeChecking.Unquote
UnquoteStateAgda.TypeChecking.Unquote
unquoteStringAgda.TypeChecking.Unquote
UnquoteTacticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
UnreachableClauses_Agda.Interaction.Options.Warnings
unReduceMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnrelatedAgda.Syntax.Common
unsafeCoerceModAgda.Compiler.MAlonzo.Misc
unsafeComparePointersAgda.Utils.Unsafe
unsafeDeclarationWarningAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
unsafeDeclarationWarning'Agda.Syntax.Concrete.Definitions.Errors
unsafeEscapeContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unsafeInTopContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unsafeModifyContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unsafePragmaAgda.Syntax.Concrete.Definitions.Errors
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.Pretty
unSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedConstraintAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
UnsolvedConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedConstraints_Agda.Interaction.Options.Warnings
UnsolvedInteractionMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedInteractionMetas_Agda.Interaction.Options.Warnings
UnsolvedMetaAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
UnsolvedMetaVariablesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
UnsupportedIndexedMatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsupportedIndexedMatch_Agda.Interaction.Options.Warnings
UnsupportedYetAgda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
UntaggedValueAgda.Interaction.JSON
unTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnusableAtModalityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnusedAgda.TypeChecking.Positivity.Occurrence
unusedVarAgda.Termination.Monad
UnusedVariableInPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unVersionViewAgda.Interaction.Library
unviewProjectedVarAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unwordsAgda.Utils.List1
unwords1Agda.Utils.String
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.AssocList
2 (Function)Agda.Utils.BiMap
update1Agda.Utils.Update
update2Agda.Utils.Update
updateAllowedReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateAt 
1 (Function)Agda.Utils.AssocList
2 (Function)Agda.Utils.List
updateBenchmarkAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateBenchmarkingStatusAgda.TypeChecking.Monad.Benchmark
updateBlockerAgda.TypeChecking.Constraints
updateCompiledClausesAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateCoveringAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefArgOccurrencesAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefBlockedAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefCompiledRepAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefCopatternLHSAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefinitionAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefinitionsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefPolarityAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefTypeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateEtaForRecordAgda.TypeChecking.Records
updateFunClausesAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateHead 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
updateHeadsAgda.TypeChecking.Injectivity
updateInstanceDefsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateInteractionPointsAfterAgda.Interaction.InteractionTop
updateLast 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
updateMetaVarAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateMetaVarRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateMetaVarTCMAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateNamedArgAgda.Syntax.Common
updateNamedArgAAgda.Syntax.Common
updatePersistentStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
updateVarsToBindAgda.Syntax.Scope.Base
upperBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
UPropAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
UsableAtModAgda.Interaction.Base
UsableAtModalityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
UselessHiding_Agda.Interaction.Options.Warnings
UselessInlineAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessInline_Agda.Interaction.Options.Warnings
UselessInstanceAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessInstance_Agda.Interaction.Options.Warnings
UselessMacroAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessMacro_Agda.Interaction.Options.Warnings
UselessOpaqueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessOpaque_Agda.Interaction.Options.Warnings
UselessPatternDeclarationForRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPatternDeclarationForRecord_Agda.Interaction.Options.Warnings
UselessPragmaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPragma_Agda.Interaction.Options.Warnings
UselessPrivateAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessPrivate_Agda.Interaction.Options.Warnings
UselessPublicAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
userNamedAgda.Syntax.Common
UserWarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UserWarning_Agda.Interaction.Options.Warnings
UserWrittenAgda.Syntax.Common
UsesAgda.Compiler.JS.Syntax
usesAgda.Compiler.JS.Syntax
usesCopatternsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
useScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UseShowInstanceAgda.Interaction.Base
useTCAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
USmallAgda.Syntax.Internal
USSetAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
UStateAgda.TypeChecking.Rules.LHS.Unify.Types
usualWarningsAgda.Interaction.Options.Warnings
UTypeAgda.Syntax.Internal.Univ, Agda.Syntax.Internal