A | Agda.Interaction.EmacsCommand |
aArity | Agda.Syntax.Treeless |
aBody | Agda.Syntax.Treeless |
Abort | Agda.TypeChecking.Injectivity |
abort | Agda.TypeChecking.MetaVars.Occurs |
Abs | |
1 (Type/Class) | Agda.Syntax.Reflected |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Type/Class) | Agda.Syntax.Internal |
4 (Data Constructor) | Agda.Syntax.Internal |
5 (Type/Class) | Agda.Auto.Syntax |
6 (Data Constructor) | Agda.Auto.Syntax |
absApp | Agda.TypeChecking.Substitute |
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 |
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 |
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 |
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 |
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 |
AbsurdMatch | Agda.Syntax.Internal |
AbsurdP | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Data Constructor) | Agda.Syntax.Abstract |
absurdPatternName | Agda.Syntax.Internal |
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 | |
1 (Type/Class) | Agda.Utils.Benchmark |
2 (Type/Class) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
aCon | Agda.Syntax.Treeless |
Action | |
1 (Type/Class) | Agda.TypeChecking.CheckInternal |
2 (Data Constructor) | Agda.TypeChecking.CheckInternal |
activateLoadedFileCache | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad |
actOnMeta | Agda.Interaction.CommandLine |
acyclic | 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 |
addCoreCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addCoreConstr | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addCoreType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addCPUTime | Agda.Utils.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 |
addDefaultLibraries | Agda.TypeChecking.Monad.Options, 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.TypeChecking.SizedTypes.WarshallSolver |
2 (Function) | Agda.Utils.Warshall |
addend | Agda.Auto.Typecheck |
addEpicCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addExports | Agda.Compiler.UHC.CompileState |
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 |
addHaskellImportUHC | 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 |
addInlineHaskell | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
addJSCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
addMetaCon | Agda.Compiler.UHC.CompileState |
addMetaData | Agda.Compiler.UHC.CompileState |
addModule | Agda.Interaction.Highlighting.Dot |
addModuleToScope | Agda.Syntax.Scope.Base |
addNamedInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
addNamesToScope | Agda.Syntax.Scope.Base |
addNameToScope | Agda.Syntax.Scope.Base |
addNode | Agda.Utils.Warshall |
addRewriteRule | Agda.TypeChecking.Rewriting |
addRewriteRules | Agda.TypeChecking.Rewriting |
addRewriteRulesFor | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
addRow | Agda.Termination.SparseMatrix |
addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
addSignatureInstances | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
addSuffix | Agda.Utils.Suffix |
addToEnv | Agda.Compiler.UHC.FromAgda |
addtrailingargs | Agda.Auto.Syntax |
addTypedInstance | Agda.TypeChecking.Telescope |
addUnknownInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
ADef | Agda.TypeChecking.Positivity |
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 |
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 |
allApplyElims | Agda.Syntax.Internal |
allEqual | Agda.Utils.List |
allFreeVars | Agda.TypeChecking.Free |
allJustM | Agda.Utils.Maybe |
allJustsOrNothings | Agda.Utils.Maybe |
allKindsOfNames | Agda.Syntax.Scope.Base |
allLeft | Agda.Utils.Either |
allM | Agda.Utils.Monad |
allMetaKinds | Agda.TypeChecking.MetaVars |
allMetas | Agda.TypeChecking.MetaVars |
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 |
AllowAmbiguousNames | Agda.Syntax.Scope.Base |
AllowedReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
AllowedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
allowedVar | Agda.TypeChecking.MetaVars.Occurs |
allowNonTerminatingReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
allProjElims | Agda.Syntax.Internal |
allReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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.Old |
2 (Function) | Agda.TypeChecking.Free |
allWithKey | Agda.Utils.Map |
ALNil | Agda.Auto.Syntax |
ALProj | Agda.Auto.Syntax |
alreadyVisited | Agda.Interaction.Imports |
alt | Agda.Compiler.MAlonzo.Compiler |
alter | Agda.Utils.HashMap |
altM1 | Agda.Utils.Monad |
Ambiguous | Agda.Interaction.FindFile |
AmbiguousAnything | Agda.Syntax.Scope.Base |
AmbiguousConstructors | Agda.Syntax.Scope.Base |
AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions |
AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
AmbiguousNothing | Agda.Syntax.Scope.Base |
AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
AmbiguousQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, 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 |
anyDefs | Agda.Termination.RecCheck |
anyM | Agda.Utils.Monad |
AnyWhere | Agda.Syntax.Concrete |
APatName | Agda.Syntax.Translation.ConcreteToAbstract |
App | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
4 (Data Constructor) | Agda.TypeChecking.EtaContract |
5 (Data Constructor) | Agda.Auto.Syntax |
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 |
appendArgNames | Agda.Syntax.Internal |
appHead | Agda.Auto.Syntax |
appInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
AppK | Agda.Syntax.Concrete.Operators.Parser |
Application | Agda.Syntax.Abstract.Views |
Applied | Agda.Syntax.Scope.Base |
Apply | |
1 (Data Constructor) | Agda.Syntax.Reflected |
2 (Data Constructor) | Agda.Compiler.JS.Syntax |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Syntax.Internal |
5 (Type/Class) | Agda.TypeChecking.Substitute |
apply | |
1 (Function) | Agda.Compiler.JS.Substitution |
2 (Function) | Agda.TypeChecking.Substitute |
apply1 | Agda.TypeChecking.Substitute |
applyDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
applyDroppingParameters | Agda.TypeChecking.InstanceArguments |
applyE | Agda.TypeChecking.Substitute |
applyFreq | Agda.TypeChecking.Test.Generators |
applyImportDirective | Agda.Syntax.Scope.Base |
applyImportDirectiveM | Agda.Syntax.Scope.Monad |
applyPatSubst | Agda.TypeChecking.Substitute.Pattern |
applyperm | Agda.Auto.CaseSplit |
applyRelevance | Agda.TypeChecking.Irrelevance |
applyRelevanceToContext | Agda.TypeChecking.Irrelevance |
applys | Agda.TypeChecking.Substitute |
applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
applySection' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
applySubst | 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 |
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 |
arbitrarySizedNatural | Agda.Utils.QuickCheck |
Arc | Agda.Utils.Warshall |
areThereNonRigidMetaArguments | Agda.TypeChecking.InstanceArguments |
Arg | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | 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 |
argInfo | 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 |
argNameToString | Agda.Syntax.Internal |
ArgNode | Agda.TypeChecking.Positivity |
Args | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
3 (Type/Class) | Agda.Syntax.Reflected |
4 (Type/Class) | Agda.Syntax.Treeless |
5 (Type/Class) | Agda.Syntax.Abstract |
6 (Type/Class) | Agda.Syntax.Internal |
args | Agda.Compiler.JS.Compiler |
argsFromElims | Agda.Syntax.Internal |
argsP | Agda.Syntax.Concrete.Operators.Parser |
argsToElims | Agda.Syntax.Reflected |
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 |
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 |
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 |
Associativity | Agda.Syntax.Fixity |
AssocList | Agda.Utils.AssocList |
asView | Agda.Syntax.Abstract.Views |
AsWeightRelation | Agda.TypeChecking.SizedTypes.Tests |
atLeastTwoParts | Agda.Syntax.Concrete.Operators.Parser |
atomicModifyIORef | Agda.Utils.IORef |
atomicModifyIORef' | Agda.Utils.IORef |
atomicWriteIORef | Agda.Utils.IORef |
atomP | Agda.Syntax.Concrete.Operators.Parser |
atTopLevel | Agda.Interaction.BasicOps |
augCallInfo | Agda.Termination.CallMatrix |
augCallMatrix | Agda.Termination.CallMatrix |
auto | Agda.Auto.Auto |
AwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
Axiom | |
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Type/Class) | Agda.Syntax.Abstract |
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
axiomName | Agda.Syntax.Abstract |