A | Agda.Interaction.GhciTop |
AbortAssign | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
abortAssign | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
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 |
absBody | Agda.Syntax.Internal |
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 |
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 |
abstractFromType | Agda.TypeChecking.Primitive |
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 |
abstractPrim | Agda.TypeChecking.Primitive |
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 |
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.Matrix |
addColumn | Agda.Termination.Matrix |
addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addConstraint | Agda.Utils.Warshall |
addConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addCtxs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addCtxTel | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addDecl | Agda.Interaction.BasicOps |
addDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addEdge | Agda.Utils.Warshall |
addEquality | Agda.TypeChecking.Rules.LHS.Unify |
addFinalNewLine | Agda.Utils.String |
addFlex | Agda.Utils.Warshall |
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 |
addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addModuleToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
addNamesToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
addNameToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
addNewConstraints | Agda.TypeChecking.Constraints |
addNode | Agda.Utils.Warshall |
addRow | Agda.Termination.Matrix |
addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addSuffix | Agda.Utils.Suffix |
addVar | Agda.Compiler.Alonzo.PatternMonad |
addWildcard | Agda.Compiler.Alonzo.PatternMonad |
ADef | Agda.TypeChecking.Positivity |
AdjList | Agda.Utils.Warshall |
AlComment | Agda.Compiler.Alonzo.Haskell |
ALConPar | Agda.Auto.Syntax |
ALCons | Agda.Auto.Syntax |
AlDecl | |
1 (Type/Class) | Agda.Compiler.Alonzo.Haskell |
2 (Data Constructor) | Agda.Compiler.Alonzo.Haskell |
AlexEOF | Agda.Syntax.Parser.Lexer |
AlexError | Agda.Syntax.Parser.Lexer |
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 |
allEqual | Agda.Utils.List |
allHoles | Agda.Syntax.Internal.Pattern |
allHolesWithContents | Agda.Syntax.Internal.Pattern |
allM | Agda.Compiler.Agate.Classify |
allNames | Agda.Syntax.Abstract |
allNamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
alloc | Agda.Utils.Pointer |
allPaths | Agda.Utils.Graph |
allThingsInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
allVars | Agda.TypeChecking.Free |
ALNil | Agda.Auto.Syntax |
alreadyVisited | Agda.Interaction.Imports |
Ambiguous | Agda.Interaction.FindFile |
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 |
andM | Agda.Compiler.Agate.Classify |
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.Syntax.Abstract |
4 (Data Constructor) | Agda.TypeChecking.EtaContract |
appBrackets | Agda.Syntax.Fixity |
Application | Agda.Syntax.Abstract.Views |
Apply | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Type/Class) | Agda.TypeChecking.Substitute |
apply | Agda.TypeChecking.Substitute |
applyImportDirective | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
applyImportDirectiveM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
AppP | Agda.Syntax.Concrete |
appP | Agda.Syntax.Concrete.Operators.Parser |
apps | 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 |
argHiding | Agda.Syntax.Common |
ArgList | Agda.Auto.Syntax |
argName | Agda.Syntax.Internal |
ArgNode | Agda.TypeChecking.Positivity |
ArgPat | Agda.TypeChecking.With |
argpatts | Agda.Compiler.MAlonzo.Compiler |
Args | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
3 (Type/Class) | Agda.Syntax.Internal |
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 |
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 |
assignS | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
assignSort | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
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 |
auto | Agda.Auto.Auto |
axHsDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |