A | |
1 (Data Constructor) | Agda.Interaction.EmacsCommand |
2 (Data Constructor) | Agda.Compiler.MAlonzo.Misc |
aArity | Agda.Syntax.Treeless, Agda.Compiler.Backend |
aBody | Agda.Syntax.Treeless, Agda.Compiler.Backend |
abort | |
1 (Function) | Agda.Interaction.Base |
2 (Function) | Agda.TypeChecking.MetaVars.Occurs |
abortIfBlocked | Agda.TypeChecking.Reduce |
Above | Agda.Compiler.JS.Pretty |
above | Agda.Utils.IntSet.Infinite |
Abs | |
1 (Type/Class) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Type/Class) | Agda.Syntax.Reflected |
4 (Data Constructor) | Agda.Syntax.Reflected |
absApp | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
absAppN | Agda.TypeChecking.Names |
absBody | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
AbsModule | Agda.Syntax.Scope.Base |
AbsN | |
1 (Type/Class) | Agda.TypeChecking.Names |
2 (Data Constructor) | Agda.TypeChecking.Names |
AbsName | Agda.Syntax.Scope.Base |
absName | Agda.Syntax.Internal |
AbsNameWithFixity | |
1 (Type/Class) | Agda.TypeChecking.Serialise.Instances.Abstract |
2 (Data Constructor) | Agda.TypeChecking.Serialise.Instances.Abstract |
absNName | Agda.TypeChecking.Names |
AbsOfCon | Agda.Syntax.Translation.ConcreteToAbstract |
AbsOfRef | Agda.Syntax.Translation.ReflectedToAbstract |
absolute | Agda.Utils.FileName |
AbsolutePath | |
1 (Type/Class) | Agda.Utils.FileName |
2 (Data Constructor) | Agda.Utils.FileName |
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 |
abstractN | Agda.TypeChecking.Names |
AbstractName | Agda.Syntax.Scope.Base |
AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract |
abstractT | Agda.TypeChecking.Names |
abstractTerm | Agda.TypeChecking.Abstract |
abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete |
abstractToConcreteHiding | Agda.Syntax.Translation.AbstractToConcrete |
abstractToConcreteScope | Agda.Syntax.Translation.AbstractToConcrete |
abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete |
abstractType | Agda.TypeChecking.Abstract |
Absurd | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
absurd | Agda.Utils.Empty |
absurdBinding | Agda.Syntax.Parser.Helpers |
absurdBody | Agda.Syntax.Internal |
AbsurdClause | Agda.Syntax.Reflected |
AbsurdLam | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
absurdLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AbsurdMatch | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
AbsurdP | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Data Constructor) | Agda.Syntax.Abstract |
absurdP | Agda.Syntax.Internal |
AbsurdPattern | Agda.TypeChecking.Rules.LHS.Problem |
absurdPatternName | Agda.Syntax.Internal |
AbsurdPatternRequiresNoRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AbsurdPatternRequiresNoRHS_ | Agda.Interaction.Options.Warnings |
absurdPatterns | Agda.TypeChecking.Rules.LHS.Problem |
AbsurdRHS | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
AbsurdRHSS | Agda.Syntax.Abstract |
absV | Agda.TypeChecking.Substitute |
acceptableFileExts | Agda.Syntax.Parser |
Access | Agda.Syntax.Common |
acConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Account | |
1 (Type/Class) | Agda.Utils.Benchmark |
2 (Type/Class) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
accum | Agda.Utils.IArray |
accumArray | Agda.Utils.IArray |
acData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
acElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
aCon | Agda.Syntax.Treeless, Agda.Compiler.Backend |
acRanges | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ACState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, 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 |
activeBackend | Agda.Compiler.Backend |
activeBackendMayEraseType | Agda.Compiler.Backend |
acType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
acyclic | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
add | |
1 (Function) | Agda.Termination.Semiring |
2 (Function) | Agda.Termination.SparseMatrix |
addAndUnblocker | Agda.TypeChecking.Constraints |
addAwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addAwakeConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addClauses | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addCoercions | Agda.Compiler.MAlonzo.Coerce |
addCohesion | Agda.Syntax.Common |
addColumn | Agda.Termination.SparseMatrix |
addCompilerPragma | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addCompositionForRecord | Agda.TypeChecking.Rules.Record |
addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addConstant' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addConstraint | |
1 (Function) | Agda.Utils.Warshall |
2 (Function) | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addConstraintTCM | Agda.TypeChecking.Constraints |
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 |
addCPUTime | Agda.Utils.Benchmark |
addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addDataCons | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addDefaultLibraries | Agda.TypeChecking.Monad.Options, 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.Utils.Warshall |
2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver |
addFinalNewLine | Agda.Utils.String |
addFlex | Agda.Utils.Warshall |
addFlexRig | Agda.TypeChecking.Free.Lazy |
addForeignCode | Agda.TypeChecking.Monad.State, 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 |
addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addLetBinding' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addLoneSig | Agda.Syntax.Concrete.Definitions.Monad |
addModality | Agda.Syntax.Common |
addModuleToScope | Agda.Syntax.Scope.Base |
addNameToScope | Agda.Syntax.Scope.Base |
addNode | Agda.Utils.Warshall |
addOrUnblocker | Agda.TypeChecking.Constraints |
addPragma | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addProfileOption | Agda.Utils.ProfileOptions |
addQuantity | Agda.Syntax.Common |
addRecordNameContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addRelevance | Agda.Syntax.Common |
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 |
addTrustedExecutables | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addType | Agda.Syntax.Parser.Helpers |
addTypedInstance | Agda.TypeChecking.InstanceArguments |
addTypedInstance' | Agda.TypeChecking.InstanceArguments |
addTypedPatterns | Agda.TypeChecking.Rules.Term |
addUniqueInts | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
addUnknownInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
addVarToBind | Agda.Syntax.Scope.Monad |
addWarning | Agda.TypeChecking.Warnings |
ADef | Agda.TypeChecking.Positivity |
aDefToMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AdjList | Agda.Utils.Warshall |
adjust | |
1 (Function) | Agda.Utils.Trie |
2 (Function) | Agda.Utils.BiMap |
adjustM | Agda.Utils.Map |
adjustM' | Agda.Utils.Map |
adjustPrecondition | Agda.Utils.BiMap |
ADotT | Agda.Syntax.Abstract.Pattern |
AesonException | |
1 (Type/Class) | Agda.Interaction.JSON |
2 (Data Constructor) | Agda.Interaction.JSON |
AffineHole | Agda.Utils.AffineHole |
AgdaError | Agda.Interaction.ExitCode |
agdaErrorFromInt | Agda.Interaction.ExitCode |
agdaErrorToInt | Agda.Interaction.ExitCode |
AgdaFileType | Agda.Syntax.Common |
AgdaLibFile | |
1 (Type/Class) | Agda.Interaction.Library.Base, Agda.Interaction.Library |
2 (Data Constructor) | Agda.Interaction.Library.Base, Agda.Interaction.Library |
agdaTermType | Agda.TypeChecking.Unquote |
agdaTypeType | Agda.TypeChecking.Unquote |
aGuard | Agda.Syntax.Treeless, Agda.Compiler.Backend |
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.Syntax.Common.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.Elim, Agda.Syntax.Internal |
AllAreOpaque | Agda.Syntax.Common |
allBlockingDefs | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
allBlockingMetas | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
allBlockingProblems | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
allCohesions | Agda.Syntax.Common |
allConsecutive | Agda.Utils.List |
allDuplicates | Agda.Utils.List |
allEqual | |
1 (Function) | Agda.Utils.List |
2 (Function) | Agda.Utils.List1 |
allFlexVars | Agda.TypeChecking.Rules.LHS.Problem |
allFreeVars | Agda.TypeChecking.Free |
allHelpTopics | Agda.Interaction.Options.Help |
allIndices | Agda.Utils.IndexedList |
allIrrelevantOrPropTel | Agda.TypeChecking.Irrelevance |
allJustM | Agda.Utils.Maybe |
AllKindsOfNames | Agda.Syntax.Scope.Base |
allKindsOfNames | Agda.Syntax.Scope.Base |
allLeft | Agda.Utils.Either |
allListT | Agda.Utils.ListT |
allM | Agda.Utils.Monad |
allMetaClasses | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AllMetas | Agda.Syntax.Internal.MetaVars |
allMetas | Agda.Syntax.Internal.MetaVars |
allMetas' | Agda.Syntax.Internal.MetaVars |
allMetasList | Agda.Syntax.Internal.MetaVars |
AllModules | Agda.Mimer.Options |
allNamesInScope | Agda.Syntax.Scope.Base |
allNamesInScope' | Agda.Syntax.Scope.Base |
allNameSpaces | Agda.Syntax.Scope.Base |
allNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
allNullaryToStringTag | Agda.Interaction.JSON |
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 |
allowedVars | Agda.TypeChecking.MetaVars.Occurs |
allowNonTerminatingReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
allowOmittedFields | Agda.Interaction.JSON |
allProjElims | Agda.Syntax.Internal.Elim, 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 |
allUsedNames | Agda.Syntax.Abstract.UsedNames |
allVars | Agda.TypeChecking.Free |
AllWarnings | Agda.TypeChecking.Warnings |
allWarnings | Agda.Interaction.Options.Warnings |
Alt | |
1 (Type/Class) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Utils.Haskell.Syntax |
alter | Agda.Utils.BiMap |
alterM | Agda.Utils.BiMap |
alterPrecondition | Agda.Utils.BiMap |
altM1 | Agda.Utils.Monad |
AlwaysColour | Agda.Interaction.Options |
alwaysMakeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
alwaysReportSDoc | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
alwaysReportSLn | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
alwaysUnblock | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
amap | Agda.Utils.IArray |
Ambiguous | Agda.Interaction.FindFile |
AmbiguousAnything | Agda.Syntax.Scope.Base |
AmbiguousConProjs | Agda.Syntax.Scope.Base |
AmbiguousConstructor | |
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AmbiguousDeclName | Agda.Syntax.Scope.Base |
AmbiguousField | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions.Errors |
AmbiguousLib | Agda.Interaction.Library.Base |
AmbiguousLocalVar | Agda.Syntax.Scope.Base |
AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AmbiguousNameReason | Agda.Syntax.Scope.Base |
ambiguousNamesInReason | Agda.Syntax.Scope.Base |
AmbiguousNothing | Agda.Syntax.Scope.Base |
AmbiguousOverloadedProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AmbiguousProjection | 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 |
anameMetadata | Agda.Syntax.Scope.Base |
anameName | Agda.Syntax.Scope.Base |
AnArg | Agda.TypeChecking.Positivity |
and2M | Agda.Utils.Monad |
andM | Agda.Utils.Monad |
andThen | Agda.Syntax.Parser.LexActions |
Ann | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
annLock | Agda.Syntax.Common |
annotate | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.Utils.Parser.MemoisedCPS |
annotateAspect | Agda.Syntax.Common.Pretty |
annotateDecls | Agda.Syntax.Scope.Monad |
annotateExpr | Agda.Syntax.Scope.Monad |
annotatePattern | Agda.Syntax.Translation.ReflectedToAbstract |
Annotation | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
AnnotationPattern | Agda.TypeChecking.Rules.LHS.Problem |
AnnP | Agda.Syntax.Abstract |
antiUnify | Agda.TypeChecking.Conversion |
antiUnifyArgs | Agda.TypeChecking.Conversion |
antiUnifyElims | Agda.TypeChecking.Conversion |
antiUnifyType | Agda.TypeChecking.Conversion |
AnyAbstract | Agda.Syntax.Abstract |
anyAbstract | Agda.Syntax.Abstract |
anyDefs | Agda.Termination.RecCheck |
anyEllipsisVar | Agda.Interaction.MakeCase |
AnyIsAbstract | Agda.Syntax.Common |
anyIsAbstract | Agda.Syntax.Common |
anyListT | Agda.Utils.ListT |
anyM | Agda.Utils.Monad |
AnyRigid | Agda.TypeChecking.MetaVars.Occurs |
anyRigid | Agda.TypeChecking.MetaVars.Occurs |
AnyWhere | Agda.Syntax.Concrete |
APatName | Agda.Syntax.Translation.ConcreteToAbstract |
APatternLike | Agda.Syntax.Abstract.Pattern |
App | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.TypeChecking.EtaContract |
app | Agda.Syntax.Abstract |
appBrackets | Agda.Syntax.Fixity |
appBrackets' | Agda.Syntax.Fixity |
appDef' | Agda.TypeChecking.Reduce |
appDefE' | Agda.TypeChecking.Reduce |
append | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.Utils.List2 |
appendArgNames | Agda.Syntax.Common |
appendList | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.Utils.List2 |
AppInfo | |
1 (Type/Class) | Agda.Syntax.Info |
2 (Data Constructor) | Agda.Syntax.Info |
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 (Type/Class) | Agda.Utils.TypeLevel |
2 (Data Constructor) | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Reflected |
4 (Data Constructor) | Agda.Compiler.JS.Syntax |
5 (Type/Class) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
6 (Data Constructor) | Agda.Syntax.Abstract |
apply | |
1 (Function) | Agda.Utils.AssocList |
2 (Function) | Agda.Compiler.JS.Substitution |
3 (Function) | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
apply1 | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
applyAttr | Agda.Syntax.Parser.Helpers |
applyAttrs | Agda.Syntax.Parser.Helpers |
applyAttrs1 | Agda.Syntax.Parser.Helpers |
applyCohesion | Agda.Syntax.Common |
applyCohesionToContext | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyCohesionToContextOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyE | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
applyFlagsToTCWarnings | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
applyFlagsToTCWarningsPreserving | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
applyImportDirective | Agda.Syntax.Scope.Base |
applyImportDirectiveM | Agda.Syntax.Scope.Monad |
applyImportDirective_ | Agda.Syntax.Scope.Base |
applyModality | Agda.Syntax.Common |
applyModalityToContext | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyModalityToContextFunBody | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyModalityToContextOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyModalityToJudgementOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyN | Agda.TypeChecking.Names |
applyN' | Agda.TypeChecking.Names |
applyNLPatSubst | Agda.TypeChecking.Substitute |
applyNLSubstToDom | Agda.TypeChecking.Substitute |
ApplyOrIApply | Agda.TypeChecking.Coverage.Match |
applyPatSubst | Agda.TypeChecking.Substitute |
applyQuantity | Agda.Syntax.Common |
applyQuantityToJudgement | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyRelevance | Agda.Syntax.Common |
applyRelevanceToContext | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyRelevanceToContextFunBody | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyRelevanceToContextOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
applyRelevanceToJudgementOnly | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ApplyS | Agda.Syntax.Abstract |
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 |
applySplitPSubst | Agda.TypeChecking.Coverage.Match |
applySubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
applySubstTerm | Agda.TypeChecking.Substitute |
applyTermE | Agda.TypeChecking.Substitute |
applyUnder | Agda.TypeChecking.Rules.LHS.Unify.Types |
applyUnless | Agda.Utils.Function |
applyUnlessM | Agda.Utils.Function |
applyUnlessNull | Agda.Utils.Null |
applyWhen | Agda.Utils.Function |
applyWhenJust | Agda.Utils.Function |
applyWhenM | Agda.Utils.Function |
applyWhenNothing | Agda.Utils.Function |
applyWhenVerboseS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend |
appOrigin | Agda.Syntax.Info |
AppP | Agda.Syntax.Concrete |
appP | Agda.Syntax.Concrete.Operators.Parser |
appParens | Agda.Syntax.Info |
appRange | Agda.Syntax.Info |
approxConInduction | Agda.Syntax.Scope.Base |
appTel | Agda.TypeChecking.Names |
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 |
AppView' | Agda.Syntax.Abstract.Views |
appView' | 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 |
areWeCaching | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Arg | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
ArgDescr | Agda.Interaction.Options |
argFromDom | Agda.Syntax.Internal |
argH | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
ArgInfo | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
argInfo | Agda.Syntax.Common |
argInfoAnnotation | Agda.Syntax.Common |
argInfoFreeVariables | Agda.Syntax.Common |
argInfoHiding | Agda.Syntax.Common |
argInfoModality | Agda.Syntax.Common |
argInfoOrigin | Agda.Syntax.Common |
argN | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
ArgName | Agda.Syntax.Common |
argNameToString | Agda.Syntax.Common |
ArgNode | Agda.TypeChecking.Positivity |
Args | |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
2 (Type/Class) | Agda.Syntax.Internal |
3 (Type/Class) | Agda.Syntax.Reflected |
4 (Type/Class) | Agda.Syntax.Abstract |
ArgsCheckState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
argsFromElims | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
argsP | Agda.Syntax.Concrete.Operators.Parser |
argsToElims | Agda.Syntax.Reflected |
ArgT | Agda.TypeChecking.Records |
argToDontCare | Agda.TypeChecking.Substitute |
Argument | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
ArgumentCtx | Agda.Syntax.Fixity |
argumentCtx_ | Agda.Syntax.Fixity |
ArgumentIndex | Agda.Termination.CallMatrix |
ArgUnused | Agda.Syntax.Treeless, Agda.Compiler.Backend |
ArgUsage | Agda.Syntax.Treeless, Agda.Compiler.Backend |
ArgUsed | Agda.Syntax.Treeless, Agda.Compiler.Backend |
ArgVars | Agda.TypeChecking.Names |
Arity | Agda.Syntax.Common |
arity | |
1 (Function) | Agda.Syntax.Internal |
2 (Function) | Agda.TypeChecking.CompiledClause |
arityPiPath | Agda.TypeChecking.Telescope.Path |
Array | |
1 (Type/Class) | Agda.Utils.IArray |
2 (Data Constructor) | Agda.Compiler.JS.Syntax |
3 (Type/Class) | Agda.Interaction.JSON |
4 (Data Constructor) | Agda.Interaction.JSON |
array | Agda.Utils.IArray |
arrow | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
Arrows | Agda.Utils.TypeLevel |
As | Agda.Syntax.Concrete |
AsB | Agda.TypeChecking.Rules.LHS.Problem |
AsBinding | Agda.TypeChecking.Rules.LHS.Problem |
AsciiCounter | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
AsciiOnly | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options |
asFinite | Agda.Utils.Float |
AsIs | Agda.Interaction.Base |
askGHCEnv | Agda.Compiler.MAlonzo.Misc |
askGHCModuleEnv | Agda.Compiler.MAlonzo.Misc |
askHsModuleEnv | Agda.Compiler.MAlonzo.Misc |
askName | Agda.Syntax.Translation.ReflectedToAbstract |
askR | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend |
asksTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
askTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
askVar | Agda.Syntax.Translation.ReflectedToAbstract |
asMainFunctionDef | Agda.Compiler.MAlonzo.Primitives |
AsName | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Concrete |
asName | Agda.Syntax.Concrete |
AsName' | Agda.Syntax.Concrete |
AsP | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
AsPatternInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
asPatterns | Agda.TypeChecking.Rules.LHS.Problem |
AsPatternShadowsConstructorOrPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AsPatternShadowsConstructorOrPatternSynonym_ | Agda.Interaction.Options.Warnings |
Aspect | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
aspect | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
Aspects | |
1 (Type/Class) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
asQuantity | Agda.Syntax.Common |
asRange | Agda.Syntax.Concrete |
assertConOf | Agda.TypeChecking.Rewriting.NonLinPattern |
assertPath | Agda.TypeChecking.Rewriting.NonLinPattern |
assertPi | Agda.TypeChecking.Rewriting.NonLinPattern |
assertProjOf | Agda.TypeChecking.Rewriting.NonLinPattern |
Assign | |
1 (Type/Class) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Interaction.Base |
assign | Agda.TypeChecking.MetaVars |
assignE | Agda.TypeChecking.Conversion |
assignMeta | Agda.TypeChecking.MetaVars |
assignMeta' | Agda.TypeChecking.MetaVars |
Assigns | Agda.Syntax.Abstract |
assignTerm | Agda.TypeChecking.MetaVars |
assignTerm' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
assignTermTCM' | Agda.TypeChecking.MetaVars |
assignV | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
assignWrapper | Agda.TypeChecking.MetaVars |
AsSizes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Associativity | Agda.Syntax.Common |
AssocList | Agda.Utils.AssocList |
assocs | Agda.Utils.IArray |
AsTermsOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AsTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
asView | Agda.Syntax.Abstract.Views |
atClause | Agda.TypeChecking.Rules.Def |
atLeastTwoParts | Agda.Syntax.Concrete.Operators.Parser |
atomicLevel | Agda.Syntax.Internal |
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 | |
1 (Function) | Agda.Interaction.BasicOps |
2 (Function) | Agda.Interaction.InteractionTop |
Attr | |
1 (Type/Class) | Agda.Syntax.Parser.Helpers |
2 (Data Constructor) | Agda.Syntax.Parser.Helpers |
Attribute | Agda.Syntax.Concrete.Attribute |
AttributeKindNotEnabled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Attributes | Agda.Syntax.Concrete.Attribute |
attributesForModality | Agda.Syntax.Concrete.Pretty |
attributesMap | Agda.Syntax.Concrete.Attribute |
attrName | Agda.Syntax.Parser.Helpers |
attrRange | Agda.Syntax.Parser.Helpers |
augCallInfo | Agda.Termination.CallMatrix |
augCallMatrix | Agda.Termination.CallMatrix |
AutoColour | Agda.Interaction.Options |
autoInline | Agda.TypeChecking.Inlining |
AwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Axiom | |
1 (Data Constructor) | Agda.Syntax.Reflected |
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
axiomConstTransp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AxiomData | |
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 |
AxiomDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
AxiomName | Agda.Syntax.Scope.Base |
axiomName | Agda.Syntax.Abstract |
AxiomS | Agda.Syntax.Abstract |