Agda-2.6.2.2.20230105: 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.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
unBraveAgda.Syntax.Internal
unBruijnAgda.TypeChecking.CompiledClause.Compile
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
underAbsAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
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
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.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
unequalsAgda.Auto.Typecheck
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
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
unfoldInlinedAgda.TypeChecking.Reduce
unfoldrAgda.Utils.List1
UnfoldStrategyAgda.TypeChecking.MetaVars.Occurs
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
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
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
UnifiesToAgda.Auto.CaseSplit
UnifyAgda.Auto.CaseSplit
unifyAgda.Auto.CaseSplit
unify'Agda.Auto.CaseSplit
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
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.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
unifyVarAgda.Auto.CaseSplit
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.BiMap
8 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
9 (Function)Agda.Compiler.JS.Substitution
10 (Function)Agda.Utils.Favorites
11 (Function)Agda.Termination.CallMatrix
12 (Function)Agda.Termination.CallGraph
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
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.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
UnknownSortAgda.Auto.Syntax
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
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.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
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
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.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedConstraintAgda.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.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
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
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.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateAt 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.AssocList
updateBenchmarkAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateBenchmarkingStatusAgda.TypeChecking.Monad.Benchmark
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
updateHeadAgda.Utils.List
updateHeadsAgda.TypeChecking.Injectivity
updateInstanceDefsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateInteractionPointsAfterAgda.Interaction.InteractionTop
updateLastAgda.Utils.List
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
ureadIORefAgda.Auto.NarrowingSearch
ureadmodifyIORefAgda.Auto.NarrowingSearch
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
UselessPatternDeclarationForRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPatternDeclarationForRecord_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
UsesFloat 
1 (Type/Class)Agda.Compiler.MAlonzo.Compiler
2 (Data Constructor)Agda.Compiler.MAlonzo.Compiler
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
UStateAgda.TypeChecking.Rules.LHS.Unify.Types
usualWarningsAgda.Interaction.Options.Warnings
uwriteIORefAgda.Auto.NarrowingSearch