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 - Q

Q | Agda.Interaction.EmacsCommand
Q0 | Agda.Syntax.Common
Q0Erased | Agda.Syntax.Common
Q0Inferred | Agda.Syntax.Common
Q0Origin | Agda.Syntax.Common
Q1 | Agda.Syntax.Common
Q1Inferred | Agda.Syntax.Common
Q1Linear | Agda.Syntax.Common
Q1Origin | Agda.Syntax.Common
QName |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
4 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
5 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qname |
1 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
2 (Function) | Agda.Compiler.JS.Compiler
qnameC | Agda.TypeChecking.Serialise.Base
qnameConcrete | Agda.Syntax.Scope.Base
QNamed |
1 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameD | Agda.TypeChecking.Serialise.Base
qnamed | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
QNameId | Agda.TypeChecking.Serialise.Base
qnameId | Agda.TypeChecking.Serialise.Base
qnameKind | Agda.Syntax.Scope.Base
qnameModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameToList0 | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameToMName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qNameType | Agda.TypeChecking.Unquote
QOp | Agda.Utils.Haskell.Syntax
Qual |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
QualifiedLocalModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
QualifiedLocalModule_ | Agda.Interaction.Options.Errors
Qualifier | Agda.Utils.Haskell.Syntax
qualify |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qualifyM | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qualifyQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qualify_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
Quantity | Agda.Syntax.Common
Quantity0 | Agda.Syntax.Common
Quantity1 | Agda.Syntax.Common
QuantityAttribute | Agda.Syntax.Concrete.Attribute
quantityAttributes | Agda.Syntax.Concrete.Attribute
quantityAttributeTable | Agda.Syntax.Concrete.Attribute
QuantityMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
QuantityMismatch_ | Agda.Interaction.Options.Errors
Quantityω | Agda.Syntax.Common
QueryResult |
1 (Type/Class) | Agda.TypeChecking.DiscrimTree
2 (Data Constructor) | Agda.TypeChecking.DiscrimTree
QuestionMark |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
QuickLaTeX | Agda.Interaction.Base
QuotableName | Agda.Syntax.Scope.Base
Quote |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
quote | Agda.Utils.String
quoteConName | Agda.TypeChecking.Quote
quoteDefn | Agda.TypeChecking.Quote
quoteDefnWithKit | Agda.TypeChecking.Quote
quotedName | Agda.TypeChecking.Quote
quoteDom | Agda.TypeChecking.Quote
quoteDomWithKit | Agda.TypeChecking.Quote
quoteList | Agda.TypeChecking.Quote
quoteListWithKit | Agda.TypeChecking.Quote
quoteMeta | Agda.TypeChecking.Quote
quoteName | Agda.TypeChecking.Quote
quoteNat | Agda.TypeChecking.Quote
QuoteP | Agda.Syntax.Concrete
quotes |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
quoteString | Agda.TypeChecking.Quote
QuoteTerm |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
quoteTerm | Agda.TypeChecking.Quote
quoteTermWithKit | Agda.TypeChecking.Quote
quoteType | Agda.TypeChecking.Quote
quoteTypeWithKit | Agda.TypeChecking.Quote
QuotingKit |
1 (Type/Class) | Agda.TypeChecking.Quote
2 (Data Constructor) | Agda.TypeChecking.Quote
quotingKit | Agda.TypeChecking.Quote
QVarOp | Agda.Utils.Haskell.Syntax
Qω | Agda.Syntax.Common
QωInferred | Agda.Syntax.Common
QωOrigin | Agda.Syntax.Common
QωPlenty | Agda.Syntax.Common