A | Agda.Interaction.EmacsCommand |
aArity | Agda.Syntax.Treeless, Agda.Compiler.Backend |
aBody | Agda.Syntax.Treeless, Agda.Compiler.Backend |
Abort | Agda.TypeChecking.Injectivity |
abort | Agda.TypeChecking.MetaVars.Occurs |
Abs | |
1 (Type/Class) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Auto.Syntax |
3 (Type/Class) | Agda.Syntax.Reflected |
4 (Data Constructor) | Agda.Syntax.Reflected |
5 (Type/Class) | Agda.Syntax.Internal |
6 (Data Constructor) | Agda.Syntax.Internal |
absApp | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
absBody | Agda.TypeChecking.Substitute.Class, 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 | |
1 (Type/Class) | Agda.Utils.FileName |
2 (Data Constructor) | Agda.Utils.FileName |
absPathD | Agda.TypeChecking.Serialise.Base |
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 |
AbstractName | Agda.Syntax.Scope.Base |
AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract |
abstractTerm | Agda.TypeChecking.Abstract |
abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete |
abstractToConcreteEnv | Agda.Syntax.Translation.AbstractToConcrete |
abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete |
abstractType | Agda.TypeChecking.Abstract |
Absurd | Agda.Syntax.Concrete |
absurd | Agda.Utils.Empty |
absurdBody | Agda.Syntax.Internal |
AbsurdClause | Agda.Syntax.Reflected |
AbsurdFocus | Agda.TypeChecking.Rules.LHS.Problem |
absurdFocusRange | Agda.TypeChecking.Rules.LHS.Problem |
absurdFocusType | Agda.TypeChecking.Rules.LHS.Problem |
absurdFocusVar | Agda.TypeChecking.Rules.LHS.Problem |
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 |
AbsurdP | |
1 (Data Constructor) | Agda.Syntax.Reflected |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Syntax.Internal |
4 (Data Constructor) | Agda.Syntax.Abstract |
absurdPatternName | Agda.Syntax.Internal |
AbsurdPatternRequiresNoRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AbsurdRHS | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
Access | Agda.Syntax.Common |
Account | |
1 (Type/Class) | Agda.Utils.Benchmark |
2 (Type/Class) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
aCon | Agda.Syntax.Treeless, 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 |
actOnMeta | Agda.Interaction.CommandLine |
acyclic | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
add | |
1 (Function) | Agda.Termination.Semiring |
2 (Function) | Agda.Termination.SparseMatrix |
addAwakeConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addAwakeConstraints | 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 |
addColumn | Agda.Termination.SparseMatrix |
addCompilerPragma | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addConnection | Agda.Interaction.Highlighting.Dot |
addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addConstraint | |
1 (Function) | Agda.Utils.Warshall |
2 (Function) | Agda.TypeChecking.Constraints |
addConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
addContext' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addCoreCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addCoreType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addCPUTime | Agda.Utils.Benchmark |
addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addDefaultLibraries | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addDeprecatedForeignCode | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addDeprecatedPragma | Agda.TypeChecking.Monad.Signature, 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.TypeChecking.SizedTypes.WarshallSolver |
2 (Function) | Agda.Utils.Warshall |
addend | Agda.Auto.Typecheck |
AddExtraRef | Agda.Auto.NarrowingSearch |
addFinalNewLine | Agda.Utils.String |
addFlex | Agda.Utils.Warshall |
addForcingAnnotations | Agda.TypeChecking.Forcing |
addForeignCode | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addHaskellCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addHaskellData | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addHaskellExport | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addHaskellImport | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addHaskellImportUHC | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addHaskellType | Agda.TypeChecking.Monad.Signature, 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 |
addImportedThings | Agda.Interaction.Imports |
addInlineHaskell | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addJSCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addModule | Agda.Interaction.Highlighting.Dot |
addModuleToScope | Agda.Syntax.Scope.Base |
addNamedInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addNamesToScope | Agda.Syntax.Scope.Base |
addNameToScope | Agda.Syntax.Scope.Base |
addNode | Agda.Utils.Warshall |
addPragma | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addRewriteRule | Agda.TypeChecking.Rewriting |
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 |
addTypedInstance | Agda.TypeChecking.Telescope |
addUnknownInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ADef | Agda.TypeChecking.Positivity |
aDefToMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AdjList | Agda.Utils.Warshall |
adjust | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.Trie |
AgdaLib | Agda.Interaction.Library.Base |
AgdaLibFile | Agda.Interaction.Library.Base |
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.Utils.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 |
allEqual | Agda.Utils.List |
allFlexVars | Agda.TypeChecking.Rules.LHS.Problem |
allFreeVars | Agda.TypeChecking.Free |
allIndices | Agda.Utils.IndexedList |
allJustM | Agda.Utils.Maybe |
allKindsOfNames | Agda.Syntax.Scope.Base |
allLeft | Agda.Utils.Either |
allM | Agda.Utils.Monad |
allMetaKinds | Agda.TypeChecking.MetaVars |
allMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AllNames | Agda.Syntax.Abstract |
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, 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 |
allowNonTerminatingReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
allProjElims | 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 |
allVars | |
1 (Function) | Agda.TypeChecking.Free |
2 (Function) | Agda.TypeChecking.Free.Old |
AllWarnings | Agda.TypeChecking.Warnings |
allWithKey | Agda.Utils.Map |
ALNil | Agda.Auto.Syntax |
ALProj | Agda.Auto.Syntax |
alreadyVisited | Agda.Interaction.Imports |
Alt | |
1 (Type/Class) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Utils.Haskell.Syntax |
alt | Agda.Compiler.MAlonzo.Compiler |
alter | Agda.Utils.HashMap |
altM1 | Agda.Utils.Monad |
Ambiguous | Agda.Interaction.FindFile |
AmbiguousAnything | Agda.Syntax.Scope.Base |
AmbiguousConProjs | Agda.Syntax.Scope.Base |
AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions |
AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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 |
anameName | Agda.Syntax.Scope.Base |
AnArg | Agda.TypeChecking.Positivity |
And | Agda.Auto.NarrowingSearch |
and2M | Agda.Utils.Monad |
andM | Agda.Utils.Monad |
annotate | Agda.Utils.Parser.MemoisedCPS |
antiUnify | Agda.TypeChecking.Conversion |
antiUnifyElims | Agda.TypeChecking.Conversion |
antiUnifyType | Agda.TypeChecking.Conversion |
AnyAbstract | Agda.Syntax.Abstract |
anyAbstract | Agda.Syntax.Abstract |
anyDefs | Agda.Termination.RecCheck |
anyM | Agda.Utils.Monad |
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.Auto.Syntax |
3 (Data Constructor) | Agda.Syntax.Concrete |
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 |
appDef' | Agda.TypeChecking.Reduce |
appDefE | Agda.TypeChecking.Reduce |
appDefE' | Agda.TypeChecking.Reduce |
appDefE_ | Agda.TypeChecking.Reduce |
appDef_ | Agda.TypeChecking.Reduce |
appElims | Agda.Auto.Syntax |
appendArgNames | Agda.Syntax.Internal |
appHead | Agda.Auto.Syntax |
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 (Data Constructor) | Agda.Compiler.JS.Syntax |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Data Constructor) | Agda.Syntax.Internal |
4 (Type/Class) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
5 (Data Constructor) | Agda.Syntax.Abstract |
6 (Type/Class) | Agda.Utils.TypeLevel |
apply | |
1 (Function) | Agda.Compiler.JS.Substitution |
2 (Function) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
apply1 | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
applyDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyDroppingParameters | Agda.TypeChecking.InstanceArguments |
applyE | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
applyFlagsToMaybeWarnings | Agda.Interaction.Imports |
applyFlagsToTCWarnings | Agda.TypeChecking.Errors |
applyImportDirective | Agda.Syntax.Scope.Base |
applyImportDirectiveM | Agda.Syntax.Scope.Monad |
applyNLPatSubst | Agda.TypeChecking.Substitute |
applyPatSubst | Agda.TypeChecking.Substitute |
applyperm | Agda.Auto.CaseSplit |
applyRelevance | Agda.TypeChecking.Irrelevance |
applyRelevanceToContext | Agda.TypeChecking.Irrelevance |
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 |
applySubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
applyUnless | Agda.Utils.Function |
applyUnlessM | Agda.Utils.Function |
applyWhen | Agda.Utils.Function |
applyWhenM | Agda.Utils.Function |
applyWhenVerboseS | Agda.TypeChecking.Reduce.Monad |
appOK | Agda.Auto.Syntax |
AppP | Agda.Syntax.Concrete |
appP | Agda.Syntax.Concrete.Operators.Parser |
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 |
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 |
areThereNonRigidMetaArguments | Agda.TypeChecking.InstanceArguments |
Arg | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
ArgDescr | Agda.Interaction.Options |
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 |
argInfo | Agda.Syntax.Common |
argInfoHiding | Agda.Syntax.Common |
argInfoOrigin | Agda.Syntax.Common |
argInfoRelevance | Agda.Syntax.Common |
ArgList | Agda.Auto.Syntax |
argN | Agda.TypeChecking.Primitive |
ArgName | Agda.Syntax.Internal |
argNameToString | Agda.Syntax.Internal |
ArgNode | Agda.TypeChecking.Positivity |
Args | |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
2 (Type/Class) | Agda.Syntax.Reflected |
3 (Type/Class) | Agda.Syntax.Internal |
4 (Type/Class) | Agda.Syntax.Abstract |
argsFromElims | Agda.Syntax.Internal |
argsP | Agda.Syntax.Concrete.Operators.Parser |
argsToElims | Agda.Syntax.Reflected |
ArgT | Agda.TypeChecking.Records |
argToDontCare | Agda.TypeChecking.Substitute |
Argument | Agda.Interaction.Highlighting.Precise |
ArgumentCtx | Agda.Syntax.Fixity |
ArgumentIndex | Agda.Termination.CallMatrix |
Arity | Agda.Syntax.Common |
arity | |
1 (Function) | Agda.Syntax.Internal |
2 (Function) | Agda.TypeChecking.CompiledClause |
arrow | Agda.Syntax.Concrete.Pretty |
Arrows | Agda.Utils.TypeLevel |
As | Agda.Syntax.Concrete |
AsB | Agda.TypeChecking.Rules.LHS.Problem |
AsBinding | Agda.TypeChecking.Rules.LHS.Problem |
AsIs | Agda.Interaction.BasicOps |
askName | Agda.Syntax.Translation.ReflectedToAbstract |
askR | Agda.TypeChecking.Reduce.Monad |
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 |
Aspects | |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
asRange | Agda.Syntax.Concrete |
assertCurrentModule | Agda.TypeChecking.Rules.Decl |
Assign | |
1 (Type/Class) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Interaction.BasicOps |
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.MetaVars |
assignV | Agda.TypeChecking.MetaVars |
assignWrapper | Agda.TypeChecking.MetaVars |
Associativity | Agda.Syntax.Fixity |
AssocList | Agda.Utils.AssocList |
asView | Agda.Syntax.Abstract.Views |
atClause | Agda.TypeChecking.Rules.Def |
atLeastTwoParts | Agda.Syntax.Concrete.Operators.Parser |
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 | Agda.Interaction.BasicOps |
augCallInfo | Agda.Termination.CallMatrix |
augCallMatrix | Agda.Termination.CallMatrix |
auto | Agda.Auto.Auto |
AutoHintMode | Agda.Auto.Options |
autoHintMode | Agda.Auto.Options |
autoHints | Agda.Auto.Options |
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.Abstract |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
axiomName | Agda.Syntax.Abstract |