U | |
1 (Type/Class) | Agda.TypeChecking.Serialise.Base |
2 (Data Constructor) | Agda.TypeChecking.Serialise.Base |
uhcBackendEnabled | Agda.Compiler.UHC.Bridge |
UId | Agda.Auto.Syntax |
umodifyIORef | Agda.Auto.NarrowingSearch |
unAbs | Agda.Syntax.Internal |
unAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
unAppView | Agda.Syntax.Abstract.Views |
unArg | Agda.Syntax.Common |
UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
unblockedTester | Agda.TypeChecking.MetaVars |
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_ | |
1 (Function) | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
2 (Function) | Agda.TypeChecking.Reduce.Monad |
Underapplied | Agda.Syntax.Internal |
underConstructor | Agda.TypeChecking.Free.Lazy |
UnderInf | Agda.TypeChecking.Positivity |
UnderLambda | |
1 (Type/Class) | Agda.Compiler.Treeless.Subst |
2 (Data Constructor) | Agda.Compiler.Treeless.Subst |
underLambda | Agda.Compiler.Treeless.Subst |
underLambdas | Agda.TypeChecking.Substitute |
Underscore | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Syntax.Abstract |
underscore | Agda.Syntax.Common |
Undo | Agda.Auto.NarrowingSearch |
unDom | Agda.Syntax.Common |
unDrop | Agda.Utils.Permutation |
unEl | Agda.Syntax.Internal |
unequal | Agda.Auto.Typecheck |
UnequalBecauseOfUniverseConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
UnequalHiding | 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 |
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.Reduce |
unfoldCorecursionE | Agda.TypeChecking.Reduce |
unfoldDefinition | Agda.TypeChecking.Reduce |
unfoldDefinition' | Agda.TypeChecking.Reduce |
unfoldDefinitionE | Agda.TypeChecking.Reduce |
UnfoldStrategy | Agda.TypeChecking.MetaVars.Occurs |
UnFreezeMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
unfreezeMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
unfreezeMetas | Agda.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 |
unguardedRecord | Agda.TypeChecking.Records |
unguardedVars | |
1 (Function) | Agda.TypeChecking.Free.Old |
2 (Function) | Agda.TypeChecking.Free |
UnicodeTest | Agda.Utils.Char |
unicodeTests | Agda.Utils.Char |
unifiable | Agda.Compiler.Epic.Injection |
UnificationRecursiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
UnificationResult | Agda.TypeChecking.Rules.LHS.Unify |
UnificationResult' | Agda.TypeChecking.Rules.LHS.Unify |
UnificationStuck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Unifies | Agda.TypeChecking.Rules.LHS.Unify |
unify | Agda.Compiler.Epic.Injection |
UnifyConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
UnifyCycle | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
unifyexp | Agda.Auto.CaseSplit |
unifyI | Agda.Compiler.Epic.Forcing |
UnifyIndices | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
unifyIndices | Agda.TypeChecking.Rules.LHS.Unify |
UnifyIndicesNotVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
unifyIndices_ | Agda.TypeChecking.Rules.LHS.Unify |
unifyPointers | Agda.TypeChecking.Conversion |
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.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 |
unionCompared | Agda.Utils.Favorites |
unionConstraints | Agda.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 |
unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
unionsWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
unionWith | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
3 (Function) | Agda.Utils.Trie |
unionWithKey | Agda.Utils.HashMap |
unionWithM | Agda.Utils.Map |
uniqOn | Agda.Utils.List |
UNIT | Agda.Compiler.Epic.AuxAST |
unitCompose | Agda.TypeChecking.SizedTypes.Utils |
univar | Agda.Auto.SearchControl |
Unknown | |
1 (Data Constructor) | Agda.Syntax.Reflected |
2 (Data Constructor) | Agda.TypeChecking.Positivity |
unknown | Agda.Termination.Order |
UnknownName | Agda.Syntax.Scope.Monad |
UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions |
UnknownS | Agda.Syntax.Reflected |
UnknownSort | Agda.Auto.Syntax |
unlabelPatVars | Agda.Syntax.Internal.Pattern |
unless | Agda.Utils.Monad |
unlessM | Agda.Utils.Monad |
unlessNull | Agda.Utils.Null |
unlessNullM | Agda.Utils.Null |
unless_ | Agda.Utils.Monad |
unLevel | Agda.TypeChecking.Level |
unLevelAtom | Agda.TypeChecking.Substitute |
unlevelWithKit | Agda.TypeChecking.Level |
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 |
unnumberPatVars | Agda.Syntax.Internal.Pattern |
unpackUnquoteM | Agda.TypeChecking.Unquote |
unPlusV | Agda.TypeChecking.Level |
unProjName | Agda.TypeChecking.Test.Generators |
unProjView | Agda.TypeChecking.ProjectionLike |
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.Unquote |
unquote | Agda.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 |
UnquoteDefRequiresSignature | Agda.Syntax.Concrete.Definitions |
UnquoteError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
UnquoteFailed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
unquoteH | Agda.TypeChecking.Unquote |
UnquoteM | Agda.TypeChecking.Unquote |
unquoteM | Agda.TypeChecking.Rules.Term |
unquoteN | Agda.TypeChecking.Unquote |
unquoteNString | Agda.TypeChecking.Unquote |
UnquotePanic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
UnquoteRes | Agda.TypeChecking.Unquote |
UnquoteState | Agda.TypeChecking.Unquote |
unquoteString | Agda.TypeChecking.Unquote |
UnquoteTactic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
unquoteTactic | Agda.TypeChecking.Rules.Term |
unquoteTCM | Agda.TypeChecking.Unquote |
unquoteTop | Agda.TypeChecking.Rules.Decl |
unranged | Agda.Syntax.Common |
Unreachable | Agda.Syntax.Treeless |
UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
UnreducedLevel | Agda.Syntax.Internal |
unReduceM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Unrelated | Agda.Syntax.Fixity |
unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc |
unsafePragmaOptions | Agda.Interaction.Options |
unScope | Agda.Syntax.Abstract.Views |
unserialize | Agda.Compiler.UHC.Bridge |
unSizedList | Agda.TypeChecking.Test.Generators |
unSizeExpr | Agda.TypeChecking.SizedTypes.Solve |
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 |
unSpine | Agda.Syntax.Internal |
unStr | Agda.Utils.String |
unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
unusableRelevance | Agda.Syntax.Common |
Unused | |
1 (Data Constructor) | Agda.TypeChecking.Positivity.Occurrence |
2 (Data Constructor) | Agda.TypeChecking.Free.Old |
3 (Data Constructor) | Agda.TypeChecking.Free |
UnusedArg | Agda.Syntax.Common |
unusedVar | Agda.Termination.Monad |
UnusedVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
unusedVars | |
1 (Function) | Agda.TypeChecking.Free.Old |
2 (Function) | Agda.TypeChecking.Free |
unVarName | Agda.TypeChecking.Test.Generators |
unwrap | Agda.Compiler.MAlonzo.Pretty |
unYesType | Agda.TypeChecking.Test.Generators |
unzip | |
1 (Function) | Agda.Utils.Map |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
unzip3 | Agda.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 |
update1 | Agda.Utils.Update |
update2 | Agda.Utils.Update |
updateAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
updateAt | |
1 (Function) | Agda.Utils.List |
2 (Function) | Agda.Utils.AssocList |
updateBenchmark | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
updateBenchmarkingStatus | Agda.TypeChecking.Monad.Benchmark |
updateDefArgOccurrences | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
updateDefCompiledRep | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
updateDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
updateDefinitions | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
updateDefPolarity | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
updateDefType | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
updateFunClauses | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
updateHead | Agda.Utils.List |
updateInPatterns | Agda.TypeChecking.Rules.LHS |
updateInstanceDefs | Agda.TypeChecking.Monad.State, 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 |
updatePersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
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 |
Updater | Agda.Utils.Update |
Updater1 | Agda.Utils.Update |
updater1 | Agda.Utils.Update |
Updater2 | Agda.Utils.Update |
updater2 | Agda.Utils.Update |
updates1 | Agda.Utils.Update |
updates2 | Agda.Utils.Update |
updateScopeLocals | Agda.Syntax.Scope.Base |
updateScopeNameSpaces | Agda.Syntax.Scope.Base |
updateScopeNameSpacesM | Agda.Syntax.Scope.Base |
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.State, Agda.TypeChecking.Monad |
upperBounds | Agda.TypeChecking.SizedTypes.WarshallSolver |
ureadIORef | Agda.Auto.NarrowingSearch |
ureadmodifyIORef | Agda.Auto.NarrowingSearch |
UsableSizeVars | Agda.Termination.Monad |
usableSizeVars | Agda.Termination.Monad |
usage | Agda.Interaction.Options |
use | Agda.Utils.Lens |
usedArguments | Agda.Compiler.Treeless.Unused |
useDefaultFixity | Agda.Syntax.Fixity |
usedSeed | Agda.Utils.QuickCheck |
usedSize | Agda.Utils.QuickCheck |
UseEverything | Agda.Syntax.Common |
useInjectivity | Agda.TypeChecking.Injectivity |
UselessAbstract | Agda.Syntax.Concrete.Definitions |
UselessInstance | 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 |
usesCopatterns | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
useTerPragma | Agda.TypeChecking.Rules.Def |
Using | |
1 (Data Constructor) | Agda.Syntax.Common |
2 (Type/Class) | Agda.Syntax.Concrete |
using | Agda.Syntax.Common |
Using' | Agda.Syntax.Common |
UsingOrHiding | Agda.Syntax.Scope.Base |
usingOrHiding | Agda.Syntax.Scope.Base |
uwriteIORef | Agda.Auto.NarrowingSearch |