Agda-2.6.0.1: 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 |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base
2 (Data Constructor) | Agda.TypeChecking.Serialise.Base
uglyShowName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
UId | Agda.Auto.Syntax
umodifyIORef | Agda.Auto.NarrowingSearch
unAbs | Agda.Syntax.Internal
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 | 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
unblockedTester | Agda.TypeChecking.MetaVars
unBruijn | Agda.TypeChecking.CompiledClause.Compile
UnconfirmedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
uncons | Agda.Utils.List
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
underAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
underAbstraction |
1 (Function) | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function) | Agda.TypeChecking.Reduce.Monad
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_ |
1 (Function) | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function) | Agda.TypeChecking.Reduce.Monad
Underapplied | Agda.Syntax.Internal
underConstructor | 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
underLambdas | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
underlyingRange | Agda.TypeChecking.Serialise.Instances.Common
Underscore |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
underscore | Agda.Syntax.Common
Undo | Agda.Auto.NarrowingSearch
unDom | Agda.Syntax.Common
unDrop | Agda.Utils.Permutation
unEl | Agda.Syntax.Internal
unequal | Agda.Auto.Typecheck
UnequalBecauseOfUniverseConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unequals | Agda.Auto.Typecheck
UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnequalTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unescape | Agda.Compiler.JS.Pretty
unescapes | Agda.Compiler.JS.Pretty
UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unExprView | Agda.Syntax.Concrete.Operators.Parser
unflattenTel | Agda.TypeChecking.Telescope
unfold | Agda.TypeChecking.MetaVars.Occurs
unfoldCorecursion | Agda.TypeChecking.Reduce
unfoldCorecursionE | Agda.TypeChecking.Reduce
unfoldDefinition | Agda.TypeChecking.Reduce
unfoldDefinition' | Agda.TypeChecking.Reduce
unfoldDefinitionE | Agda.TypeChecking.Reduce
unfoldDefinitionStep | Agda.TypeChecking.Reduce
unfoldInlined | Agda.TypeChecking.Reduce
UnfoldStrategy | Agda.TypeChecking.MetaVars.Occurs
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
unfreezeMetas' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Unguarded |
1 (Data Constructor) | Agda.TypeChecking.Free.Lazy
2 (Data Constructor) | Agda.TypeChecking.Free
3 (Data Constructor) | Agda.TypeChecking.Free.Old
unguardedRecord | Agda.TypeChecking.Records
UnGuardedRhs | Agda.Utils.Haskell.Syntax
unguardedVars |
1 (Function) | Agda.TypeChecking.Free
2 (Function) | Agda.TypeChecking.Free.Old
UnicodeOk | Agda.Interaction.Options.IORefs
UnicodeOrAscii | Agda.Interaction.Options.IORefs
unicodeOrAscii | Agda.Interaction.Options.IORefs
UnicodeTest | Agda.Utils.Char
unicodeTests | Agda.Utils.Char
UnificationFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnificationResult | Agda.TypeChecking.Rules.LHS.Unify
UnificationResult' | Agda.TypeChecking.Rules.LHS.Unify
UnificationStuck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Unifies | Agda.TypeChecking.Rules.LHS.Unify
Unify | Agda.Auto.CaseSplit
unify | Agda.Auto.CaseSplit
unify' | Agda.Auto.CaseSplit
UnifyConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyCycle | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unifyexp | Agda.Auto.CaseSplit
UnifyIndices | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
unifyIndices | Agda.TypeChecking.Rules.LHS.Unify
UnifyIndicesNotVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyRecursiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnifyReflexiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unifyVar | Agda.Auto.CaseSplit
UninstantiatedDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
union |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.BiMap
4 (Function) | Agda.Utils.Bag
5 (Function) | Agda.Utils.Trie
6 (Function) | Agda.Compiler.JS.Substitution
7 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
8 (Function) | Agda.Utils.Favorites
9 (Function) | Agda.Termination.CallMatrix
10 (Function) | Agda.Termination.CallGraph
unionCompared | Agda.Utils.Favorites
unionMaybeWith |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
unionNe | Agda.Utils.NonemptyList
unions |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.Bag
4 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unionsWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionWith |
1 (Function) | Agda.Utils.HashMap
2 (Function) | Agda.Utils.Trie
3 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionWithKey | Agda.Utils.HashMap
unionWithM | Agda.Utils.Map
uniqOn | Agda.Utils.List
unitCompose | Agda.TypeChecking.SizedTypes.Utils
unit_con | Agda.Utils.Haskell.Syntax
univar | Agda.Auto.SearchControl
UniverseCheck | Agda.Syntax.Common
univInf | Agda.TypeChecking.Substitute
UnivSort | Agda.Syntax.Internal
univSort | Agda.TypeChecking.Substitute
univSort' | Agda.TypeChecking.Substitute
UnkindedVar | Agda.Utils.Haskell.Syntax
Unknown |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Termination.Order
unknown | Agda.Termination.Order
UnknownField | Agda.Interaction.Library.Parse
UnknownFixityInMixfixDecl | 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
UnknownNamesInFixityDecl_ | Agda.Interaction.Options.Warnings
UnknownNamesInPolarityPragmas | Agda.Syntax.Concrete.Definitions
UnknownNamesInPolarityPragmas_ | Agda.Interaction.Options.Warnings
UnknownS | Agda.Syntax.Reflected
UnknownSort | Agda.Auto.Syntax
unlabelPatVars | Agda.Syntax.Internal.Pattern
unless | Agda.Utils.Monad
unlessDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unlessM | Agda.Utils.Monad
unlessNull | Agda.Utils.Null
unlessNullM | Agda.Utils.Null
unLevel | Agda.TypeChecking.Level
unLevelAtom | Agda.TypeChecking.Substitute
unlevelWithKit | Agda.TypeChecking.Level
unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unLvl | Agda.TypeChecking.Primitive
unM | Agda.Termination.SparseMatrix
unMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unName | Agda.TypeChecking.Names
unnamed | Agda.Syntax.Common
unnamedArg | Agda.Syntax.Common
unNat | Agda.TypeChecking.Primitive
unnumberPatVars | Agda.Syntax.Internal.Pattern
unpackUnquoteM | Agda.TypeChecking.Unquote
unPlusV | Agda.TypeChecking.Level
unPM | Agda.Syntax.Parser
unProjView | Agda.TypeChecking.ProjectionLike
unqhname | Agda.Compiler.MAlonzo.Misc
UnQual | Agda.Utils.Haskell.Syntax
unqualify | Agda.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
unquote | Agda.TypeChecking.Unquote
UnquoteDecl |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
UnquoteDef |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
UnquoteDefRequiresSignature | Agda.Syntax.Concrete.Definitions
UnquoteError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
UnquotePanic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
UnreducedLevel | Agda.Syntax.Internal
unreducedLevel | Agda.Syntax.Internal
unReduceM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Unrelated | Agda.Syntax.Fixity
unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc
unsafePragmaOptions | Agda.Interaction.Options
unScope | Agda.Syntax.Abstract.Views
unSizeExpr | Agda.TypeChecking.SizedTypes.Solve
unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UnsolvedConstraint | 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.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
unStr | Agda.Utils.String
unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Unused | Agda.TypeChecking.Positivity.Occurrence
unusedVar | Agda.Termination.Monad
UnusedVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
unVersionView | Agda.Interaction.Library
unzip |
1 (Function) | Agda.Utils.Map
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
unzip3 | Agda.Utils.Map
unzipMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
update |
1 (Function) | Agda.Utils.HashMap
2 (Function) | Agda.Utils.AssocList
update1 | Agda.Utils.Update
update2 | Agda.Utils.Update
updateAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateAt |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.AssocList
updateBenchmark | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateBenchmarkingStatus | Agda.TypeChecking.Monad.Benchmark
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
updateDefCompiledRep | 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
updateFunClauses | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateFunCopatternLHS | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateHead | Agda.Utils.List
updateHeads | Agda.TypeChecking.Injectivity
updateInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateInteractionPointsAfter | Agda.Interaction.InteractionTop
updateLast | Agda.Utils.List
updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateNamedArg | Agda.Syntax.Common
updatePersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
updateProblemRest | Agda.TypeChecking.Rules.LHS.ProblemRest
updatePtr | Agda.Utils.Pointer
updatePtrM | Agda.Utils.Pointer
Updater | Agda.Utils.Update
Updater1 | Agda.Utils.Update
updater1 | Agda.Utils.Update
Updater2 | Agda.Utils.Update
updater2 | 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
upperBounds | Agda.TypeChecking.SizedTypes.WarshallSolver
ureadIORef | Agda.Auto.NarrowingSearch
ureadmodifyIORef | Agda.Auto.NarrowingSearch
usableMod | Agda.TypeChecking.Irrelevance
UsableModality | Agda.TypeChecking.Irrelevance
usableModality | 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
usageWarning | Agda.Interaction.Options.Warnings
use | Agda.Utils.Lens
usedArguments | Agda.Compiler.Treeless.Unused
useDefaultFixity | Agda.Syntax.Fixity
UseEverything | Agda.Syntax.Common
UseForce | Agda.Interaction.BasicOps
useInjectivity | Agda.TypeChecking.Injectivity
UselessAbstract | Agda.Syntax.Concrete.Definitions
UselessAbstract_ | 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
UselessInstance_ | Agda.Interaction.Options.Warnings
UselessPrivate | Agda.Syntax.Concrete.Definitions
UselessPrivate_ | Agda.Interaction.Options.Warnings
UselessPublic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UselessPublic_ | Agda.Interaction.Options.Warnings
useNamesFromPattern | Agda.TypeChecking.Rules.LHS.ProblemRest
useOriginFrom | Agda.TypeChecking.Rules.LHS.ProblemRest
usePatOrigin | Agda.TypeChecking.Substitute
useR | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
UserWarning | 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
UseShowInstance | Agda.Interaction.BasicOps
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
UsingOrHiding | Agda.Syntax.Scope.Base
usingOrHiding | Agda.Syntax.Scope.Base
usualWarnings | Agda.Interaction.Options.Warnings
uwriteIORef | Agda.Auto.NarrowingSearch