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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - U

U | Agda.Mimer.Options
UE | Agda.TypeChecking.Coverage.SplitClause
uglyShowName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
ULarge | Agda.Syntax.Internal
unAbs | Agda.Syntax.Internal
unAbsN | Agda.TypeChecking.Names
unambiguous | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
unAmbQ | Agda.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
unArg | Agda.Syntax.Common
unBind | Agda.Syntax.Abstract
unbindVariable | Agda.Syntax.Scope.Monad
UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unblockDef | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockedTester | Agda.TypeChecking.MetaVars
unblockMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnAll | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAll | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAllMetas | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAllMetasIn | Agda.Syntax.Internal.MetaVars
UnblockOnAny | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAny | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAnyMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnAnyMetaIn | Agda.Syntax.Internal.MetaVars
unblockOnBoth | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnDef | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnDef | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnEither | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
UnblockOnProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockOnProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unblockProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
unBlockT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnboundName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnboundName_ | Agda.Interaction.Options.Errors
UnboundVariablesInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnboundVariablesInPatternSynonym_ | Agda.Interaction.Options.Errors
unBrave | Agda.Syntax.Internal
unBruijn | Agda.TypeChecking.CompiledClause.Compile
unBuiltinAccess | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unCallSite | Agda.Utils.CallStack
UnconfirmedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
uncons |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.List1
unConstV | Agda.TypeChecking.Level
uncurry3 | Agda.Utils.Tuple
uncurry4 | Agda.Utils.Tuple
uncurrys | Agda.Utils.TypeLevel
unDeepSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Undefined | Agda.Compiler.JS.Syntax
underAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
underAbstraction' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
underAbstractionAbs | Agda.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
Underapplied | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
underBinder | Agda.TypeChecking.Free.Lazy
underBinder' | Agda.TypeChecking.Free.Lazy
UnderComposition |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
underConstructor | Agda.TypeChecking.Free.Lazy
underFlexRig | Agda.TypeChecking.Free.Lazy
UnderInf | Agda.TypeChecking.Positivity.Occurrence
UnderLambda |
1 (Type/Class) | Agda.Compiler.Treeless.Subst
2 (Data Constructor) | Agda.Compiler.Treeless.Subst
underLambda | Agda.Compiler.Treeless.Subst
underlyingRange | Agda.TypeChecking.Serialise.Instances.Common
underModality | Agda.TypeChecking.Free.Lazy
underOpaqueId | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
underQuantity | Agda.TypeChecking.Free.Lazy
underRelevance | Agda.TypeChecking.Free.Lazy
Underscore |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
underscore | Agda.Syntax.Common
unDom | Agda.Syntax.Internal
unDrop | Agda.Utils.Permutation
unEl | Agda.Syntax.Internal
UnequalCohesion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalCohesion_ | Agda.Interaction.Options.Errors
UnequalFiniteness | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalFiniteness_ | Agda.Interaction.Options.Errors
UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalHiding_ | Agda.Interaction.Options.Errors
UnequalLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalLevel_ | Agda.Interaction.Options.Errors
UnequalPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalPolarity_ | Agda.Interaction.Options.Errors
UnequalQuantity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalQuantity_ | Agda.Interaction.Options.Errors
UnequalRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalRelevance_ | Agda.Interaction.Options.Errors
UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalSorts_ | Agda.Interaction.Options.Errors
UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalTerms_ | Agda.Interaction.Options.Errors
unescape | Agda.Compiler.JS.Pretty
unescapes | Agda.Compiler.JS.Pretty
UnexpectedModalityAnnotationInParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedModalityAnnotationInParameter_ | Agda.Interaction.Options.Errors
UnexpectedParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedParameter_ | Agda.Interaction.Options.Errors
UnexpectedTypeSignatureForParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedTypeSignatureForParameter_ | Agda.Interaction.Options.Errors
UnexpectedWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedWhere_ | Agda.Interaction.Options.Errors
UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnexpectedWithPatterns_ | Agda.Interaction.Options.Errors
unExprView | Agda.Syntax.Concrete.Operators.Parser
unflattenTel | Agda.TypeChecking.Telescope
unflattenTel' | Agda.TypeChecking.Telescope
unfold |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.TypeChecking.MetaVars.Occurs
unfoldB | Agda.TypeChecking.MetaVars.Occurs
unfoldCorecursion | Agda.TypeChecking.Reduce
unfoldCorecursionE | Agda.TypeChecking.Reduce
unfoldDefinitionE | Agda.TypeChecking.Reduce
unfoldDefinitionStep | Agda.TypeChecking.Reduce
Unfolding | Agda.Syntax.Concrete
UnfoldingDecl | Agda.Syntax.Abstract
UnfoldingDeclS | Agda.Syntax.Abstract
UnfoldingOutsideOpaque | Agda.Syntax.Concrete.Definitions.Errors
UnfoldingOutsideOpaque_ | Agda.Interaction.Options.Errors
UnfoldingWrongName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnfoldingWrongName_ | Agda.Interaction.Options.Warnings
unfoldInlined | Agda.TypeChecking.Reduce
unfoldr | Agda.Utils.List1
UnfoldStrategy | Agda.TypeChecking.MetaVars.Occurs
UnfoldTransparentName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnfoldTransparentName_ | Agda.Interaction.Options.Warnings
UnFreezeMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unfreezeMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unfreezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ungatherRecordDirectives | Agda.Syntax.Concrete
Unguarded | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
unguardedRecord | Agda.TypeChecking.Records
UnGuardedRhs | Agda.Utils.Haskell.Syntax
unguardedVars | Agda.TypeChecking.Free
UnicodeOk | Agda.Syntax.Concrete.Glyph, Agda.Interaction.Options, Agda.Syntax.Concrete.Pretty
UnicodeOrAscii | Agda.Syntax.Concrete.Glyph, Agda.Interaction.Options, Agda.Syntax.Concrete.Pretty
UnicodeSubscript | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Compiler.Backend
UnificationFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnificationMeta | Agda.Syntax.Info
UnificationResult | Agda.TypeChecking.Rules.LHS.Unify
UnificationResult' | Agda.TypeChecking.Rules.LHS.Unify
UnificationStep | Agda.TypeChecking.Rules.LHS.Unify.Types
UnificationStuck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnificationStuck_ | Agda.Interaction.Options.Errors
Unifies | Agda.TypeChecking.Rules.LHS.Unify
UnifyBlocked | Agda.TypeChecking.Rules.LHS.Unify
UnifyConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyConflict_ | Agda.Interaction.Options.Errors
UnifyCycle | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyCycle_ | Agda.Interaction.Options.Errors
unifyElims | Agda.TypeChecking.IApplyConfluence
unifyElimsMeta | Agda.TypeChecking.IApplyConfluence
UnifyEquiv | Agda.TypeChecking.Coverage.SplitClause
UnifyIndices | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
unifyIndices | Agda.TypeChecking.Rules.LHS.Unify
unifyIndices' | Agda.TypeChecking.Rules.LHS.Unify
UnifyIndicesNotVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyLog | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyLog' | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyLogEntry | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyLogT | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyOutput |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Unify.Types
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify.Types
unifyProof | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyRecursiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyReflexiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyState | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyStep | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyStepT | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyStuck | Agda.TypeChecking.Rules.LHS.Unify
unifySubst | Agda.TypeChecking.Rules.LHS.Unify.Types
UnifyUnusableModality | Agda.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
unionBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unionCompared | Agda.Utils.Favorites
unionMaybeWith |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
unionPrecondition | Agda.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
unionSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unionsMaybeWith | Agda.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
unionWithKey | Agda.Utils.Map1
uniqOn | Agda.Utils.List
uniqueInt | Agda.Utils.Graph.AdjacencyMap.Unidirectional
UniqueOpaque | Agda.Syntax.Common
unitCohesion | Agda.Syntax.Common
unitCompose | Agda.TypeChecking.SizedTypes.Utils
unitModality | Agda.Syntax.Common
unitPolarity | Agda.Syntax.Common
unitQuantity | Agda.Syntax.Common
unitRelevance | Agda.Syntax.Common
unit_con | Agda.Utils.Haskell.Syntax
Univ |
1 (Type/Class) | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
univChecks | Agda.TypeChecking.Rules.Application
UniverseCheck | Agda.Syntax.Common
universeCheck | Agda.Syntax.Concrete.Definitions.Types
universeCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
univFibrancy | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
UnivSize | Agda.Syntax.Internal
UnivSort | Agda.Syntax.Internal
univSort | Agda.TypeChecking.Substitute
univSort' | Agda.TypeChecking.Substitute
univUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
UnkindedVar | Agda.Utils.Haskell.Syntax
unKleisli | Agda.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
unknown | Agda.Termination.Order
UnknownAttribute | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
UnknownAttribute_ | Agda.Interaction.Options.Warnings
UnknownBackend | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnknownBackend_ | Agda.Interaction.Options.Errors
UnknownError | Agda.Interaction.ExitCode
UnknownField | Agda.Interaction.Library.Base
UnknownFixityInMixfixDecl | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UnknownFixityInMixfixDecl_ | Agda.Interaction.Options.Warnings
unknownFreeVariables | Agda.Syntax.Common
UnknownFVs | Agda.Syntax.Common
UnknownHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnknownName | Agda.Syntax.Scope.Base
UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UnknownNamesInFixityDecl_ | Agda.Interaction.Options.Warnings
UnknownNamesInPolarityPragmas | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UnknownNamesInPolarityPragmas_ | Agda.Interaction.Options.Warnings
UnknownPolarity | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
UnknownPolarity_ | Agda.Interaction.Options.Warnings
UnknownS | Agda.Syntax.Reflected
unlabelPatVars | Agda.Syntax.Internal.Pattern
unlamView | Agda.TypeChecking.Substitute
unless | Agda.Utils.Monad
unlessDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unlessM | Agda.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
unLevel | Agda.TypeChecking.Level
unlevelWithKit | Agda.TypeChecking.Level
unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unLvl | Agda.TypeChecking.Primitive
unM | Agda.Termination.SparseMatrix
unmapListT | Agda.Utils.ListT
unMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unName | Agda.TypeChecking.Names
unnamed | Agda.Syntax.Common
unNamedArg | Agda.Syntax.Concrete
unnamedArg | Agda.Syntax.Common
unNat | Agda.TypeChecking.Primitive
unNice | Agda.Syntax.Concrete.Definitions.Monad
unNLM | Agda.TypeChecking.Rewriting.NonLinMatch
unNoSubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
unnumberPatVars | Agda.Syntax.Internal.Pattern
unpackUnquoteM | Agda.TypeChecking.Unquote
unPiView | Agda.Syntax.Abstract.Views
unPlusV | Agda.TypeChecking.Level
unPM | Agda.Syntax.Parser
unProjView | Agda.TypeChecking.ProjectionLike
unPureConversionT | Agda.TypeChecking.Conversion.Pure
unqhname | Agda.Compiler.MAlonzo.Misc
UnQual | Agda.Utils.Haskell.Syntax
Unqualified | Agda.Mimer.Options
unqualify | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
unquotableName | Agda.TypeChecking.Errors.Names
Unquote |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Type/Class) | Agda.TypeChecking.Unquote
unquote | Agda.TypeChecking.Unquote
UnquoteData |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
UnquoteDataS | Agda.Syntax.Abstract
UnquoteDecl |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
UnquoteDeclS | Agda.Syntax.Abstract
UnquoteDef |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
UnquoteDefRequiresSignature | Agda.Syntax.Concrete.Definitions.Errors
UnquoteDefRequiresSignature_ | Agda.Interaction.Options.Errors
UnquoteDefS | Agda.Syntax.Abstract
UnquoteError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unquoteError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unquoteErrorName | Agda.TypeChecking.Errors.Names
unquoteErrorNameString | Agda.Interaction.Options.Errors
UnquoteError_ |
1 (Type/Class) | Agda.Interaction.Options.Errors
2 (Data Constructor) | Agda.Interaction.Options.Errors
UnquoteFailed | Agda.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
UnquoteM | Agda.TypeChecking.Unquote
unquoteM | Agda.TypeChecking.Rules.Term
unquoteN | Agda.TypeChecking.Unquote
unquoteNormalise | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unquoteNString | Agda.TypeChecking.Unquote
UnquoteRes | Agda.TypeChecking.Unquote
UnquoteState | Agda.TypeChecking.Unquote
unquoteString | Agda.TypeChecking.Unquote
UnquoteTactic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unquoteTactic | Agda.TypeChecking.Rules.Term
unquoteTCM | Agda.TypeChecking.Unquote
unquoteTop | Agda.TypeChecking.Rules.Decl
unranged | Agda.Syntax.Common
Unreachable |
1 (Data Constructor) | Agda.Utils.Impossible
2 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnreachableClauses_ | Agda.Interaction.Options.Warnings
unReduceM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Unrelated | Agda.Syntax.Common
unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc
unsafeComparePointers | Agda.Utils.Unsafe
unsafeDeclarationWarning | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
unsafeDeclarationWarning' | Agda.Syntax.Concrete.Definitions.Errors
unsafeEscapeContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unsafeFromMap | Agda.Utils.Map1
unsafeFromSet | Agda.Utils.Set1
unsafeInTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unsafeModifyContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unsafePragma | Agda.Syntax.Concrete.Definitions.Errors
unsafePragmaOptions | Agda.Interaction.Options
unsafeSetUnicodeOrAscii | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
unsafeTopLevelModuleName | Agda.Syntax.TopLevelModuleName
unScope | Agda.Syntax.Abstract.Views
unSingleLevel | Agda.TypeChecking.Level
unSingleLevels | Agda.TypeChecking.Level
unSizeExpr | Agda.TypeChecking.SizedTypes.Pretty
unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedConstraint | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedConstraints_ | Agda.Interaction.Options.Warnings
UnsolvedInteractionMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedInteractionMetas_ | Agda.Interaction.Options.Warnings
UnsolvedMeta | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
UnsolvedMetaVariables | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedMetaVariables_ | Agda.Interaction.Options.Warnings
unsolvedWarnings | Agda.Interaction.Options.Warnings
unSpine | Agda.Syntax.Internal
unSpine' | Agda.Syntax.Internal
UnsupportedAttribute | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
UnsupportedAttribute_ | Agda.Interaction.Options.Warnings
UnsupportedCxt | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
UnsupportedIndexedMatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsupportedIndexedMatch_ | Agda.Interaction.Options.Warnings
UnsupportedYet | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
UntaggedValue | Agda.Interaction.JSON
unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnusableAtModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnusableAtModality_ | Agda.Interaction.Options.Errors
Unused | Agda.TypeChecking.Positivity.Occurrence
UnusedPolarity | Agda.Syntax.Common
unusedVar | Agda.Termination.Monad
UnusedVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnusedVariableInPatternSynonym_ | Agda.Interaction.Options.Errors
UnusedVariablesInDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnusedVariablesInDisplayForm_ | Agda.Interaction.Options.Warnings
unviewProjectedVar | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unwords | Agda.Utils.List1
unwords1 | Agda.Utils.String
unwrapUnaryRecords | Agda.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
update1 | Agda.Utils.Update
update2 | Agda.Utils.Update
updateAllowedReductions | Agda.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
updateBenchmarkingStatus | Agda.TypeChecking.Monad.Benchmark
updateBlocker | Agda.TypeChecking.Constraints
updateCompiledClauses | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateCovering | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefArgOccurrences | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefBlocked | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefCompiledRep | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefCopatternLHS | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefinitions | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefPolarity | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateDefType | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateEtaForRecord | Agda.TypeChecking.Records
updateFunClauses | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateHead |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.List1
updateHeads | Agda.TypeChecking.Injectivity
updateInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateInteractionPointsAfter | Agda.Interaction.InteractionTop
updateLast |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.List1
updateLookupWithKey | Agda.Utils.Map1
updateMax | Agda.Utils.Map1
updateMaxWithKey | Agda.Utils.Map1
updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateMetaVarTCM | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateMin | Agda.Utils.Map1
updateMinWithKey | Agda.Utils.Map1
updateNamedArg | Agda.Syntax.Common
updateNamedArgA | Agda.Syntax.Common
updatePersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updatePrecondition | Agda.Utils.BiMap
updateProblemRest | Agda.TypeChecking.Rules.LHS.ProblemRest
Updater | Agda.Utils.Update
Updater1 | Agda.Utils.Update
updater1 | Agda.Utils.Update
Updater2 | Agda.Utils.Update
updater2 | Agda.Utils.Update
UpdaterT | Agda.Utils.Update
updates1 | Agda.Utils.Update
updates2 | Agda.Utils.Update
updateScopeLocals | Agda.Syntax.Scope.Base
updateScopeNameSpaces | Agda.Syntax.Scope.Base
updateScopeNameSpacesM | Agda.Syntax.Scope.Base
updateTheDef | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateVarsToBind | Agda.Syntax.Scope.Base
updateWithKey | Agda.Utils.Map1
upperBounds | Agda.TypeChecking.SizedTypes.WarshallSolver
UProp | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
UsableAtMod | Agda.Interaction.Base
UsableAtModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
usableAtModality | Agda.TypeChecking.Irrelevance
usableAtModality' | Agda.TypeChecking.Irrelevance
usableCohesion | Agda.Syntax.Common
usableMod | Agda.TypeChecking.Irrelevance
usableModAbs | Agda.TypeChecking.Irrelevance
UsableModality | Agda.TypeChecking.Irrelevance
usableModality | Agda.Syntax.Common
usablePolarity | Agda.Syntax.Common
usableQuantity | Agda.Syntax.Common
usableRel | Agda.TypeChecking.Irrelevance
UsableRelevance | Agda.TypeChecking.Irrelevance
usableRelevance | Agda.Syntax.Common
UsableSizeVars | Agda.Termination.Monad
usableSizeVars | Agda.Termination.Monad
usage | Agda.Interaction.Options
usageInfo | Agda.Utils.GetOpt
usageWarning | Agda.Interaction.Options.Warnings
use | Agda.Utils.Lens
useConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
usedArguments | Agda.Compiler.Treeless.Unused
useDefaultFixity | Agda.Syntax.Notation
UsedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UseEverything | Agda.Syntax.Common
UseForce | Agda.Interaction.Base
useInjectivity | Agda.TypeChecking.Injectivity
UselessAbstract | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessAbstract_ | Agda.Interaction.Options.Warnings
UselessHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessHiding_ | Agda.Interaction.Options.Warnings
UselessInline | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessInline_ | Agda.Interaction.Options.Warnings
UselessInstance | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessInstance_ | Agda.Interaction.Options.Warnings
UselessMacro | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessMacro_ | Agda.Interaction.Options.Warnings
UselessOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessOpaque_ | Agda.Interaction.Options.Warnings
UselessPatternDeclarationForRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPatternDeclarationForRecord_ | Agda.Interaction.Options.Warnings
UselessPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPragma_ | Agda.Interaction.Options.Warnings
UselessPrivate | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
UselessPrivate_ | Agda.Interaction.Options.Warnings
UselessPublic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicAnonymousModule | Agda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicLet | Agda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicNoOpen | Agda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicPreamble | Agda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublicReason | Agda.TypeChecking.Monad.Base.Warning, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublic_ | Agda.Interaction.Options.Warnings
UselessTactic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessTactic_ | Agda.Interaction.Options.Warnings
useNamesFromPattern | Agda.TypeChecking.Rules.LHS.ProblemRest
useNamesFromProblemEqs | Agda.TypeChecking.Rules.LHS.ProblemRest
useOriginFrom | Agda.TypeChecking.Rules.LHS.ProblemRest
usePatOrigin | Agda.TypeChecking.Substitute
usePatternInfo | Agda.TypeChecking.Substitute
useR | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UserBinderName | Agda.Syntax.Common
userNamed | Agda.Syntax.Common
UserWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UserWarning_ | Agda.Interaction.Options.Warnings
UserWritten | Agda.Syntax.Common
Uses | Agda.Compiler.JS.Syntax
uses | Agda.Compiler.JS.Syntax
usesCopatterns | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
useScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UseShowInstance | Agda.Interaction.Base
useTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
useTerPragma | Agda.TypeChecking.Rules.Def
Using |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Syntax.Concrete
using | Agda.Syntax.Common
Using' | Agda.Syntax.Common
UsingOnly | Agda.Syntax.Scope.Base
UsingOrHiding | Agda.Syntax.Scope.Base
usingOrHiding | Agda.Syntax.Scope.Base
USmall | Agda.Syntax.Internal
USSet | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
UState | Agda.TypeChecking.Rules.LHS.Unify.Types
usualWarnings | Agda.Interaction.Options.Warnings
UType | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal