Agda-2.3.2: 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.TypeChecking.Rules.LHS.Unify
UId | Agda.Auto.Syntax
umodifyIORef | Agda.Auto.NarrowingSearch
unAbs | Agda.Syntax.Internal
unAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
unAppView | Agda.Syntax.Abstract.Views
unArg | Agda.Syntax.Common
UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unblockedTester | Agda.TypeChecking.MetaVars
unCommandM | Agda.Interaction.InteractionTop
unConName | Agda.TypeChecking.Test.Generators
uncons | Agda.Utils.List
uncurry3 | Agda.Utils.Tuple
uncurry4 | Agda.Utils.Tuple
unDeepSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
undef | Agda.Compiler.JS.Parser
Undefined | Agda.Compiler.JS.Syntax
unDefName | Agda.TypeChecking.Test.Generators
underAbs | Agda.TypeChecking.Substitute
underAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
underAbstraction_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
UnderInf | Agda.TypeChecking.Positivity
underLambdas | Agda.TypeChecking.Substitute
Underscore |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
underscore | Agda.Syntax.Concrete.Pretty
Undo | Agda.Auto.NarrowingSearch
unDom | Agda.Syntax.Common
unEl | Agda.Syntax.Internal
unequal | Agda.Auto.Typecheck
UnequalBecauseOfUniverseConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unequals | Agda.Auto.Typecheck
UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTelescopes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unescape | Agda.Compiler.JS.Pretty
unescapes | Agda.Compiler.JS.Pretty
UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unExprView | Agda.Syntax.Concrete.Operators.Parser
unflattenTel | Agda.TypeChecking.Telescope
unfold | Agda.TypeChecking.MetaVars.Occurs
unfoldCorecursion | Agda.TypeChecking.CompiledClause.Match
unfoldDefinition | Agda.TypeChecking.Reduce
UnfoldStrategy | Agda.TypeChecking.MetaVars.Occurs
unfreezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unGraph | Agda.Utils.Graph
unguardedRecord | Agda.TypeChecking.Records
uniConstr | Agda.TypeChecking.Rules.LHS.Unify
Unifiable | Agda.TypeChecking.Rules.LHS.Unify
unifiable | Agda.Compiler.Epic.Injection
UnificationResult | Agda.TypeChecking.Rules.LHS.Unify
Unifies | Agda.TypeChecking.Rules.LHS.Unify
Unify | Agda.TypeChecking.Rules.LHS.Unify
unify | Agda.Compiler.Epic.Injection
UnifyEnv | Agda.TypeChecking.Rules.LHS.Unify
UnifyException | Agda.TypeChecking.Rules.LHS.Unify
unifyexp | Agda.Auto.CaseSplit
unifyI | Agda.Compiler.Epic.Forcing
unifyIndices | Agda.TypeChecking.Rules.LHS.Unify
unifyIndices_ | Agda.TypeChecking.Rules.LHS.Unify
UnifyMayPostpone | Agda.TypeChecking.Rules.LHS.Unify
UnifyOutput | Agda.TypeChecking.Rules.LHS.Unify
unifyPointers | Agda.TypeChecking.Conversion
UnifyState | Agda.TypeChecking.Rules.LHS.Unify
UninstantiatedDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UninstantiatedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
union |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.Trie
4 (Function) | Agda.Termination.CallGraph
5 (Function) | Agda.Utils.Graph
6 (Function) | Agda.Compiler.JS.Substitution
unionConstraints | Agda.Compiler.Epic.Injection
unions |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.Graph
unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
unionWith | Agda.Utils.HashMap
unionWithM | Agda.Utils.Map
uniqBy | Agda.Utils.List
uniSub | Agda.TypeChecking.Rules.LHS.Unify
UNIT | Agda.Compiler.Epic.AuxAST
univar | Agda.Auto.SearchControl
Unknown | Agda.TypeChecking.Positivity
unknown | Agda.Termination.CallGraph
UnknownName | Agda.Syntax.Scope.Monad
UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions
UnknownSort | Agda.Auto.Syntax
unlessM | Agda.Utils.Monad
unless_ | Agda.Utils.Monad
unLevel | Agda.TypeChecking.Level
unLevelAtom | Agda.TypeChecking.Substitute
unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unLvl | Agda.TypeChecking.Primitive
unMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
unnamed | Agda.Syntax.Common
unNat | Agda.TypeChecking.Primitive
unNoType | Agda.TypeChecking.Test.Generators
unqhname | Agda.Compiler.MAlonzo.Misc
unqname | Agda.Compiler.Epic.CompileState
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.Quote
unquote | Agda.TypeChecking.Quote
unquoteFailed | Agda.TypeChecking.Quote
unquoteFailedGeneric | Agda.TypeChecking.Quote
unquoteH | Agda.TypeChecking.Quote
unquoteN | Agda.TypeChecking.Quote
UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnreducedLevel | Agda.Syntax.Internal
unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc
unsafePragmaOptions | Agda.Interaction.Options
unScope | Agda.TypeChecking.Rules.Term
unSizedList | Agda.TypeChecking.Test.Generators
unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
UnsolvedConstraint | Agda.Interaction.Highlighting.Precise
UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedConstraints | Agda.TypeChecking.Errors
UnsolvedMeta | Agda.Interaction.Highlighting.Precise
UnsolvedMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedMetaVariables | Agda.TypeChecking.Errors
unStr | Agda.TypeChecking.Primitive
unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unUnify | Agda.TypeChecking.Rules.LHS.Unify
unusableRelevance | Agda.TypeChecking.Irrelevance
Unused |
1 (Data Constructor) | Agda.TypeChecking.Free
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnusedArg | Agda.Syntax.Common
UnusedVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unusedVars | Agda.TypeChecking.Free
unVarName | Agda.TypeChecking.Test.Generators
unwrap | Agda.Compiler.MAlonzo.Pretty
unYesType | Agda.TypeChecking.Test.Generators
unzip | Agda.Utils.Map
unzip3 | Agda.Utils.Map
unzipMaybe | Agda.Utils.Maybe
updateDefArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateDefCompiledRep | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateDefinition | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateDefPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateDefType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
updateLast | Agda.Utils.List
updateMeta | Agda.TypeChecking.MetaVars
updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateNamedArg | Agda.Syntax.Common
updateProblemRest | Agda.TypeChecking.Rules.LHS.ProblemRest
updateProblemRest_ | Agda.TypeChecking.Rules.LHS.ProblemRest
updatePtr | Agda.Utils.Pointer, Agda.Syntax.Internal
updatePtrM | Agda.Utils.Pointer, Agda.Syntax.Internal
updateShared | Agda.Syntax.Internal
updateSharedFM | Agda.Syntax.Internal
updateSharedM | Agda.Syntax.Internal
updateSharedTerm | Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateSharedTermF | Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateSharedTermT | Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateTheDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ureadIORef | Agda.Auto.NarrowingSearch
ureadmodifyIORef | Agda.Auto.NarrowingSearch
UReduce | Agda.TypeChecking.Rules.LHS.Unify
ureduce | Agda.TypeChecking.Rules.LHS.Unify
usage | Agda.Interaction.Options
UseBoundNames |
1 (Type/Class) | Agda.Syntax.Concrete.Operators
2 (Data Constructor) | Agda.Syntax.Concrete.Operators
usedSeed | Agda.Utils.QuickCheck
usedSize | Agda.Utils.QuickCheck
useInjectivity | Agda.TypeChecking.Injectivity
UselessAbstract | Agda.Syntax.Concrete.Definitions
UselessPrivate | Agda.Syntax.Concrete.Definitions
UseLit | Agda.TypeChecking.Test.Generators
useLitChar | Agda.TypeChecking.Test.Generators
UseLiterals | Agda.TypeChecking.Test.Generators
useLitFloat | Agda.TypeChecking.Test.Generators
useLitInt | Agda.TypeChecking.Test.Generators
useLitString | Agda.TypeChecking.Test.Generators
useNamesFromPattern | Agda.TypeChecking.Rules.LHS.ProblemRest
Uses | Agda.Compiler.JS.Syntax
uses | Agda.Compiler.JS.Syntax
Using | Agda.Syntax.Concrete
UsingOrHiding | Agda.Syntax.Concrete
usingOrHiding | Agda.Syntax.Concrete
USt | Agda.TypeChecking.Rules.LHS.Unify
uwriteIORef | Agda.Auto.NarrowingSearch