Agda-2.3.2: 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 | Agda.Interaction.EmacsCommand
abort | Agda.TypeChecking.MetaVars.Occurs
Abs |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
3 (Type/Class) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Internal
absApp | Agda.TypeChecking.Substitute
absAppHH | Agda.TypeChecking.Rules.LHS.Unify
absBody | Agda.TypeChecking.Substitute
abslamvarname | Agda.Auto.Convert
AbsModule | Agda.Syntax.Scope.Base
AbsName | Agda.Syntax.Scope.Base
absName | Agda.Syntax.Internal
absolute | Agda.Utils.FileName
AbsolutePath | Agda.Utils.FileName
abspatvarname | Agda.Auto.CaseSplit
AbsToCon | Agda.Syntax.Translation.AbstractToConcrete
Abstract |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.TypeChecking.Substitute
abstract | Agda.TypeChecking.Substitute
abstractArgs | Agda.TypeChecking.Substitute
AbstractDef | Agda.Syntax.Common
AbstractMode |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AbstractModule | Agda.Syntax.Scope.Base
AbstractName | Agda.Syntax.Scope.Base
AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract
AbstractTerm | Agda.TypeChecking.Abstract
abstractTerm | Agda.TypeChecking.Abstract
abstractToConcrete | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete
abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete
Absurd | Agda.Syntax.Concrete
AbsurdLam |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
AbsurdLambda | Agda.Auto.Syntax
AbsurdP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
AbsurdPatternRequiresNoRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AbsurdRHS |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Access | Agda.Syntax.Common
actOnMeta | Agda.Interaction.CommandLine.CommandLine
actualConstructor | Agda.TypeChecking.Rules.Def
acyclic | Agda.Utils.Graph
add |
1 (Function) | Agda.Termination.Semiring
2 (Function) | Agda.Termination.Matrix
3 (Function) | Agda.Termination.SparseMatrix
addAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
addblk | Agda.Auto.Typecheck
addColumn |
1 (Function) | Agda.Termination.Matrix
2 (Function) | 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
addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxString | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxString_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addCtxTel | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addDecl | Agda.Interaction.BasicOps
addDefName | Agda.Compiler.Epic.CompileState
addDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEdge | Agda.Utils.Warshall
addend | Agda.Auto.Typecheck
addEpicCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addEquality | Agda.TypeChecking.Rules.LHS.Unify
addEqualityHH | Agda.TypeChecking.Rules.LHS.Unify
addExtLambdaTele | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
AddExtraRef | Agda.Auto.NarrowingSearch
addFinalNewLine | Agda.Utils.String
addFlex | Agda.Utils.Warshall
addForcingAnnotations | Agda.TypeChecking.Forcing
addHaskellCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addHaskellImport | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
addHaskellType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addImport | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
addImportCycleCheck | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
addImportedThings | Agda.Interaction.Imports
addInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
addJSCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
addModule | Agda.Interaction.Highlighting.Dot
addModuleToScope | Agda.Syntax.Scope.Base
addNamesToScope | Agda.Syntax.Scope.Base
addNameToScope | Agda.Syntax.Scope.Base
addNode | Agda.Utils.Warshall
addRow |
1 (Function) | Agda.Termination.Matrix
2 (Function) | Agda.Termination.SparseMatrix
addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
addSuffix | Agda.Utils.Suffix
addtrailingargs | Agda.Auto.Syntax
ADef | Agda.TypeChecking.Positivity
AdjList | Agda.Utils.Warshall
adjust | Agda.Utils.HashMap
agdaTermType | Agda.TypeChecking.Quote
ALConPar | Agda.Auto.Syntax
ALCons | Agda.Auto.Syntax
AlexEOF | Agda.Syntax.Parser.Lexer
AlexError | Agda.Syntax.Parser.Lexer
alexGetByte | Agda.Syntax.Parser.Alex
alexGetChar | Agda.Syntax.Parser.Alex
AlexInput |
1 (Type/Class) | Agda.Syntax.Parser.Alex
2 (Data Constructor) | Agda.Syntax.Parser.Alex
alexInputPrevChar | Agda.Syntax.Parser.Alex
AlexReturn | Agda.Syntax.Parser.Lexer
alexScanUser | Agda.Syntax.Parser.Lexer
AlexSkip | Agda.Syntax.Parser.Lexer
AlexToken | Agda.Syntax.Parser.Lexer
align | Agda.Utils.Pretty
allEqual | Agda.Utils.List
allHoles | Agda.Syntax.Internal.Pattern
allHolesWithContents | Agda.Syntax.Internal.Pattern
allKindsOfNames | Agda.Syntax.Scope.Base
allMetaKinds | Agda.TypeChecking.MetaVars
allMetas | Agda.TypeChecking.MetaVars
allNames | Agda.Syntax.Abstract
allNamesInScope | Agda.Syntax.Scope.Base
allNamesInScope' | Agda.Syntax.Scope.Base
allowedVar | Agda.TypeChecking.MetaVars.Occurs
allPaths | Agda.Utils.Graph
allRight | Agda.Utils.Either
allThingsInScope | Agda.Syntax.Scope.Base
allVars | Agda.TypeChecking.Free
ALNil | Agda.Auto.Syntax
ALProj | Agda.Auto.Syntax
alreadyVisited | Agda.Interaction.Imports
altM1 | Agda.Utils.Monad
Ambiguous | Agda.Interaction.FindFile
AmbiguousFunClauses | Agda.Syntax.Concrete.Definitions
AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbiguousQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
amodName | Agda.Syntax.Scope.Base
anameKind | Agda.Syntax.Scope.Base
anameName | Agda.Syntax.Scope.Base
AnArg | Agda.TypeChecking.Positivity
And | Agda.Auto.NarrowingSearch
and2M | Agda.Utils.Monad
andM | Agda.Utils.Monad
AnyAbstract | Agda.Syntax.Abstract
anyAbstract | Agda.Syntax.Abstract
AnyWhere | Agda.Syntax.Concrete
APatName | Agda.Syntax.Translation.ConcreteToAbstract
App |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Compiler.Epic.AuxAST
4 (Data Constructor) | Agda.Syntax.Abstract
5 (Data Constructor) | Agda.TypeChecking.EtaContract
app | Agda.Syntax.Abstract
appBrackets | Agda.Syntax.Fixity
appDef | Agda.TypeChecking.Reduce
appDef' | Agda.TypeChecking.Reduce
Application | Agda.Syntax.Abstract.Views
Apply |
1 (Data Constructor) | Agda.Compiler.JS.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Abstract
4 (Type/Class) | Agda.TypeChecking.Substitute
apply |
1 (Function) | Agda.Compiler.JS.Substitution
2 (Function) | Agda.TypeChecking.Substitute
applyDroppingParameters | Agda.TypeChecking.InstanceArguments
ApplyHH | Agda.TypeChecking.Rules.LHS.Unify
applyHH | Agda.TypeChecking.Rules.LHS.Unify
applyImportDirective | Agda.Syntax.Scope.Base
applyImportDirectiveM | Agda.Syntax.Scope.Monad
applyperm | Agda.Auto.CaseSplit
applyRelevance | Agda.TypeChecking.Irrelevance
applyRelevanceToContext | Agda.TypeChecking.Irrelevance
applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
applySubst | Agda.TypeChecking.Substitute
AppP | Agda.Syntax.Concrete
appP | Agda.Syntax.Concrete.Operators.Parser
apps | Agda.Compiler.Epic.AuxAST
AppV | Agda.Syntax.Concrete.Operators.Parser
AppView |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract.Views
appView |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Views
apTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Arbitrary | Agda.Utils.QuickCheck
arbitrary | Agda.Utils.QuickCheck
arbitraryBoundedEnum | Agda.Utils.QuickCheck
arbitraryBoundedIntegral | Agda.Utils.QuickCheck
arbitraryBoundedRandom | Agda.Utils.QuickCheck
arbitrarySizedBoundedIntegral | Agda.Utils.QuickCheck
arbitrarySizedFractional | Agda.Utils.QuickCheck
arbitrarySizedIntegral | Agda.Utils.QuickCheck
Arc | Agda.Utils.Warshall
Arg |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
argFromDom | Agda.Syntax.Common
argH | Agda.TypeChecking.Primitive
argHiding | Agda.Syntax.Common
argIsDef | Agda.Compiler.Epic.NatDetection
ArgList | Agda.Auto.Syntax
argN | Agda.TypeChecking.Primitive
argName | Agda.Syntax.Internal
ArgNode | Agda.TypeChecking.Positivity
argpatts | Agda.Compiler.MAlonzo.Compiler
argRelevance | Agda.Syntax.Common
Args |
1 (Data Constructor) | Agda.Utils.QuickCheck
2 (Type/Class) | Agda.Utils.QuickCheck
3 (Type/Class) | Agda.Syntax.Internal
args | Agda.Compiler.JS.Compiler
ArgumentCtx | Agda.Syntax.Fixity
ArgumentTo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Arity | Agda.Syntax.Common
arity |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.TypeChecking.CompiledClause
arrow | Agda.Syntax.Concrete.Pretty
As | Agda.Syntax.Concrete
AsB | Agda.TypeChecking.Rules.LHS.Problem
AsBinding | Agda.TypeChecking.Rules.LHS.Problem
AsIs | Agda.Interaction.BasicOps
askPostpone | Agda.TypeChecking.Rules.LHS.Unify
AsName |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
asName | Agda.Syntax.Concrete
AsP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Aspect | Agda.Interaction.Highlighting.Precise
aspect | Agda.Interaction.Highlighting.Precise
asRange | Agda.Syntax.Concrete
Assign | Agda.Interaction.BasicOps
assign | Agda.TypeChecking.MetaVars
assignConstrTag | Agda.Compiler.Epic.CompileState
assignConstrTag' | Agda.Compiler.Epic.CompileState
assignTerm | Agda.TypeChecking.MetaVars
assignTerm' | Agda.TypeChecking.MetaVars
assignV | Agda.TypeChecking.MetaVars
associative | Agda.Utils.TestHelpers
asView | Agda.TypeChecking.Rules.LHS.Split
atomP | Agda.Syntax.Concrete.Operators.Parser
atTopLevel | Agda.Interaction.BasicOps
auto | Agda.Auto.Auto
Axiom |
1 (Data Constructor) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
axiomName | Agda.Syntax.Abstract