| A | |
| 1 (Data Constructor) | Agda.Interaction.EmacsCommand |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Misc |
| aArity | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| aBody | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| abort | |
| 1 (Function) | Agda.Interaction.Base |
| 2 (Function) | Agda.TypeChecking.MetaVars.Occurs |
| abortIfBlocked | Agda.TypeChecking.Reduce |
| Above | Agda.Compiler.JS.Pretty |
| above | Agda.Utils.IntSet.Infinite |
| Abs | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| 3 (Type/Class) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Type/Class) | Agda.Syntax.Reflected |
| 6 (Data Constructor) | Agda.Syntax.Reflected |
| absApp | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| absAppN | Agda.TypeChecking.Names |
| absBody | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| abslamvarname | Agda.Auto.Convert |
| AbsModule | Agda.Syntax.Scope.Base |
| AbsN | |
| 1 (Type/Class) | Agda.TypeChecking.Names |
| 2 (Data Constructor) | Agda.TypeChecking.Names |
| AbsName | Agda.Syntax.Scope.Base |
| absName | Agda.Syntax.Internal |
| AbsNameWithFixity | |
| 1 (Type/Class) | Agda.TypeChecking.Serialise.Instances.Abstract |
| 2 (Data Constructor) | Agda.TypeChecking.Serialise.Instances.Abstract |
| absNName | Agda.TypeChecking.Names |
| AbsOfCon | Agda.Syntax.Translation.ConcreteToAbstract |
| AbsOfRef | Agda.Syntax.Translation.ReflectedToAbstract |
| absolute | Agda.Utils.FileName |
| AbsolutePath | |
| 1 (Type/Class) | Agda.Utils.FileName |
| 2 (Data Constructor) | Agda.Utils.FileName |
| abspatvarname | Agda.Auto.CaseSplit |
| AbsTerm | Agda.TypeChecking.Abstract |
| absTerm | Agda.TypeChecking.Abstract |
| AbsToCon | Agda.Syntax.Translation.AbstractToConcrete |
| Abstract | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| abstract | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| abstractArgs | Agda.TypeChecking.Substitute |
| AbstractConstructorNotInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AbstractDef | Agda.Syntax.Common |
| AbstractDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AbstractMode | |
| 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 |
| AbstractModule | Agda.Syntax.Scope.Base |
| abstractN | Agda.TypeChecking.Names |
| AbstractName | Agda.Syntax.Scope.Base |
| AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract |
| abstractT | Agda.TypeChecking.Names |
| abstractTerm | Agda.TypeChecking.Abstract |
| abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete |
| abstractToConcreteHiding | Agda.Syntax.Translation.AbstractToConcrete |
| abstractToConcreteScope | Agda.Syntax.Translation.AbstractToConcrete |
| abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete |
| abstractType | Agda.TypeChecking.Abstract |
| Absurd | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| absurd | Agda.Utils.Empty |
| absurdBody | Agda.Syntax.Internal |
| AbsurdClause | Agda.Syntax.Reflected |
| AbsurdLam | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| AbsurdLambda | Agda.Auto.Syntax |
| absurdLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AbsurdMatch | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| AbsurdP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| absurdP | Agda.Syntax.Internal |
| AbsurdPattern | Agda.TypeChecking.Rules.LHS.Problem |
| absurdPatternName | Agda.Syntax.Internal |
| AbsurdPatternRequiresNoRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AbsurdPatternRequiresNoRHS_ | Agda.Interaction.Options.Warnings |
| absurdPatterns | Agda.TypeChecking.Rules.LHS.Problem |
| AbsurdRHS | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| AbsurdRHSS | Agda.Syntax.Abstract |
| absV | Agda.TypeChecking.Substitute |
| acceptableFileExts | Agda.Syntax.Parser |
| Access | Agda.Syntax.Common |
| acConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Account | |
| 1 (Type/Class) | Agda.Utils.Benchmark |
| 2 (Type/Class) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| acData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| acElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| aCon | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| acRanges | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ACState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Action | |
| 1 (Type/Class) | Agda.TypeChecking.CheckInternal |
| 2 (Data Constructor) | Agda.TypeChecking.CheckInternal |
| activateLoadedFileCache | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| activeBackend | Agda.Compiler.Backend |
| activeBackendMayEraseType | Agda.Compiler.Backend |
| acType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| acyclic | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| add | |
| 1 (Function) | Agda.Termination.Semiring |
| 2 (Function) | Agda.Termination.SparseMatrix |
| addAndUnblocker | Agda.TypeChecking.Constraints |
| addAwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addAwakeConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addblk | Agda.Auto.Typecheck |
| addClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addCoercions | Agda.Compiler.MAlonzo.Coerce |
| addCohesion | Agda.Syntax.Common |
| addColumn | Agda.Termination.SparseMatrix |
| addCompilerPragma | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addCompositionForRecord | Agda.TypeChecking.Rules.Record |
| addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addConstant' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addConstraint | |
| 1 (Function) | Agda.Utils.Warshall |
| 2 (Function) | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addConstraintTCM | Agda.TypeChecking.Constraints |
| addConstraintTo | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AddContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addCPUTime | Agda.Utils.Benchmark |
| addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addDataCons | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addDefaultLibraries | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addEdge | |
| 1 (Function) | Agda.Utils.Warshall |
| 2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| addend | Agda.Auto.Typecheck |
| AddExtraRef | Agda.Auto.NarrowingSearch |
| addFinalNewLine | Agda.Utils.String |
| addFlex | Agda.Utils.Warshall |
| addFlexRig | Agda.TypeChecking.Free.Lazy |
| addForeignCode | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addImport | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addImportCycleCheck | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addImportedInstances | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addLetBinding' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addLoneSig | Agda.Syntax.Concrete.Definitions.Monad |
| addModality | Agda.Syntax.Common |
| addModuleToScope | Agda.Syntax.Scope.Base |
| addNamedInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addNameToScope | Agda.Syntax.Scope.Base |
| addNode | Agda.Utils.Warshall |
| addOrUnblocker | Agda.TypeChecking.Constraints |
| addPragma | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addProfileOption | Agda.Utils.ProfileOptions |
| addQuantity | Agda.Syntax.Common |
| addRecordNameContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addRelevance | Agda.Syntax.Common |
| addRewriteRules | Agda.TypeChecking.Rewriting |
| addRewriteRulesFor | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addRow | Agda.Termination.SparseMatrix |
| addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addSuffix | Agda.Utils.Suffix |
| addtrailingargs | Agda.Auto.Syntax |
| addTrustedExecutables | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addTypedInstance | Agda.TypeChecking.Telescope |
| addTypedInstance' | Agda.TypeChecking.Telescope |
| addTypedPatterns | Agda.TypeChecking.Rules.Term |
| addUniqueInts | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| addUnknownInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| addVarToBind | Agda.Syntax.Scope.Monad |
| addWarning | Agda.TypeChecking.Warnings |
| ADef | Agda.TypeChecking.Positivity |
| aDefToMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AdjList | Agda.Utils.Warshall |
| adjust | |
| 1 (Function) | Agda.Utils.Trie |
| 2 (Function) | Agda.Utils.BiMap |
| adjustM | Agda.Utils.Map |
| adjustM' | Agda.Utils.Map |
| adjustPrecondition | Agda.Utils.BiMap |
| ADotT | Agda.Syntax.Abstract.Pattern |
| AesonException | |
| 1 (Type/Class) | Agda.Interaction.JSON |
| 2 (Data Constructor) | Agda.Interaction.JSON |
| AffineHole | Agda.Utils.AffineHole |
| AgdaError | Agda.Interaction.ExitCode |
| agdaErrorFromInt | Agda.Interaction.ExitCode |
| agdaErrorToInt | Agda.Interaction.ExitCode |
| AgdaFileType | Agda.Syntax.Common |
| AgdaLibFile | |
| 1 (Type/Class) | Agda.Interaction.Library.Base, Agda.Interaction.Library |
| 2 (Data Constructor) | Agda.Interaction.Library.Base, Agda.Interaction.Library |
| agdaTermType | Agda.TypeChecking.Unquote |
| agdaTypeType | Agda.TypeChecking.Unquote |
| aGuard | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| AHMModule | Agda.Auto.Options |
| AHMNone | Agda.Auto.Options |
| ALConPar | Agda.Auto.Syntax |
| ALCons | Agda.Auto.Syntax |
| AlexEOF | Agda.Syntax.Parser.Lexer |
| AlexError | Agda.Syntax.Parser.Lexer |
| alexGetByte | Agda.Syntax.Parser.Alex |
| alexGetChar | Agda.Syntax.Parser.Alex |
| AlexInput | |
| 1 (Type/Class) | Agda.Syntax.Parser.Alex |
| 2 (Data Constructor) | Agda.Syntax.Parser.Alex |
| alexInputPrevChar | Agda.Syntax.Parser.Alex |
| AlexReturn | Agda.Syntax.Parser.Lexer |
| alexScanUser | Agda.Syntax.Parser.Lexer |
| AlexSkip | Agda.Syntax.Parser.Lexer |
| AlexToken | Agda.Syntax.Parser.Lexer |
| align | Agda.Syntax.Common.Pretty |
| aLit | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| All | |
| 1 (Type/Class) | Agda.Utils.IndexedList |
| 2 (Type/Class) | Agda.Utils.TypeLevel |
| allApplyElims | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| AllAreOpaque | Agda.Syntax.Common |
| allBlockingDefs | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| allBlockingMetas | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| allBlockingProblems | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| allCohesions | Agda.Syntax.Common |
| allConsecutive | Agda.Utils.List |
| allDuplicates | Agda.Utils.List |
| allEqual | |
| 1 (Function) | Agda.Utils.List |
| 2 (Function) | Agda.Utils.List1 |
| allFlexVars | Agda.TypeChecking.Rules.LHS.Problem |
| allFreeVars | Agda.TypeChecking.Free |
| allHelpTopics | Agda.Interaction.Options.Help |
| allIndices | Agda.Utils.IndexedList |
| allJustM | Agda.Utils.Maybe |
| AllKindsOfNames | Agda.Syntax.Scope.Base |
| allKindsOfNames | Agda.Syntax.Scope.Base |
| allLeft | Agda.Utils.Either |
| allListT | Agda.Utils.ListT |
| allM | Agda.Utils.Monad |
| allMetaKinds | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AllMetas | Agda.Syntax.Internal.MetaVars |
| allMetas | Agda.Syntax.Internal.MetaVars |
| allMetas' | Agda.Syntax.Internal.MetaVars |
| allMetasList | Agda.Syntax.Internal.MetaVars |
| allNamesInScope | Agda.Syntax.Scope.Base |
| allNamesInScope' | Agda.Syntax.Scope.Base |
| allNameSpaces | Agda.Syntax.Scope.Base |
| allNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| allNullaryToStringTag | Agda.Interaction.JSON |
| allowAllReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AllowAmbiguousNames | Agda.Syntax.Scope.Base |
| AllowedReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AllowedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AllowedVar | Agda.TypeChecking.MetaVars.Occurs |
| allowedVars | Agda.TypeChecking.MetaVars.Occurs |
| allowNonTerminatingReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| allowOmittedFields | Agda.Interaction.JSON |
| allProjElims | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| allReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| allRelevances | Agda.Syntax.Common |
| allRelevantVars | Agda.TypeChecking.Free |
| allRelevantVarsIgnoring | Agda.TypeChecking.Free |
| allRight | Agda.Utils.Either |
| allThingsInScope | Agda.Syntax.Scope.Base |
| allUsedNames | Agda.Syntax.Abstract.UsedNames |
| allVars | Agda.TypeChecking.Free |
| AllWarnings | Agda.TypeChecking.Warnings |
| allWarnings | Agda.Interaction.Options.Warnings |
| ALNil | Agda.Auto.Syntax |
| ALProj | Agda.Auto.Syntax |
| Alt | |
| 1 (Type/Class) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| alter | Agda.Utils.BiMap |
| alterM | Agda.Utils.BiMap |
| alterPrecondition | Agda.Utils.BiMap |
| altM1 | Agda.Utils.Monad |
| AlwaysColour | Agda.Interaction.Options |
| alwaysMakeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| alwaysUnblock | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| Ambiguous | Agda.Interaction.FindFile |
| AmbiguousAnything | Agda.Syntax.Scope.Base |
| AmbiguousConProjs | Agda.Syntax.Scope.Base |
| AmbiguousConstructor | Agda.Syntax.Concrete.Definitions.Errors |
| AmbiguousDeclName | Agda.Syntax.Scope.Base |
| AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions.Errors |
| AmbiguousLib | Agda.Interaction.Library.Base |
| AmbiguousLocalVar | Agda.Syntax.Scope.Base |
| AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AmbiguousNameReason | Agda.Syntax.Scope.Base |
| ambiguousNamesInReason | Agda.Syntax.Scope.Base |
| AmbiguousNothing | Agda.Syntax.Scope.Base |
| AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AmbiguousProjectionError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AmbiguousQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| aModeToDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| amodLineage | Agda.Syntax.Scope.Base |
| amodName | Agda.Syntax.Scope.Base |
| anameKind | Agda.Syntax.Scope.Base |
| anameLineage | Agda.Syntax.Scope.Base |
| anameMetadata | Agda.Syntax.Scope.Base |
| anameName | Agda.Syntax.Scope.Base |
| AnArg | Agda.TypeChecking.Positivity |
| And | Agda.Auto.NarrowingSearch |
| and2M | Agda.Utils.Monad |
| andM | Agda.Utils.Monad |
| andThen | Agda.Syntax.Parser.LexActions |
| Ann | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| annLock | Agda.Syntax.Common |
| annotate | |
| 1 (Function) | Agda.Syntax.Common.Pretty |
| 2 (Function) | Agda.Utils.Parser.MemoisedCPS |
| annotateAspect | Agda.Syntax.Common.Pretty |
| annotateDecls | Agda.Syntax.Scope.Monad |
| annotateExpr | Agda.Syntax.Scope.Monad |
| annotatePattern | Agda.Syntax.Translation.ReflectedToAbstract |
| Annotation | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| AnnotationPattern | Agda.TypeChecking.Rules.LHS.Problem |
| AnnP | Agda.Syntax.Abstract |
| antiUnify | Agda.TypeChecking.Conversion |
| antiUnifyArgs | Agda.TypeChecking.Conversion |
| antiUnifyElims | Agda.TypeChecking.Conversion |
| antiUnifyType | Agda.TypeChecking.Conversion |
| AnyAbstract | Agda.Syntax.Abstract |
| anyAbstract | Agda.Syntax.Abstract |
| anyDefs | Agda.Termination.RecCheck |
| anyEllipsisVar | Agda.Interaction.MakeCase |
| AnyIsAbstract | Agda.Syntax.Common |
| anyIsAbstract | Agda.Syntax.Common |
| anyListT | Agda.Utils.ListT |
| anyM | Agda.Utils.Monad |
| AnyRigid | Agda.TypeChecking.MetaVars.Occurs |
| anyRigid | Agda.TypeChecking.MetaVars.Occurs |
| AnyWhere | Agda.Syntax.Concrete |
| aoHintMode | Agda.Auto.Options |
| aoHints | Agda.Auto.Options |
| aoMode | Agda.Auto.Options |
| aoPick | Agda.Auto.Options |
| aoTimeOut | Agda.Auto.Options |
| APatName | Agda.Syntax.Translation.ConcreteToAbstract |
| APatternLike | Agda.Syntax.Abstract.Pattern |
| App | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Auto.Syntax |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| 5 (Data Constructor) | Agda.TypeChecking.EtaContract |
| app | Agda.Syntax.Abstract |
| appBrackets | Agda.Syntax.Fixity |
| appBrackets' | Agda.Syntax.Fixity |
| appDef' | Agda.TypeChecking.Reduce |
| appDefE' | Agda.TypeChecking.Reduce |
| appElims | Agda.Auto.Syntax |
| append | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.List2 |
| appendArgNames | Agda.Syntax.Common |
| appendList | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.List2 |
| appHead | Agda.Auto.Syntax |
| AppInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| appInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AppK | Agda.Syntax.Concrete.Operators.Parser.Monad |
| Application | Agda.Syntax.Abstract.Views |
| Applied | Agda.Syntax.Scope.Base |
| Apply | |
| 1 (Type/Class) | Agda.Utils.TypeLevel |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 3 (Data Constructor) | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Reflected |
| 5 (Type/Class) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| 6 (Data Constructor) | Agda.Syntax.Abstract |
| apply | |
| 1 (Function) | Agda.Utils.AssocList |
| 2 (Function) | Agda.Compiler.JS.Substitution |
| 3 (Function) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| apply1 | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| applyCohesion | Agda.Syntax.Common |
| applyCohesionToContext | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyCohesionToContextOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyE | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| applyFlagsToTCWarnings | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| applyFlagsToTCWarningsPreserving | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| applyImportDirective | Agda.Syntax.Scope.Base |
| applyImportDirectiveM | Agda.Syntax.Scope.Monad |
| applyImportDirective_ | Agda.Syntax.Scope.Base |
| applyModality | Agda.Syntax.Common |
| applyModalityToContext | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyModalityToContextFunBody | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyModalityToContextOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyModalityToJudgementOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyN | Agda.TypeChecking.Names |
| applyN' | Agda.TypeChecking.Names |
| applyNLPatSubst | Agda.TypeChecking.Substitute |
| applyNLSubstToDom | Agda.TypeChecking.Substitute |
| ApplyOrIApply | Agda.TypeChecking.Coverage.Match |
| applyPatSubst | Agda.TypeChecking.Substitute |
| applyperm | Agda.Auto.CaseSplit |
| applyQuantity | Agda.Syntax.Common |
| applyQuantityToJudgement | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyRelevance | Agda.Syntax.Common |
| applyRelevanceToContext | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyRelevanceToContextFunBody | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyRelevanceToContextOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applyRelevanceToJudgementOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ApplyS | Agda.Syntax.Abstract |
| applys | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applySection' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| applySplitPSubst | Agda.TypeChecking.Coverage.Match |
| applySubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| applySubstTerm | Agda.TypeChecking.Substitute |
| applyTermE | Agda.TypeChecking.Substitute |
| applyUnder | Agda.TypeChecking.Rules.LHS.Unify.Types |
| applyUnless | Agda.Utils.Function |
| applyUnlessM | Agda.Utils.Function |
| applyWhen | Agda.Utils.Function |
| applyWhenM | Agda.Utils.Function |
| applyWhenVerboseS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend |
| appOK | Agda.Auto.Syntax |
| appOrigin | Agda.Syntax.Info |
| AppP | Agda.Syntax.Concrete |
| appP | Agda.Syntax.Concrete.Operators.Parser |
| appParens | Agda.Syntax.Info |
| appRange | Agda.Syntax.Info |
| approxConInduction | Agda.Syntax.Scope.Base |
| appTel | Agda.TypeChecking.Names |
| appUId | Agda.Auto.Syntax |
| AppV | Agda.Syntax.Concrete.Operators.Parser |
| AppView | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract.Views |
| appView | |
| 1 (Function) | Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract.Views |
| AppView' | Agda.Syntax.Abstract.Views |
| appView' | Agda.Syntax.Abstract.Views |
| apReduce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| apTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Arc | Agda.Utils.Warshall |
| areWeCaching | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Arg | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| ArgDescr | Agda.Interaction.Options |
| argFromDom | Agda.Syntax.Internal |
| argH | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| ArgInfo | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| argInfo | Agda.Syntax.Common |
| argInfoAnnotation | Agda.Syntax.Common |
| argInfoFreeVariables | Agda.Syntax.Common |
| argInfoHiding | Agda.Syntax.Common |
| argInfoModality | Agda.Syntax.Common |
| argInfoOrigin | Agda.Syntax.Common |
| ArgList | Agda.Auto.Syntax |
| argN | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| ArgName | Agda.Syntax.Common |
| argNameToString | Agda.Syntax.Common |
| ArgNode | Agda.TypeChecking.Positivity |
| Args | |
| 1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| 2 (Type/Class) | Agda.Syntax.Internal |
| 3 (Type/Class) | Agda.Syntax.Reflected |
| 4 (Type/Class) | Agda.Syntax.Abstract |
| ArgsCheckState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| argsFromElims | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| argsP | Agda.Syntax.Concrete.Operators.Parser |
| argsToElims | Agda.Syntax.Reflected |
| ArgT | Agda.TypeChecking.Records |
| argToDontCare | Agda.TypeChecking.Substitute |
| Argument | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| ArgumentCtx | Agda.Syntax.Fixity |
| argumentCtx_ | Agda.Syntax.Fixity |
| ArgumentIndex | Agda.Termination.CallMatrix |
| ArgUnused | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| ArgUsage | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| ArgUsed | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| ArgVars | Agda.TypeChecking.Names |
| Arity | Agda.Syntax.Common |
| arity | |
| 1 (Function) | Agda.Syntax.Internal |
| 2 (Function) | Agda.TypeChecking.CompiledClause |
| arityPiPath | Agda.TypeChecking.Telescope.Path |
| Array | |
| 1 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 2 (Type/Class) | Agda.Interaction.JSON |
| 3 (Data Constructor) | Agda.Interaction.JSON |
| arrow | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
| Arrows | Agda.Utils.TypeLevel |
| As | Agda.Syntax.Concrete |
| AsB | Agda.TypeChecking.Rules.LHS.Problem |
| AsBinding | Agda.TypeChecking.Rules.LHS.Problem |
| AsciiCounter | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| AsciiOnly | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options |
| asFinite | Agda.Utils.Float |
| AsIs | Agda.Interaction.Base |
| askGHCEnv | Agda.Compiler.MAlonzo.Misc |
| askGHCModuleEnv | Agda.Compiler.MAlonzo.Misc |
| askHsModuleEnv | Agda.Compiler.MAlonzo.Misc |
| askName | Agda.Syntax.Translation.ReflectedToAbstract |
| askR | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend |
| asksTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| askTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| askVar | Agda.Syntax.Translation.ReflectedToAbstract |
| asMainFunctionDef | Agda.Compiler.MAlonzo.Primitives |
| AsName | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| asName | Agda.Syntax.Concrete |
| AsName' | Agda.Syntax.Concrete |
| AsP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| asPatterns | Agda.TypeChecking.Rules.LHS.Problem |
| AsPatternShadowsConstructorOrPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AsPatternShadowsConstructorOrPatternSynonym_ | Agda.Interaction.Options.Warnings |
| Aspect | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| aspect | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| Aspects | |
| 1 (Type/Class) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| asQuantity | Agda.Syntax.Common |
| asRange | Agda.Syntax.Concrete |
| assertConOf | Agda.TypeChecking.Rewriting.NonLinPattern |
| assertPath | Agda.TypeChecking.Rewriting.NonLinPattern |
| assertPi | Agda.TypeChecking.Rewriting.NonLinPattern |
| assertProjOf | Agda.TypeChecking.Rewriting.NonLinPattern |
| Assign | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Interaction.Base |
| assign | Agda.TypeChecking.MetaVars |
| assignE | Agda.TypeChecking.Conversion |
| Assignments | Agda.Auto.CaseSplit |
| assignMeta | Agda.TypeChecking.MetaVars |
| assignMeta' | Agda.TypeChecking.MetaVars |
| Assigns | Agda.Syntax.Abstract |
| assignTerm | Agda.TypeChecking.MetaVars |
| assignTerm' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| assignTermTCM' | Agda.TypeChecking.MetaVars |
| assignV | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| assignWrapper | Agda.TypeChecking.MetaVars |
| AsSizes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Associativity | Agda.Syntax.Common |
| AssocList | Agda.Utils.AssocList |
| AsTermsOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AsTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| asView | Agda.Syntax.Abstract.Views |
| atClause | Agda.TypeChecking.Rules.Def |
| atLeastTwoParts | Agda.Syntax.Concrete.Operators.Parser |
| atomicLevel | Agda.Syntax.Internal |
| atomicModifyIORef | Agda.Utils.IORef |
| atomicModifyIORef' | Agda.Utils.IORef |
| atomicWriteIORef | Agda.Utils.IORef |
| atomizeLayers | Agda.Syntax.Parser.Literate |
| atomP | |
| 1 (Function) | Agda.Utils.Parser.MemoisedCPS |
| 2 (Function) | Agda.Syntax.Concrete.Operators.Parser |
| atTopLevel | |
| 1 (Function) | Agda.Interaction.BasicOps |
| 2 (Function) | Agda.Interaction.InteractionTop |
| Attribute | Agda.Syntax.Concrete.Attribute |
| AttributeKindNotEnabled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Attributes | Agda.Syntax.Concrete.Attribute |
| attributesForModality | Agda.Syntax.Concrete.Pretty |
| attributesMap | Agda.Syntax.Concrete.Attribute |
| augCallInfo | Agda.Termination.CallMatrix |
| augCallMatrix | Agda.Termination.CallMatrix |
| auto | Agda.Auto.Auto |
| AutoColour | Agda.Interaction.Options |
| AutoHintMode | Agda.Auto.Options |
| autoHintMode | Agda.Auto.Options |
| autoHints | Agda.Auto.Options |
| autoInline | Agda.TypeChecking.Inlining |
| autoMessage | Agda.Auto.Auto |
| autoMode | Agda.Auto.Options |
| AutoOptions | |
| 1 (Type/Class) | Agda.Auto.Options |
| 2 (Data Constructor) | Agda.Auto.Options |
| autoPick | Agda.Auto.Options |
| AutoProgress | Agda.Auto.Auto |
| autoProgress | Agda.Auto.Auto |
| AutoResult | |
| 1 (Type/Class) | Agda.Auto.Auto |
| 2 (Data Constructor) | Agda.Auto.Auto |
| autoTimeOut | Agda.Auto.Options |
| AutoToken | Agda.Auto.Options |
| autoTokens | Agda.Auto.Options |
| AwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Axiom | |
| 1 (Data Constructor) | Agda.Syntax.Reflected |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| axiomConstTransp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AxiomData | |
| 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 |
| AxiomDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| AxiomName | Agda.Syntax.Scope.Base |
| axiomName | Agda.Syntax.Abstract |
| AxiomS | Agda.Syntax.Abstract |