UE | Agda.TypeChecking.Coverage.SplitClause |
uglyShowName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
UId | Agda.Auto.Syntax |
ULarge | Agda.Syntax.Internal |
umodifyIORef | Agda.Auto.NarrowingSearch |
unAbs | Agda.Syntax.Internal |
unAbsN | Agda.TypeChecking.Names |
unambiguous | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
unAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
unAppView | |
1 (Function) | Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract.Views |
unArg | Agda.Syntax.Common |
unBind | Agda.Syntax.Abstract |
unbindVariable | Agda.Syntax.Scope.Monad |
UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unblockDef | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockedTester | Agda.TypeChecking.MetaVars |
unblockMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
UnblockOnAll | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnAll | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnAllMetas | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnAllMetasIn | Agda.Syntax.Internal.MetaVars |
UnblockOnAny | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnAny | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnAnyMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnAnyMetaIn | Agda.Syntax.Internal.MetaVars |
unblockOnBoth | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
UnblockOnDef | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnDef | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnEither | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
UnblockOnMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnMeta | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
UnblockOnProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockOnProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unblockProblem | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
unBlockT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnboundVariablesInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unBrave | Agda.Syntax.Internal |
unBruijn | Agda.TypeChecking.CompiledClause.Compile |
unBuiltinAccess | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnconfirmedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
uncons | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.Utils.List |
unConstV | Agda.TypeChecking.Level |
uncurry3 | Agda.Utils.Tuple |
uncurry4 | Agda.Utils.Tuple |
uncurrys | Agda.Utils.TypeLevel |
unDeepSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Undefined | Agda.Compiler.JS.Syntax |
underAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
underAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
underAbstraction' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
underAbstractionAbs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
underAbstractionAbs' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
underAbstraction_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnderAddition | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
Underapplied | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
underBinder | Agda.TypeChecking.Free.Lazy |
underBinder' | Agda.TypeChecking.Free.Lazy |
UnderComposition | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
underConstructor | Agda.TypeChecking.Free.Lazy |
underFlexRig | Agda.TypeChecking.Free.Lazy |
UnderInf | Agda.TypeChecking.Positivity.Occurrence |
UnderLambda | |
1 (Type/Class) | Agda.Compiler.Treeless.Subst |
2 (Data Constructor) | Agda.Compiler.Treeless.Subst |
underLambda | Agda.Compiler.Treeless.Subst |
underLambdas | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
underlyingRange | Agda.TypeChecking.Serialise.Instances.Common |
underModality | Agda.TypeChecking.Free.Lazy |
underOpaqueId | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
underQuantity | Agda.TypeChecking.Free.Lazy |
underRelevance | Agda.TypeChecking.Free.Lazy |
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.Internal |
unDrop | Agda.Utils.Permutation |
unEl | Agda.Syntax.Internal |
unequal | Agda.Auto.Typecheck |
UnequalBecauseOfUniverseConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnequalCohesion | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnequalFiniteness | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnequalLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnequalQuantity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnequalRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unequals | Agda.Auto.Typecheck |
UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnequalTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unescape | Agda.Compiler.JS.Pretty |
unescapes | Agda.Compiler.JS.Pretty |
UnexpectedModalityAnnotationInParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnexpectedParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnexpectedTypeSignatureForParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unExprView | Agda.Syntax.Concrete.Operators.Parser |
unflattenTel | Agda.TypeChecking.Telescope |
unflattenTel' | Agda.TypeChecking.Telescope |
unfold | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.TypeChecking.MetaVars.Occurs |
unfoldB | Agda.TypeChecking.MetaVars.Occurs |
unfoldCorecursion | Agda.TypeChecking.Reduce |
unfoldCorecursionE | Agda.TypeChecking.Reduce |
unfoldDefinitionE | Agda.TypeChecking.Reduce |
unfoldDefinitionStep | Agda.TypeChecking.Reduce |
Unfolding | Agda.Syntax.Concrete |
UnfoldingDecl | Agda.Syntax.Abstract |
UnfoldingDeclS | Agda.Syntax.Abstract |
UnfoldingOutsideOpaque | Agda.Syntax.Concrete.Definitions.Errors |
unfoldInlined | Agda.TypeChecking.Reduce |
unfoldr | Agda.Utils.List1 |
UnfoldStrategy | Agda.TypeChecking.MetaVars.Occurs |
UnfoldTransparentName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnfoldTransparentName_ | Agda.Interaction.Options.Warnings |
UnFreezeMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unfreezeMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unfreezeMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Unguarded | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
unguardedRecord | Agda.TypeChecking.Records |
UnGuardedRhs | Agda.Utils.Haskell.Syntax |
unguardedVars | Agda.TypeChecking.Free |
UnicodeOk | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options |
UnicodeOrAscii | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options |
UnicodeSubscript | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
UnificationFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnificationResult | Agda.TypeChecking.Rules.LHS.Unify |
UnificationResult' | Agda.TypeChecking.Rules.LHS.Unify |
UnificationStep | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnificationStuck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Unifies | Agda.TypeChecking.Rules.LHS.Unify |
UnifiesTo | Agda.Auto.CaseSplit |
Unify | Agda.Auto.CaseSplit |
unify | Agda.Auto.CaseSplit |
unify' | Agda.Auto.CaseSplit |
UnifyBlocked | Agda.TypeChecking.Rules.LHS.Unify |
UnifyConflict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnifyCycle | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unifyElims | Agda.TypeChecking.IApplyConfluence |
unifyElimsMeta | Agda.TypeChecking.IApplyConfluence |
UnifyEquiv | Agda.TypeChecking.Coverage.SplitClause |
unifyexp | Agda.Auto.CaseSplit |
UnifyIndices | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
unifyIndices | Agda.TypeChecking.Rules.LHS.Unify |
unifyIndices' | Agda.TypeChecking.Rules.LHS.Unify |
UnifyIndicesNotVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnifyLog | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyLog' | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyLogEntry | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyLogT | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyOutput | |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Unify.Types |
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify.Types |
unifyProof | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyRecursiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnifyReflexiveEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnifyState | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyStep | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyStepT | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyStuck | Agda.TypeChecking.Rules.LHS.Unify |
unifySubst | Agda.TypeChecking.Rules.LHS.Unify.Types |
UnifyUnusableModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unifyVar | Agda.Auto.CaseSplit |
UninstantiatedDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
union | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.BoolSet |
3 (Function) | Agda.Utils.Bag |
4 (Function) | Agda.Utils.SmallSet |
5 (Function) | Agda.Utils.Trie |
6 (Function) | Agda.Utils.List1 |
7 (Function) | Agda.Utils.BiMap |
8 (Function) | Agda.Utils.Favorites |
9 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
10 (Function) | Agda.Termination.CallMatrix |
11 (Function) | Agda.Termination.CallGraph |
12 (Function) | Agda.Compiler.JS.Substitution |
unionBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unionCompared | Agda.Utils.Favorites |
unionMaybeWith | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
unionPrecondition | Agda.Utils.BiMap |
unions | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.Bag |
3 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unionsMaybeWith | Agda.Utils.Maybe |
unionsWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
unionWith | |
1 (Function) | Agda.Utils.Trie |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
uniqOn | Agda.Utils.List |
uniqueInt | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
UniqueOpaque | Agda.Syntax.Common |
unitCohesion | Agda.Syntax.Common |
unitCompose | Agda.TypeChecking.SizedTypes.Utils |
unitModality | Agda.Syntax.Common |
unitQuantity | Agda.Syntax.Common |
unitRelevance | Agda.Syntax.Common |
unit_con | Agda.Utils.Haskell.Syntax |
Univ | |
1 (Type/Class) | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
univar | Agda.Auto.SearchControl |
univChecks | Agda.TypeChecking.Rules.Application |
UniverseCheck | Agda.Syntax.Common |
universeCheck | Agda.Syntax.Concrete.Definitions.Types |
universeCheckPragma | Agda.Syntax.Concrete.Definitions.Monad |
univFibrancy | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
UnivSize | Agda.Syntax.Internal |
UnivSort | Agda.Syntax.Internal |
univSort | Agda.TypeChecking.Substitute |
univSort' | Agda.TypeChecking.Substitute |
univUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
UnkindedVar | Agda.Utils.Haskell.Syntax |
Unknown | |
1 (Data Constructor) | Agda.Interaction.Options.Warnings |
2 (Data Constructor) | Agda.Termination.Order |
3 (Data Constructor) | Agda.Syntax.Reflected |
unknown | Agda.Termination.Order |
UnknownError | Agda.Interaction.ExitCode |
UnknownField | Agda.Interaction.Library.Base |
UnknownFixityInMixfixDecl | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
UnknownFixityInMixfixDecl_ | Agda.Interaction.Options.Warnings |
unknownFreeVariables | Agda.Syntax.Common |
UnknownFVs | Agda.Syntax.Common |
UnknownHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnknownName | Agda.Syntax.Scope.Base |
UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
UnknownNamesInFixityDecl_ | Agda.Interaction.Options.Warnings |
UnknownNamesInPolarityPragmas | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
UnknownNamesInPolarityPragmas_ | Agda.Interaction.Options.Warnings |
UnknownS | Agda.Syntax.Reflected |
UnknownSort | Agda.Auto.Syntax |
unlabelPatVars | Agda.Syntax.Internal.Pattern |
unlamView | Agda.TypeChecking.Substitute |
unless | Agda.Utils.Monad |
unlessDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unlessM | Agda.Utils.Monad |
unlessNull | |
1 (Function) | Agda.Utils.Null |
2 (Function) | Agda.Utils.List1 |
unlessNullM | Agda.Utils.Null |
unLevel | Agda.TypeChecking.Level |
unlevelWithKit | Agda.TypeChecking.Level |
unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unLvl | Agda.TypeChecking.Primitive |
unM | Agda.Termination.SparseMatrix |
unmapListT | Agda.Utils.ListT |
unMaxView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unName | Agda.TypeChecking.Names |
unnamed | Agda.Syntax.Common |
unnamedArg | Agda.Syntax.Common |
unNat | Agda.TypeChecking.Primitive |
unNice | Agda.Syntax.Concrete.Definitions.Monad |
unNLM | Agda.TypeChecking.Rewriting.NonLinMatch |
unnumberPatVars | Agda.Syntax.Internal.Pattern |
unpackUnquoteM | Agda.TypeChecking.Unquote |
unPiView | Agda.Syntax.Abstract.Views |
unPlusV | Agda.TypeChecking.Level |
unPM | Agda.Syntax.Parser |
unProjView | Agda.TypeChecking.ProjectionLike |
unPureConversionT | Agda.TypeChecking.Conversion.Pure |
unqhname | Agda.Compiler.MAlonzo.Misc |
UnQual | Agda.Utils.Haskell.Syntax |
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 |
UnquoteData | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
UnquoteDataS | Agda.Syntax.Abstract |
UnquoteDecl | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
UnquoteDeclS | Agda.Syntax.Abstract |
UnquoteDef | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
UnquoteDefRequiresSignature | Agda.Syntax.Concrete.Definitions.Errors |
UnquoteDefS | Agda.Syntax.Abstract |
UnquoteError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnquoteFailed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnquoteFlags | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnquoteM | Agda.TypeChecking.Unquote |
unquoteM | Agda.TypeChecking.Rules.Term |
unquoteN | Agda.TypeChecking.Unquote |
unquoteNormalise | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unquoteNString | Agda.TypeChecking.Unquote |
UnquotePanic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnquoteRes | Agda.TypeChecking.Unquote |
UnquoteState | Agda.TypeChecking.Unquote |
unquoteString | Agda.TypeChecking.Unquote |
UnquoteTactic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unquoteTactic | Agda.TypeChecking.Rules.Term |
unquoteTCM | Agda.TypeChecking.Unquote |
unquoteTop | Agda.TypeChecking.Rules.Decl |
unranged | Agda.Syntax.Common |
Unreachable | |
1 (Data Constructor) | Agda.Utils.Impossible |
2 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnreachableClauses_ | Agda.Interaction.Options.Warnings |
unReduceM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Unrelated | Agda.Syntax.Common |
unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc |
unsafeDeclarationWarning | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
unsafeDeclarationWarning' | Agda.Syntax.Concrete.Definitions.Errors |
unsafeEscapeContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unsafeInTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unsafeModifyContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unsafePragma | Agda.Syntax.Concrete.Definitions.Errors |
unsafePragmaOptions | Agda.Interaction.Options |
unsafeSetUnicodeOrAscii | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
unsafeTopLevelModuleName | Agda.Syntax.TopLevelModuleName |
unScope | Agda.Syntax.Abstract.Views |
unSingleLevel | Agda.TypeChecking.Level |
unSingleLevels | Agda.TypeChecking.Level |
unSizeExpr | Agda.TypeChecking.SizedTypes.Solve |
unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnsolvedConstraint | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnsolvedConstraints_ | Agda.Interaction.Options.Warnings |
UnsolvedInteractionMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnsolvedInteractionMetas_ | Agda.Interaction.Options.Warnings |
UnsolvedMeta | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
UnsolvedMetaVariables | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnsolvedMetaVariables_ | Agda.Interaction.Options.Warnings |
unsolvedWarnings | Agda.Interaction.Options.Warnings |
unSpine | Agda.Syntax.Internal |
unSpine' | Agda.Syntax.Internal |
UnsupportedAttribute | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
UnsupportedAttribute_ | Agda.Interaction.Options.Warnings |
UnsupportedCxt | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify |
UnsupportedIndexedMatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UnsupportedIndexedMatch_ | Agda.Interaction.Options.Warnings |
UnsupportedYet | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify |
UntaggedValue | Agda.Interaction.JSON |
unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Unused | Agda.TypeChecking.Positivity.Occurrence |
unusedVar | Agda.Termination.Monad |
UnusedVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unVersionView | Agda.Interaction.Library |
unviewProjectedVar | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
unwords | Agda.Utils.List1 |
unwords1 | Agda.Utils.String |
unwrapUnaryRecords | Agda.Interaction.JSON |
unzip | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
unzipMaybe | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
unzipWith | Agda.Utils.List |
update | |
1 (Function) | Agda.Utils.BiMap |
2 (Function) | Agda.Utils.AssocList |
update1 | Agda.Utils.Update |
update2 | Agda.Utils.Update |
updateAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateAt | |
1 (Function) | Agda.Utils.List |
2 (Function) | Agda.Utils.AssocList |
updateBenchmark | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateBenchmarkingStatus | Agda.TypeChecking.Monad.Benchmark |
updateBlocker | Agda.TypeChecking.Constraints |
updateCompiledClauses | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateCovering | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateDefArgOccurrences | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateDefBlocked | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateDefCompiledRep | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateDefCopatternLHS | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateDefinitions | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateDefPolarity | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateDefType | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateEtaForRecord | Agda.TypeChecking.Records |
updateFunClauses | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateHead | |
1 (Function) | Agda.Utils.List |
2 (Function) | Agda.Utils.List1 |
updateHeads | Agda.TypeChecking.Injectivity |
updateInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateInteractionPointsAfter | Agda.Interaction.InteractionTop |
updateLast | |
1 (Function) | Agda.Utils.List |
2 (Function) | Agda.Utils.List1 |
updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateMetaVarTCM | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateNamedArg | Agda.Syntax.Common |
updateNamedArgA | Agda.Syntax.Common |
updatePersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updatePrecondition | Agda.Utils.BiMap |
updateProblemRest | Agda.TypeChecking.Rules.LHS.ProblemRest |
updatePtr | Agda.Utils.Pointer |
updatePtrM | Agda.Utils.Pointer |
Updater | Agda.Utils.Update |
Updater1 | Agda.Utils.Update |
updater1 | Agda.Utils.Update |
Updater2 | Agda.Utils.Update |
updater2 | Agda.Utils.Update |
UpdaterT | 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 |
updateTheDef | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
updateVarsToBind | Agda.Syntax.Scope.Base |
upperBounds | Agda.TypeChecking.SizedTypes.WarshallSolver |
UProp | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
ureadIORef | Agda.Auto.NarrowingSearch |
ureadmodifyIORef | Agda.Auto.NarrowingSearch |
UsableAtMod | Agda.Interaction.Base |
UsableAtModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
usableAtModality | Agda.TypeChecking.Irrelevance |
usableAtModality' | Agda.TypeChecking.Irrelevance |
usableCohesion | Agda.Syntax.Common |
usableMod | Agda.TypeChecking.Irrelevance |
usableModAbs | Agda.TypeChecking.Irrelevance |
UsableModality | Agda.TypeChecking.Irrelevance |
usableModality | Agda.Syntax.Common |
usableQuantity | Agda.Syntax.Common |
usableRel | Agda.TypeChecking.Irrelevance |
UsableRelevance | Agda.TypeChecking.Irrelevance |
usableRelevance | Agda.Syntax.Common |
UsableSizeVars | Agda.Termination.Monad |
usableSizeVars | Agda.Termination.Monad |
usage | Agda.Interaction.Options |
usageWarning | Agda.Interaction.Options.Warnings |
use | Agda.Utils.Lens |
useConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
usedArguments | Agda.Compiler.Treeless.Unused |
useDefaultFixity | Agda.Syntax.Notation |
UseEverything | Agda.Syntax.Common |
UseForce | Agda.Interaction.Base |
useInjectivity | Agda.TypeChecking.Injectivity |
UselessAbstract | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
UselessAbstract_ | Agda.Interaction.Options.Warnings |
UselessHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UselessHiding_ | Agda.Interaction.Options.Warnings |
UselessInline | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UselessInline_ | Agda.Interaction.Options.Warnings |
UselessInstance | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
UselessInstance_ | Agda.Interaction.Options.Warnings |
UselessOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UselessOpaque_ | Agda.Interaction.Options.Warnings |
UselessPatternDeclarationForRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UselessPatternDeclarationForRecord_ | Agda.Interaction.Options.Warnings |
UselessPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UselessPragma_ | Agda.Interaction.Options.Warnings |
UselessPrivate | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
UselessPrivate_ | Agda.Interaction.Options.Warnings |
UselessPublic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UselessPublic_ | Agda.Interaction.Options.Warnings |
useNamesFromPattern | Agda.TypeChecking.Rules.LHS.ProblemRest |
useNamesFromProblemEqs | Agda.TypeChecking.Rules.LHS.ProblemRest |
useOriginFrom | Agda.TypeChecking.Rules.LHS.ProblemRest |
usePatOrigin | Agda.TypeChecking.Substitute |
usePatternInfo | Agda.TypeChecking.Substitute |
useR | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
userNamed | Agda.Syntax.Common |
UserWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UserWarning_ | Agda.Interaction.Options.Warnings |
UserWritten | Agda.Syntax.Common |
Uses | Agda.Compiler.JS.Syntax |
uses | Agda.Compiler.JS.Syntax |
usesCopatterns | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
useScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
UseShowInstance | Agda.Interaction.Base |
useTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
UsingOnly | Agda.Syntax.Scope.Base |
UsingOrHiding | Agda.Syntax.Scope.Base |
usingOrHiding | Agda.Syntax.Scope.Base |
USmall | Agda.Syntax.Internal |
USSet | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
UState | Agda.TypeChecking.Rules.LHS.Unify.Types |
usualWarnings | Agda.Interaction.Options.Warnings |
UType | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
uwriteIORef | Agda.Auto.NarrowingSearch |