Agda-2.8.0: A dependently typed functional programming language and proof assistant

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - A

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
AbsentRHSRequiresAbsurdPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbsentRHSRequiresAbsurdPattern_ | Agda.Interaction.Options.Errors
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, Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Utils.FileName
AbsTerm | Agda.TypeChecking.Abstract
absTerm | Agda.TypeChecking.Abstract
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
AbstractConstructorNotInScope_ | Agda.Interaction.Options.Errors
AbstractDef | Agda.Syntax.Common
AbstractDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbstractInLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbstractInLetBindings_ | Agda.Interaction.Options.Warnings
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
abstractT | Agda.TypeChecking.Names
abstractTerm | Agda.TypeChecking.Abstract
abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteHiding | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteQName | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteScope | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteTelescope | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteUnqualify | 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
absurdNEMap | Agda.Utils.Map1
AbsurdP |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
absurdP | Agda.Syntax.Internal
AbsurdPattern | Agda.TypeChecking.Rules.LHS.Problem
absurdPatternName | Agda.Syntax.Internal
AbsurdPatternRequiresAbsentRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbsurdPatternRequiresAbsentRHS_ | 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
Access | Agda.Syntax.Common
acCheckedArgs | 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
acFun | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
aCon | Agda.Syntax.Treeless, 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.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
activeBackendMayEraseType | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, 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 | 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 | Agda.TypeChecking.SizedTypes.WarshallSolver
addFinalNewLine | Agda.Utils.String
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
addOrUnblocker | Agda.TypeChecking.Constraints
addPolarity | Agda.Syntax.Common
addPolarity' | Agda.Syntax.Common
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
adjust |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.Trie
3 (Function) | Agda.Utils.BiMap
adjustAt | Agda.Utils.Map1
adjustM | Agda.Utils.Map
adjustM' | Agda.Utils.Map
adjustMax | Agda.Utils.Map1
adjustMaxWithKey | Agda.Utils.Map1
adjustMin | Agda.Utils.Map1
adjustMinWithKey | Agda.Utils.Map1
adjustPrecondition | Agda.Utils.BiMap
adjustWithKey | Agda.Utils.Map1
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
agdaFileExtensions | Agda.Syntax.Parser
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
agdaLibFiles | Agda.Interaction.Library.Base
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 |
1 (Function) | Agda.Utils.List
2 (Function) | 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
allModalPolarities | Agda.Syntax.Common
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
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 |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.BiMap
alter' | Agda.Utils.Map1
alterF | Agda.Utils.Map1
alterF' | Agda.Utils.Map1
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
AmbiguousConstructorN_ | Agda.Interaction.Options.Errors
AmbiguousConstructor_ | Agda.Interaction.Options.Errors
AmbiguousDeclName | Agda.Syntax.Scope.Base
AmbiguousField | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousField_ | Agda.Interaction.Options.Errors
AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions.Errors
AmbiguousFunClauses_ | Agda.Interaction.Options.Errors
AmbiguousLib | Agda.Interaction.Library.Base
AmbiguousLocalVar | Agda.Syntax.Scope.Base
AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousModule_ | Agda.Interaction.Options.Errors
AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousNameReason | Agda.Syntax.Scope.Base
ambiguousNamesInReason | Agda.Syntax.Scope.Base
AmbiguousName_ | Agda.Interaction.Options.Errors
AmbiguousNothing | Agda.Syntax.Scope.Base
AmbiguousOverloadedProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousOverloadedProjection_ | Agda.Interaction.Options.Errors
AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousParseForApplication_ | Agda.Interaction.Options.Errors
AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousParseForLHS_ | Agda.Interaction.Options.Errors
AmbiguousProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousProjection_ | Agda.Interaction.Options.Errors
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
AmbiguousTopLevelModuleName_ | Agda.Interaction.Options.Errors
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
Annotation |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
AnnotationPattern | Agda.TypeChecking.Rules.LHS.Problem
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
AnyWhere_ | Agda.Syntax.Concrete
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.Compiler.JS.Syntax
3 (Data Constructor) | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Reflected
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
apply2 | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyAttr | Agda.Syntax.Parser.Helpers
applyAttributes | 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
applyPolarity | Agda.Syntax.Common
applyPolarityToContext | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
applyUnlessIts | Agda.Utils.Function
applyUnlessM | Agda.Utils.Function
applyUnlessNull | Agda.Utils.Null
applyWhen | Agda.Utils.Function
applyWhenIts | 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
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.Utils.GetOpt, 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
ArgOrder | Agda.Utils.GetOpt
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 (Data Constructor) | Agda.Interaction.JSON
2 (Type/Class) | Agda.Interaction.JSON
3 (Type/Class) | Agda.Utils.IArray
4 (Data Constructor) | Agda.Compiler.JS.Syntax
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.Internal, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Compiler.Backend
AsciiOnly | Agda.Syntax.Concrete.Glyph, Agda.Interaction.Options, Agda.Syntax.Concrete.Pretty
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
AsPatternInPatternSynonym_ | Agda.Interaction.Options.Errors
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
assertPristineRelevance | Agda.Syntax.Parser.Helpers
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 |
1 (Function) | Agda.Utils.IArray
2 (Function) | Agda.Utils.Map1
AsTermsOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AsTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
asum | Agda.Utils.List
asum1 | Agda.Utils.List
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.Concrete.Attribute
2 (Data Constructor) | Agda.Syntax.Concrete.Attribute
Attribute | Agda.Syntax.Concrete.Attribute
AttributeKindNotEnabled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AttributeKindNotEnabled_ | Agda.Interaction.Options.Errors
Attributes | Agda.Syntax.Concrete.Attribute
attributesForModality | Agda.Syntax.Concrete.Pretty
attributesMap | Agda.Syntax.Concrete.Attribute
attrName | Agda.Syntax.Concrete.Attribute
attrRange | Agda.Syntax.Concrete.Attribute
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