| A | Agda.Interaction.EmacsCommand |
| abort | Agda.TypeChecking.MetaVars.Occurs |
| 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 |
| absApp | Agda.TypeChecking.Substitute |
| absAppHH | Agda.TypeChecking.Rules.LHS.Unify |
| absBody | Agda.TypeChecking.Substitute |
| abslamvarname | Agda.Auto.Convert |
| AbsModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| AbsName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| absName | Agda.Syntax.Internal |
| absolute | Agda.Utils.FileName |
| AbsolutePath | Agda.Utils.FileName |
| abspatvarname | Agda.Auto.CaseSplit |
| AbsToCon | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| Abstract | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.TypeChecking.Substitute |
| abstract | Agda.TypeChecking.Substitute |
| abstractArgs | Agda.TypeChecking.Substitute |
| AbstractDef | Agda.Syntax.Common |
| AbstractMode | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AbstractModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| AbstractName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| AbstractTerm | Agda.TypeChecking.Abstract |
| abstractTerm | Agda.TypeChecking.Abstract |
| abstractToConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| Absurd | Agda.Syntax.Concrete |
| AbsurdLam | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| AbsurdLambda | Agda.Auto.Syntax |
| AbsurdP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| AbsurdPatternRequiresNoRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AbsurdRHS | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Access | Agda.Syntax.Common |
| actOnMeta | Agda.Interaction.CommandLine.CommandLine |
| actualConstructor | Agda.TypeChecking.Rules.Def |
| add | |
| 1 (Function) | Agda.Termination.Semiring |
| 2 (Function) | Agda.Termination.SparseMatrix |
| 3 (Function) | Agda.Termination.Matrix |
| addAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| addblk | Agda.Auto.Typecheck |
| addColumn | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| addConnection | Agda.Interaction.Highlighting.Dot |
| addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addConstraint | |
| 1 (Function) | Agda.Utils.Warshall |
| 2 (Function) | Agda.Compiler.Epic.Injection |
| 3 (Function) | Agda.TypeChecking.Constraints |
| addConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| addContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addCtxs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addCtxString | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addCtxTel | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addDecl | Agda.Interaction.BasicOps |
| addDefName | Agda.Compiler.Epic.CompileState |
| addDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addEdge | Agda.Utils.Warshall |
| addend | Agda.Auto.Typecheck |
| addEpicCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addEquality | Agda.TypeChecking.Rules.LHS.Unify |
| addEqualityHH | Agda.TypeChecking.Rules.LHS.Unify |
| addExtLambdaTele | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| AddExtraRef | Agda.Auto.NarrowingSearch |
| addFinalNewLine | Agda.Utils.String |
| addFlex | Agda.Utils.Warshall |
| addForcingAnnotations | Agda.TypeChecking.Forcing |
| addHaskellCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addHaskellImport | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| addHaskellType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addImport | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| addImportCycleCheck | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| addImportedThings | Agda.Interaction.Imports |
| addInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| addJSCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addModule | Agda.Interaction.Highlighting.Dot |
| addModuleToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| addNamesToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| addNameToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| addNode | Agda.Utils.Warshall |
| addRow | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addSuffix | Agda.Utils.Suffix |
| addtrailingargs | Agda.Auto.Syntax |
| ADef | Agda.TypeChecking.Positivity |
| AdjList | Agda.Utils.Warshall |
| agdaTermType | Agda.TypeChecking.Quote |
| 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.Utils.Pretty |
| allEqual | Agda.Utils.List |
| allHoles | Agda.Syntax.Internal.Pattern |
| allHolesWithContents | Agda.Syntax.Internal.Pattern |
| allMetaKinds | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| allNames | Agda.Syntax.Abstract |
| allNamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| allNamesInScope' | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| alloc | Agda.Utils.Pointer |
| allowedVar | Agda.TypeChecking.MetaVars.Occurs |
| allPaths | Agda.Utils.Graph |
| allRight | Agda.Utils.Either |
| allThingsInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| allVarOrIrrelevant | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| allVars | Agda.TypeChecking.Free |
| ALNil | Agda.Auto.Syntax |
| ALProj | Agda.Auto.Syntax |
| alreadyVisited | Agda.Interaction.Imports |
| Ambiguous | Agda.Interaction.FindFile |
| AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions |
| AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbiguousQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| amodName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| anameKind | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| anameName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| AnArg | Agda.TypeChecking.Positivity |
| And | Agda.Auto.NarrowingSearch |
| AnyAbstract | Agda.Syntax.Abstract |
| anyAbstract | Agda.Syntax.Abstract |
| AnyWhere | Agda.Syntax.Concrete |
| APatName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| App | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| 5 (Data Constructor) | Agda.TypeChecking.EtaContract |
| appBrackets | Agda.Syntax.Fixity |
| Application | Agda.Syntax.Abstract.Views |
| Apply | |
| 1 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| 4 (Type/Class) | Agda.TypeChecking.Substitute |
| apply | |
| 1 (Function) | Agda.Compiler.JS.Substitution |
| 2 (Function) | Agda.TypeChecking.Substitute |
| ApplyHH | Agda.TypeChecking.Rules.LHS.Unify |
| applyHH | Agda.TypeChecking.Rules.LHS.Unify |
| applyImportDirective | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| applyImportDirectiveM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| applyperm | Agda.Auto.CaseSplit |
| applyRelevance | Agda.TypeChecking.Irrelevance |
| applyRelevanceToContext | Agda.TypeChecking.Irrelevance |
| applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| AppP | Agda.Syntax.Concrete |
| appP | Agda.Syntax.Concrete.Operators.Parser |
| apps | |
| 1 (Function) | Agda.Compiler.Epic.AuxAST |
| 2 (Function) | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| 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 |
| Arbitrary | Agda.Utils.QuickCheck |
| arbitrary | Agda.Utils.QuickCheck |
| arbitraryBoundedIntegral | Agda.Utils.QuickCheck |
| arbitraryBoundedRandom | Agda.Utils.QuickCheck |
| arbitrarySizedBoundedIntegral | Agda.Utils.QuickCheck |
| arbitrarySizedFractional | Agda.Utils.QuickCheck |
| arbitrarySizedIntegral | Agda.Utils.QuickCheck |
| Arc | Agda.Utils.Warshall |
| Arg | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| argH | Agda.TypeChecking.Primitive |
| argHiding | Agda.Syntax.Common |
| argIsDef | Agda.Compiler.Epic.NatDetection |
| ArgList | Agda.Auto.Syntax |
| argN | Agda.TypeChecking.Primitive |
| argName | Agda.Syntax.Internal |
| ArgNode | Agda.TypeChecking.Positivity |
| argpatts | Agda.Compiler.MAlonzo.Compiler |
| argRelevance | Agda.Syntax.Common |
| Args | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| 3 (Type/Class) | Agda.Syntax.Internal |
| args | Agda.Compiler.JS.Compiler |
| ArgumentCtx | Agda.Syntax.Fixity |
| ArgumentTo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Arity | Agda.Syntax.Common |
| arity | Agda.Syntax.Internal |
| arrow | Agda.Syntax.Concrete.Pretty |
| As | Agda.Syntax.Concrete |
| AsB | Agda.TypeChecking.Rules.LHS |
| AsBinding | Agda.TypeChecking.Rules.LHS |
| AsIs | Agda.Interaction.BasicOps |
| askPostpone | Agda.TypeChecking.Rules.LHS.Unify |
| AsName | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| asName | Agda.Syntax.Concrete |
| AsP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Aspect | Agda.Interaction.Highlighting.Precise |
| aspect | Agda.Interaction.Highlighting.Precise |
| asRange | Agda.Syntax.Concrete |
| Assign | Agda.Interaction.BasicOps |
| assign | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| assignConstrTag | Agda.Compiler.Epic.CompileState |
| assignConstrTag' | Agda.Compiler.Epic.CompileState |
| assignTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| assignV | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| associative | Agda.Utils.TestHelpers |
| asView | Agda.TypeChecking.Rules.LHS.Split |
| atomP | Agda.Syntax.Concrete.Operators.Parser |
| atTopLevel | Agda.Interaction.BasicOps |
| auto | Agda.Auto.Auto |
| Axiom | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| axiomName | Agda.Syntax.Abstract |