Agda-2.2.10: 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
unAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
unAppView | Agda.Syntax.Abstract.Views
unArg | Agda.Syntax.Common
UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unblockedTester | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
unConName | Agda.TypeChecking.Test.Generators
uncurry3 | Agda.Utils.Tuple
unDefName | Agda.TypeChecking.Test.Generators
underAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
underAbstraction_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
Underscore |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
underscore | Agda.Syntax.Concrete.Pretty
Undo | Agda.Auto.NarrowingSearch
unEl | Agda.Syntax.Internal
unequal | Agda.Auto.Typecheck
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
UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unExprView | Agda.Syntax.Concrete.Operators.Parser
unflattenTel | Agda.TypeChecking.Telescope
unfoldCorecursion | Agda.TypeChecking.CompiledClause.Match
unfoldDefinition | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
unGraph | Agda.Utils.Graph
uniConstr | Agda.TypeChecking.Rules.LHS.Unify
unification | Agda.Compiler.Epic.Forcing
UnificationResult | Agda.TypeChecking.Rules.LHS.Unify
Unifies | Agda.TypeChecking.Rules.LHS.Unify
Unify | 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
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.Graph
2 (Function) | Agda.Utils.Trie
3 (Function) | Agda.Termination.CallGraph
unions | Agda.Utils.Graph
unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
unionWithM | Agda.Utils.Map
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, Agda.Interaction.GhciTop
UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions
UnknownSort | Agda.Auto.Syntax
unlessM | Agda.Utils.Monad
unLevelAtom | Agda.TypeChecking.Level
unLevelView | Agda.TypeChecking.Level
unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unLvl | Agda.TypeChecking.Primitive
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
UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc
unSizedList | Agda.TypeChecking.Test.Generators
unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedConstraints | Agda.Interaction.Imports
UnsolvedMeta | Agda.Interaction.Highlighting.Precise
UnsolvedMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedMetaVariables | Agda.Interaction.Imports
unStr | Agda.TypeChecking.Primitive
unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unUnify | Agda.TypeChecking.Rules.LHS.Unify
Unused | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unVarName | Agda.TypeChecking.Test.Generators
unYesType | Agda.TypeChecking.Test.Generators
updateMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updatePtr | Agda.Utils.Pointer
updateWithConstructorRanges | Agda.TypeChecking.With
ureadIORef | Agda.Auto.NarrowingSearch
ureadmodifyIORef | Agda.Auto.NarrowingSearch
ureduce | Agda.TypeChecking.Rules.LHS.Unify
usage | Agda.Interaction.Options
usedSeed | Agda.Utils.QuickCheck
usedSize | Agda.Utils.QuickCheck
useInjectivity | Agda.TypeChecking.Injectivity
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
Using | Agda.Syntax.Concrete
UsingOrHiding | Agda.Syntax.Concrete
usingOrHiding | Agda.Syntax.Concrete
USt | Agda.TypeChecking.Rules.LHS.Unify
uwriteIORef | Agda.Auto.NarrowingSearch