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

Index - U

U 
1 (Type/Class)Agda.TypeChecking.Serialise.Base
2 (Data Constructor)Agda.TypeChecking.Serialise.Base
uhcBackendEnabledAgda.Compiler.UHC.Bridge
UIdAgda.Auto.Syntax
umodifyIORefAgda.Auto.NarrowingSearch
unAbsAgda.Syntax.Internal
unAmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
unAppViewAgda.Syntax.Abstract.Views
unArgAgda.Syntax.Common
UnBlockAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unblockedTesterAgda.TypeChecking.MetaVars
unConNameAgda.TypeChecking.Test.Generators
unconsAgda.Utils.List
uncurry3Agda.Utils.Tuple
uncurry4Agda.Utils.Tuple
unDeepSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
undefAgda.Compiler.JS.Parser
UndefinedAgda.Compiler.JS.Syntax
unDefNameAgda.TypeChecking.Test.Generators
underAbsAgda.TypeChecking.Substitute
underAbstractionAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
underAbstraction_ 
1 (Function)Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
2 (Function)Agda.TypeChecking.Reduce.Monad
UnderappliedAgda.Syntax.Internal
underConstructorAgda.TypeChecking.Free.Lazy
UnderInfAgda.TypeChecking.Positivity
UnderLambda 
1 (Type/Class)Agda.Compiler.Treeless.Subst
2 (Data Constructor)Agda.Compiler.Treeless.Subst
underLambdaAgda.Compiler.Treeless.Subst
underLambdasAgda.TypeChecking.Substitute
Underscore 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
underscoreAgda.Syntax.Common
UndoAgda.Auto.NarrowingSearch
unDomAgda.Syntax.Common
unDropAgda.Utils.Permutation
unElAgda.Syntax.Internal
unequalAgda.Auto.Typecheck
UnequalBecauseOfUniverseConflictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalHidingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnequalRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unequalsAgda.Auto.Typecheck
UnequalSortsAgda.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.Reduce
unfoldCorecursionEAgda.TypeChecking.Reduce
unfoldDefinitionAgda.TypeChecking.Reduce
unfoldDefinition'Agda.TypeChecking.Reduce
unfoldDefinitionEAgda.TypeChecking.Reduce
UnfoldStrategyAgda.TypeChecking.MetaVars.Occurs
UnFreezeMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unfreezeMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unfreezeMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unfreezeMetas'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
Unguarded 
1 (Data Constructor)Agda.TypeChecking.Free.Lazy
2 (Data Constructor)Agda.TypeChecking.Free.Old
3 (Data Constructor)Agda.TypeChecking.Free
unguardedRecordAgda.TypeChecking.Records
unguardedVars 
1 (Function)Agda.TypeChecking.Free.Old
2 (Function)Agda.TypeChecking.Free
UnicodeTestAgda.Utils.Char
unicodeTestsAgda.Utils.Char
unifiableAgda.Compiler.Epic.Injection
UnificationRecursiveEqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnificationResultAgda.TypeChecking.Rules.LHS.Unify
UnificationResult'Agda.TypeChecking.Rules.LHS.Unify
UnificationStuckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnifiesAgda.TypeChecking.Rules.LHS.Unify
unifyAgda.Compiler.Epic.Injection
UnifyConflictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnifyCycleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unifyexpAgda.Auto.CaseSplit
unifyIAgda.Compiler.Epic.Forcing
UnifyIndicesAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
unifyIndicesAgda.TypeChecking.Rules.LHS.Unify
UnifyIndicesNotVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unifyIndices_Agda.TypeChecking.Rules.LHS.Unify
unifyPointersAgda.TypeChecking.Conversion
UninstantiatedDotPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UninstantiatedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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.Favorites
6 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
7 (Function)Agda.Utils.Trie
8 (Function)Agda.Termination.CallMatrix
9 (Function)Agda.Termination.CallGraph
10 (Function)Agda.Compiler.JS.Substitution
unionComparedAgda.Utils.Favorites
unionConstraintsAgda.Compiler.Epic.Injection
unionMaybeWith 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
unions 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.HashMap
3 (Function)Agda.Utils.Bag
4 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
unionSignaturesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
unionsWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
unionWith 
1 (Function)Agda.Utils.HashMap
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Function)Agda.Utils.Trie
unionWithKeyAgda.Utils.HashMap
unionWithMAgda.Utils.Map
uniqOnAgda.Utils.List
UNITAgda.Compiler.Epic.AuxAST
unitComposeAgda.TypeChecking.SizedTypes.Utils
univarAgda.Auto.SearchControl
Unknown 
1 (Data Constructor)Agda.Syntax.Reflected
2 (Data Constructor)Agda.TypeChecking.Positivity
unknownAgda.Termination.Order
UnknownNameAgda.Syntax.Scope.Monad
UnknownNamesInFixityDeclAgda.Syntax.Concrete.Definitions
UnknownSAgda.Syntax.Reflected
UnknownSortAgda.Auto.Syntax
unlabelPatVarsAgda.Syntax.Internal.Pattern
unlessAgda.Utils.Monad
unlessMAgda.Utils.Monad
unlessNullAgda.Utils.Null
unlessNullMAgda.Utils.Null
unless_Agda.Utils.Monad
unLevelAgda.TypeChecking.Level
unLevelAtomAgda.TypeChecking.Substitute
unlevelWithKitAgda.TypeChecking.Level
unlistenToMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
unLvlAgda.TypeChecking.Primitive
unMaxViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
unnamedAgda.Syntax.Common
unNatAgda.TypeChecking.Primitive
unNoTypeAgda.TypeChecking.Test.Generators
unnumberPatVarsAgda.Syntax.Internal.Pattern
unpackUnquoteMAgda.TypeChecking.Unquote
unPlusVAgda.TypeChecking.Level
unProjNameAgda.TypeChecking.Test.Generators
unProjViewAgda.TypeChecking.ProjectionLike
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.Unquote
unquoteAgda.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
UnquoteDefRequiresSignatureAgda.Syntax.Concrete.Definitions
UnquoteErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnquoteFailedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unquoteHAgda.TypeChecking.Unquote
UnquoteMAgda.TypeChecking.Unquote
unquoteMAgda.TypeChecking.Rules.Term
unquoteNAgda.TypeChecking.Unquote
unquoteNStringAgda.TypeChecking.Unquote
UnquotePanicAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnquoteResAgda.TypeChecking.Unquote
UnquoteStateAgda.TypeChecking.Unquote
unquoteStringAgda.TypeChecking.Unquote
UnquoteTacticAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unquoteTacticAgda.TypeChecking.Rules.Term
unquoteTCMAgda.TypeChecking.Unquote
unquoteTopAgda.TypeChecking.Rules.Decl
unrangedAgda.Syntax.Common
UnreachableAgda.Syntax.Treeless
UnreachableClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnreducedLevelAgda.Syntax.Internal
unReduceMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
UnrelatedAgda.Syntax.Fixity
unsafeCoerceModAgda.Compiler.MAlonzo.Misc
unsafePragmaOptionsAgda.Interaction.Options
unScopeAgda.Syntax.Abstract.Views
unserializeAgda.Compiler.UHC.Bridge
unSizedListAgda.TypeChecking.Test.Generators
unSizeExprAgda.TypeChecking.SizedTypes.Solve
unSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
UnsolvedConstraintAgda.Interaction.Highlighting.Precise
UnsolvedConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedConstraintsAgda.TypeChecking.Errors
UnsolvedMetaAgda.Interaction.Highlighting.Precise
UnsolvedMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unsolvedMetaVariablesAgda.TypeChecking.Errors
unSpineAgda.Syntax.Internal
unStrAgda.Utils.String
unTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unusableRelevanceAgda.Syntax.Common
Unused 
1 (Data Constructor)Agda.TypeChecking.Positivity.Occurrence
2 (Data Constructor)Agda.TypeChecking.Free.Old
3 (Data Constructor)Agda.TypeChecking.Free
UnusedArgAgda.Syntax.Common
unusedVarAgda.Termination.Monad
UnusedVariableInPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
unusedVars 
1 (Function)Agda.TypeChecking.Free.Old
2 (Function)Agda.TypeChecking.Free
unVarNameAgda.TypeChecking.Test.Generators
unwrapAgda.Compiler.MAlonzo.Pretty
unYesTypeAgda.TypeChecking.Test.Generators
unzip 
1 (Function)Agda.Utils.Map
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
unzip3Agda.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
update1Agda.Utils.Update
update2Agda.Utils.Update
updateAllowedReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
updateAt 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.AssocList
updateBenchmarkAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateBenchmarkingStatusAgda.TypeChecking.Monad.Benchmark
updateDefArgOccurrencesAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefCompiledRepAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefinitionAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefinitionsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefPolarityAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateDefTypeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateFunClausesAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateHeadAgda.Utils.List
updateInPatternsAgda.TypeChecking.Rules.LHS
updateInstanceDefsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateLastAgda.Utils.List
updateMetaAgda.TypeChecking.MetaVars
updateMetaVarAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateMetaVarRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
updateNamedArgAgda.Syntax.Common
updatePersistentStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
updateProblemRestAgda.TypeChecking.Rules.LHS.ProblemRest
updateProblemRest_Agda.TypeChecking.Rules.LHS.ProblemRest
updatePtrAgda.Utils.Pointer, Agda.Syntax.Internal
updatePtrMAgda.Utils.Pointer, Agda.Syntax.Internal
UpdaterAgda.Utils.Update
Updater1Agda.Utils.Update
updater1Agda.Utils.Update
Updater2Agda.Utils.Update
updater2Agda.Utils.Update
updates1Agda.Utils.Update
updates2Agda.Utils.Update
updateScopeLocalsAgda.Syntax.Scope.Base
updateScopeNameSpacesAgda.Syntax.Scope.Base
updateScopeNameSpacesMAgda.Syntax.Scope.Base
updateSharedAgda.Syntax.Internal
updateSharedFMAgda.Syntax.Internal
updateSharedMAgda.Syntax.Internal
updateSharedTermAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateSharedTermFAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateSharedTermTAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
updateTheDefAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
upperBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
ureadIORefAgda.Auto.NarrowingSearch
ureadmodifyIORefAgda.Auto.NarrowingSearch
UsableSizeVarsAgda.Termination.Monad
usableSizeVarsAgda.Termination.Monad
usageAgda.Interaction.Options
useAgda.Utils.Lens
usedArgumentsAgda.Compiler.Treeless.Unused
useDefaultFixityAgda.Syntax.Fixity
usedSeedAgda.Utils.QuickCheck
usedSizeAgda.Utils.QuickCheck
UseEverythingAgda.Syntax.Common
useInjectivityAgda.TypeChecking.Injectivity
UselessAbstractAgda.Syntax.Concrete.Definitions
UselessInstanceAgda.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.ProblemRest
UsesAgda.Compiler.JS.Syntax
usesAgda.Compiler.JS.Syntax
usesCopatternsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
useTerPragmaAgda.TypeChecking.Rules.Def
Using 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Syntax.Concrete
usingAgda.Syntax.Common
Using'Agda.Syntax.Common
UsingOrHidingAgda.Syntax.Scope.Base
usingOrHidingAgda.Syntax.Scope.Base
uwriteIORefAgda.Auto.NarrowingSearch