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

Index - U

UAgda.TypeChecking.Rules.LHS.Unify
UIdAgda.Auto.Syntax
umodifyIORefAgda.Auto.NarrowingSearch
unAbsAgda.Syntax.Internal
unAmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
unAppViewAgda.Syntax.Abstract.Views
unArgAgda.Syntax.Common
UnBlockAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unblockedTesterAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
unConNameAgda.TypeChecking.Test.Generators
uncurry3Agda.Utils.Tuple
undefAgda.Compiler.JS.Parser
UndefinedAgda.Compiler.JS.Syntax
unDefNameAgda.TypeChecking.Test.Generators
underAbsAgda.TypeChecking.MetaVars.Occurs
underAbstractionAgda.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
underscoreAgda.Syntax.Concrete.Pretty
UndoAgda.Auto.NarrowingSearch
unElAgda.Syntax.Internal
unElimAgda.TypeChecking.Eliminators
unElimViewAgda.TypeChecking.Eliminators
unequalAgda.Auto.Typecheck
UnequalHidingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unequalsAgda.Auto.Typecheck
UnequalSortsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTelescopesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTermsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalTypesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unescapeAgda.Compiler.JS.Pretty
unescapesAgda.Compiler.JS.Pretty
UnexpectedWithPatternsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unExprViewAgda.Syntax.Concrete.Operators.Parser
unflattenTelAgda.TypeChecking.Telescope
unfoldAgda.TypeChecking.MetaVars.Occurs
unfoldCorecursionAgda.TypeChecking.CompiledClause.Match
unfoldDefinitionAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
UnfoldStrategyAgda.TypeChecking.MetaVars.Occurs
unfreezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unGraphAgda.Utils.Graph
uniConstrAgda.TypeChecking.Rules.LHS.Unify
UnifiableAgda.TypeChecking.Rules.LHS.Unify
unifiableAgda.Compiler.Epic.Injection
UnificationResultAgda.TypeChecking.Rules.LHS.Unify
UnifiesAgda.TypeChecking.Rules.LHS.Unify
UnifyAgda.TypeChecking.Rules.LHS.Unify
unifyAgda.Compiler.Epic.Injection
UnifyEnvAgda.TypeChecking.Rules.LHS.Unify
UnifyExceptionAgda.TypeChecking.Rules.LHS.Unify
unifyexpAgda.Auto.CaseSplit
unifyIAgda.Compiler.Epic.Forcing
unifyIndicesAgda.TypeChecking.Rules.LHS.Unify
unifyIndices_Agda.TypeChecking.Rules.LHS.Unify
UnifyMayPostponeAgda.TypeChecking.Rules.LHS.Unify
UnifyOutputAgda.TypeChecking.Rules.LHS.Unify
UnifyStateAgda.TypeChecking.Rules.LHS.Unify
UninstantiatedDotPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UninstantiatedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
union 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Graph
3 (Function)Agda.Utils.Trie
4 (Function)Agda.Compiler.JS.Substitution
5 (Function)Agda.Termination.CallGraph
unionConstraintsAgda.Compiler.Epic.Injection
unions 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.Graph
unionSignaturesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
unionWithMAgda.Utils.Map
uniqByAgda.Utils.List
uniSubAgda.TypeChecking.Rules.LHS.Unify
UNITAgda.Compiler.Epic.AuxAST
univarAgda.Auto.SearchControl
UnknownAgda.TypeChecking.Positivity
unknownAgda.Termination.CallGraph
UnknownNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
UnknownNamesInFixityDeclAgda.Syntax.Concrete.Definitions
UnknownSortAgda.Auto.Syntax
unlessMAgda.Utils.Monad
unLevelAtomAgda.TypeChecking.Substitute
unlistenToMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unLvlAgda.TypeChecking.Primitive
unnamedAgda.Syntax.Common
unNatAgda.TypeChecking.Primitive
unNoTypeAgda.TypeChecking.Test.Generators
unqhnameAgda.Compiler.MAlonzo.Misc
unqnameAgda.Compiler.Epic.CompileState
unqualifyAgda.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
unquoteAgda.TypeChecking.Quote
unquoteFailedAgda.TypeChecking.Quote
unquoteFailedGenericAgda.TypeChecking.Quote
unquoteHAgda.TypeChecking.Quote
unquoteNAgda.TypeChecking.Quote
UnreachableClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnreducedLevelAgda.Syntax.Internal
unsafeCoerceModAgda.Compiler.MAlonzo.Misc
unsafePragmaOptionsAgda.Interaction.Options
unScopeAgda.TypeChecking.Rules.Term
unSizedListAgda.TypeChecking.Test.Generators
unSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
UnsolvedConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedConstraintsAgda.Interaction.Imports
UnsolvedMetaAgda.Interaction.Highlighting.Precise
UnsolvedMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedMetaVariablesAgda.Interaction.Imports
unStrAgda.TypeChecking.Primitive
unTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unUnifyAgda.TypeChecking.Rules.LHS.Unify
unusableRelevanceAgda.TypeChecking.Irrelevance
UnusedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unVarNameAgda.TypeChecking.Test.Generators
unYesTypeAgda.TypeChecking.Test.Generators
updateMetaAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
updateMetaVarAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateMetaVarRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updatePtrAgda.Utils.Pointer
ureadIORefAgda.Auto.NarrowingSearch
ureadmodifyIORefAgda.Auto.NarrowingSearch
UReduceAgda.TypeChecking.Rules.LHS.Unify
ureduceAgda.TypeChecking.Rules.LHS.Unify
usageAgda.Interaction.Options
usedSeedAgda.Utils.QuickCheck
usedSizeAgda.Utils.QuickCheck
useInjectivityAgda.TypeChecking.Injectivity
UselessAbstractAgda.Syntax.Concrete.Definitions
UselessPrivateAgda.Syntax.Concrete.Definitions
UseLitAgda.TypeChecking.Test.Generators
useLitCharAgda.TypeChecking.Test.Generators
UseLiteralsAgda.TypeChecking.Test.Generators
useLitFloatAgda.TypeChecking.Test.Generators
useLitIntAgda.TypeChecking.Test.Generators
useLitStringAgda.TypeChecking.Test.Generators
useNamesFromPatternAgda.TypeChecking.Rules.LHS
UsesAgda.Compiler.JS.Syntax
usesAgda.Compiler.JS.Syntax
UsingAgda.Syntax.Concrete
UsingOrHidingAgda.Syntax.Concrete
usingOrHidingAgda.Syntax.Concrete
UStAgda.TypeChecking.Rules.LHS.Unify
uwriteIORefAgda.Auto.NarrowingSearch