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 |
AbsName | Agda.Syntax.Scope.Base |
absName | Agda.Syntax.Internal |
absolute | Agda.Utils.FileName |
AbsolutePath | Agda.Utils.FileName |
abspatvarname | Agda.Auto.CaseSplit |
AbsToCon | Agda.Syntax.Translation.AbstractToConcrete |
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 |
AbstractName | Agda.Syntax.Scope.Base |
AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract |
AbstractTerm | Agda.TypeChecking.Abstract |
abstractTerm | Agda.TypeChecking.Abstract |
abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete |
abstractToConcreteEnv | Agda.Syntax.Translation.AbstractToConcrete |
abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete |
Absurd | Agda.Syntax.Concrete |
absurdBody | Agda.Syntax.Internal |
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 |
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 |
Account | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
actOnMeta | Agda.Interaction.CommandLine.CommandLine |
acyclic | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
add | |
1 (Function) | Agda.Termination.Semiring |
2 (Function) | Agda.Termination.SparseMatrix |
addAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
addblk | Agda.Auto.Typecheck |
addClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addColumn | Agda.Termination.SparseMatrix |
addConnection | Agda.Interaction.Highlighting.Dot |
addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addConstraint | |
1 (Function) | Agda.Utils.Warshall |
2 (Function) | Agda.TypeChecking.Constraints |
3 (Function) | Agda.Compiler.Epic.Injection |
addConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
AddContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addCPUTime | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addCtxs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addCtxString | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addCtxStrings_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addCtxString_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addCtxTel | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addDefName | Agda.Compiler.Epic.CompileState |
addDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addEdge | |
1 (Function) | Agda.Utils.Warshall |
2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver |
addend | Agda.Auto.Typecheck |
addEpicCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addEquality | Agda.TypeChecking.Rules.LHS.Unify |
addEqualityHH | Agda.TypeChecking.Rules.LHS.Unify |
AddExtraRef | Agda.Auto.NarrowingSearch |
addFinalNewLine | Agda.Utils.String |
addFlex | Agda.Utils.Warshall |
addForcingAnnotations | Agda.TypeChecking.Forcing |
addHaskellCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addHaskellExport | 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 |
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 |
addNamesToScope | Agda.Syntax.Scope.Base |
addNameToScope | Agda.Syntax.Scope.Base |
addNode | Agda.Utils.Warshall |
addRow | Agda.Termination.SparseMatrix |
addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addSuffix | Agda.Utils.Suffix |
addtrailingargs | Agda.Auto.Syntax |
ADef | Agda.TypeChecking.Positivity |
AdjList | Agda.Utils.Warshall |
adjust | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.Trie |
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 |
allApplyElims | Agda.Syntax.Internal |
allEqual | Agda.Utils.List |
allHoles | Agda.Syntax.Internal.Pattern |
allHolesWithContents | Agda.Syntax.Internal.Pattern |
allKindsOfNames | Agda.Syntax.Scope.Base |
allMetaKinds | Agda.TypeChecking.MetaVars |
allMetas | Agda.TypeChecking.MetaVars |
allNames | Agda.Syntax.Abstract |
allNamesInScope | Agda.Syntax.Scope.Base |
allNamesInScope' | Agda.Syntax.Scope.Base |
allNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
allowAllReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
AllowedReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
AllowedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
allowedVar | Agda.TypeChecking.MetaVars.Occurs |
allPaths | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
allReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
allRight | Agda.Utils.Either |
allThingsInScope | Agda.Syntax.Scope.Base |
allVars | Agda.TypeChecking.Free |
allWithKey | Agda.Utils.Map |
ALNil | Agda.Auto.Syntax |
ALProj | Agda.Auto.Syntax |
alreadyVisited | Agda.Interaction.Imports |
altM1 | Agda.Utils.Monad |
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.Abstract, Agda.Syntax.Internal |
AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
amodLineage | Agda.Syntax.Scope.Base |
amodName | Agda.Syntax.Scope.Base |
anameKind | Agda.Syntax.Scope.Base |
anameLineage | 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 |
AnyAbstract | Agda.Syntax.Abstract |
anyAbstract | Agda.Syntax.Abstract |
AnyWhere | Agda.Syntax.Concrete |
ap | Agda.Utils.Monad |
APatName | Agda.Syntax.Translation.ConcreteToAbstract |
App | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
5 (Data Constructor) | Agda.TypeChecking.EtaContract |
app | Agda.Syntax.Abstract |
appBrackets | Agda.Syntax.Fixity |
appDef | Agda.TypeChecking.Reduce |
appDef' | Agda.TypeChecking.Reduce |
appDefE | Agda.TypeChecking.Reduce |
appDefE' | Agda.TypeChecking.Reduce |
appDefE_ | Agda.TypeChecking.Reduce |
appDef_ | Agda.TypeChecking.Reduce |
appElims | Agda.Auto.Syntax |
appHead | Agda.Auto.Syntax |
appInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
Application | Agda.Syntax.Abstract.Views |
Applied | Agda.Syntax.Scope.Base |
Apply | |
1 (Data Constructor) | Agda.Compiler.JS.Syntax |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Syntax.Internal |
4 (Type/Class) | Agda.TypeChecking.Substitute |
apply | |
1 (Function) | Agda.Compiler.JS.Substitution |
2 (Function) | Agda.TypeChecking.Substitute |
applyDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
applyDroppingParameters | Agda.TypeChecking.InstanceArguments |
applyE | Agda.TypeChecking.Substitute |
applyFreq | Agda.TypeChecking.Test.Generators |
ApplyHH | Agda.TypeChecking.Rules.LHS.Unify |
applyHH | Agda.TypeChecking.Rules.LHS.Unify |
applyImportDirective | Agda.Syntax.Scope.Base |
applyImportDirectiveM | Agda.Syntax.Scope.Monad |
applyperm | Agda.Auto.CaseSplit |
applyRelevance | Agda.TypeChecking.Irrelevance |
applyRelevanceToContext | Agda.TypeChecking.Irrelevance |
applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
applySubst | Agda.TypeChecking.Substitute |
applyUnless | Agda.Utils.Function |
applyWhen | Agda.Utils.Function |
appOK | Agda.Auto.Syntax |
AppP | Agda.Syntax.Concrete |
appP | Agda.Syntax.Concrete.Operators.Parser |
apps | Agda.Compiler.Epic.AuxAST |
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 |
apTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Arbitrary | Agda.Utils.QuickCheck |
arbitrary | Agda.Utils.QuickCheck |
arbitraryBoundedEnum | 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 |
3 (Type/Class) | Agda.Syntax.Concrete |
4 (Type/Class) | Agda.Syntax.Abstract |
5 (Type/Class) | Agda.Syntax.Internal |
argColors | Agda.Syntax.Common |
argFromDom | Agda.Syntax.Common |
argFromElim | Agda.Syntax.Internal |
argH | Agda.TypeChecking.Primitive |
ArgInfo | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
3 (Type/Class) | Agda.Syntax.Concrete |
4 (Type/Class) | Agda.Syntax.Abstract |
5 (Type/Class) | Agda.Syntax.Internal |
argInfo | Agda.Syntax.Common |
argInfoColors | Agda.Syntax.Common |
argInfoHiding | Agda.Syntax.Common |
argInfoRelevance | 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 |
Args | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Type/Class) | Agda.Syntax.Internal |
args | Agda.Compiler.JS.Compiler |
argsFromElims | Agda.Syntax.Internal |
ArgsHH | Agda.TypeChecking.Rules.LHS.Unify |
argToDontCare | Agda.TypeChecking.Substitute |
Argument | Agda.Interaction.Highlighting.Precise |
ArgumentCtx | Agda.Syntax.Fixity |
ArgumentIndex | Agda.Termination.CallMatrix |
ArgumentTo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Arity | Agda.Syntax.Common |
arity | |
1 (Function) | Agda.Syntax.Internal |
2 (Function) | Agda.TypeChecking.CompiledClause |
arrow | Agda.Syntax.Concrete.Pretty |
As | Agda.Syntax.Concrete |
AsB | Agda.TypeChecking.Rules.LHS.Problem |
AsBinding | Agda.TypeChecking.Rules.LHS.Problem |
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 | |
1 (Type/Class) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Interaction.BasicOps |
assign | Agda.TypeChecking.MetaVars |
assignConstrTag | Agda.Compiler.Epic.CompileState |
assignConstrTag' | Agda.Compiler.Epic.CompileState |
assignE | Agda.TypeChecking.Conversion |
assignMeta | Agda.TypeChecking.MetaVars |
assignMeta' | Agda.TypeChecking.MetaVars |
Assigns | Agda.Syntax.Abstract |
assignTerm | Agda.TypeChecking.MetaVars |
assignTerm' | Agda.TypeChecking.MetaVars |
assignV | Agda.TypeChecking.MetaVars |
assignWrapper | Agda.TypeChecking.MetaVars |
associative | Agda.Utils.TestHelpers |
asView | Agda.Syntax.Abstract.Views |
AsWeightRelation | Agda.TypeChecking.SizedTypes.Tests |
atomP | Agda.Syntax.Concrete.Operators.Parser |
atTopLevel | Agda.Interaction.BasicOps |
augCallInfo | Agda.Termination.CallMatrix |
augCallMatrix | Agda.Termination.CallMatrix |
auto | Agda.Auto.Auto |
Axiom | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Type/Class) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
axiomName | Agda.Syntax.Abstract |