Agda

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
UnboundNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnboundName_Agda.Interaction.Options.Errors
UnboundVariablesInPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnboundVariablesInPatternSynonym_Agda.Interaction.Options.Errors
unBraveAgda.Syntax.Internal
unBruijnAgda.TypeChecking.CompiledClause.Compile
unBuiltinAccessAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unCallSiteAgda.Utils.CallStack
UnconfirmedReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
uncons 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
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
UnequalCohesionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalCohesion_Agda.Interaction.Options.Errors
UnequalFinitenessAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalFiniteness_Agda.Interaction.Options.Errors
UnequalHidingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalHiding_Agda.Interaction.Options.Errors
UnequalLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalLevel_Agda.Interaction.Options.Errors
UnequalPolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalPolarity_Agda.Interaction.Options.Errors
UnequalQuantityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalQuantity_Agda.Interaction.Options.Errors
UnequalRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalRelevance_Agda.Interaction.Options.Errors
UnequalSortsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalSorts_Agda.Interaction.Options.Errors
UnequalTermsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalTerms_Agda.Interaction.Options.Errors
unescapeAgda.Compiler.JS.Pretty
unescapesAgda.Compiler.JS.Pretty
UnexpectedModalityAnnotationInParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedModalityAnnotationInParameter_Agda.Interaction.Options.Errors
UnexpectedParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedParameter_Agda.Interaction.Options.Errors
UnexpectedTypeSignatureForParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedTypeSignatureForParameter_Agda.Interaction.Options.Errors
UnexpectedWhereAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedWhere_Agda.Interaction.Options.Errors
UnexpectedWithPatternsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedWithPatterns_Agda.Interaction.Options.Errors
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
UnfoldingOutsideOpaque_Agda.Interaction.Options.Errors
UnfoldingWrongNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnfoldingWrongName_Agda.Interaction.Options.Warnings
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.Interaction.Options, Agda.Syntax.Concrete.Pretty
UnicodeOrAsciiAgda.Syntax.Concrete.Glyph, Agda.Interaction.Options, Agda.Syntax.Concrete.Pretty
UnicodeSubscriptAgda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Concrete, 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
UnificationStuck_Agda.Interaction.Options.Errors
UnifiesAgda.TypeChecking.Rules.LHS.Unify
UnifyBlockedAgda.TypeChecking.Rules.LHS.Unify
UnifyConflictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyConflict_Agda.Interaction.Options.Errors
UnifyCycleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyCycle_Agda.Interaction.Options.Errors
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
union 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Map1
3 (Function)Agda.Utils.Set1
4 (Function)Agda.Utils.Bag
5 (Function)Agda.Utils.BoolSet
6 (Function)Agda.Utils.SmallSet
7 (Function)Agda.Utils.Trie
8 (Function)Agda.Utils.List1
9 (Function)Agda.Utils.Favorites
10 (Function)Agda.Utils.BiMap
11 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
12 (Function)Agda.Termination.CallMatrix
13 (Function)Agda.Termination.CallGraph
14 (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.Map1
3 (Function)Agda.Utils.Set1
4 (Function)Agda.Utils.Bag
5 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionSignaturesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unionsMaybeWithAgda.Utils.Maybe
unionsWith 
1 (Function)Agda.Utils.Map1
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionWith 
1 (Function)Agda.Utils.Map1
2 (Function)Agda.Utils.Trie
3 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionWithKeyAgda.Utils.Map1
uniqOnAgda.Utils.List
uniqueIntAgda.Utils.Graph.AdjacencyMap.Unidirectional
UniqueOpaqueAgda.Syntax.Common
unitCohesionAgda.Syntax.Common
unitComposeAgda.TypeChecking.SizedTypes.Utils
unitModalityAgda.Syntax.Common
unitPolarityAgda.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
UnknownBackendAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnknownBackend_Agda.Interaction.Options.Errors
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.Map1
2 (Function)Agda.Utils.Set1
3 (Function)Agda.Utils.Null
4 (Function)Agda.Utils.List1
unlessNullM 
1 (Function)Agda.Utils.Map1
2 (Function)Agda.Utils.Set1
3 (Function)Agda.Utils.Null
4 (Function)Agda.Utils.List1
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.Concrete
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
unquotableNameAgda.TypeChecking.Errors.Names
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
UnquoteDefRequiresSignature_Agda.Interaction.Options.Errors
UnquoteDefSAgda.Syntax.Abstract
UnquoteErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unquoteErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unquoteErrorNameAgda.TypeChecking.Errors.Names
unquoteErrorNameStringAgda.Interaction.Options.Errors
UnquoteError_ 
1 (Type/Class)Agda.Interaction.Options.Errors
2 (Data Constructor)Agda.Interaction.Options.Errors
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
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
unsafeFromMapAgda.Utils.Map1
unsafeFromSetAgda.Utils.Set1
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
UnusableAtModality_Agda.Interaction.Options.Errors
UnusedAgda.TypeChecking.Positivity.Occurrence
UnusedPolarityAgda.Syntax.Common
unusedVarAgda.Termination.Monad
UnusedVariableInPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnusedVariableInPatternSynonym_Agda.Interaction.Options.Errors
UnusedVariablesInDisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnusedVariablesInDisplayForm_Agda.Interaction.Options.Warnings
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
unzipWith 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
update 
1 (Function)Agda.Utils.Map1
2 (Function)Agda.Utils.AssocList
3 (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.Map1
2 (Function)Agda.Utils.AssocList
3 (Function)Agda.Utils.List
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
updateLookupWithKeyAgda.Utils.Map1
updateMaxAgda.Utils.Map1
updateMaxWithKeyAgda.Utils.Map1
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
updateMinAgda.Utils.Map1
updateMinWithKeyAgda.Utils.Map1
updateNamedArgAgda.Syntax.Common
updateNamedArgAAgda.Syntax.Common
updatePersistentStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updatePreconditionAgda.Utils.BiMap
updateProblemRestAgda.TypeChecking.Rules.LHS.ProblemRest
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
updateWithKeyAgda.Utils.Map1
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
usablePolarityAgda.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
UsedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
UselessPublicAnonymousModuleAgda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicLetAgda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicNoOpenAgda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicPreambleAgda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicReasonAgda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublic_Agda.Interaction.Options.Warnings
UselessTacticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessTactic_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
UserBinderNameAgda.Syntax.Common
userNamedAgda.Syntax.Common
UserWarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UserWarningsAgda.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