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 |