Agda-2.6.0.1: 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
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
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
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
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
QPB | Agda.Auto.NarrowingSearch
QPBlocked | Agda.Auto.NarrowingSearch
QPDoubleBlocked | Agda.Auto.NarrowingSearch
Qual |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
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
Quantityω | Agda.Syntax.Common
QuestionMark |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
QuickLaTeX | Agda.Interaction.InteractionTop
QuotableName | Agda.Syntax.Scope.Base
Quote |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
quote | Agda.Utils.String
quoteClauseWithKit | Agda.TypeChecking.Quote
quoteConName | Agda.TypeChecking.Quote
QuoteContext |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
quoteContext | Agda.TypeChecking.Rules.Term
quoteDefn | Agda.TypeChecking.Quote
quoteDefnWithKit | Agda.TypeChecking.Quote
quoteDom | Agda.TypeChecking.Quote
quoteDomWithKit | Agda.TypeChecking.Quote
QuoteGoal |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
quoteGoal | Agda.TypeChecking.Rules.Term
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 | Agda.Utils.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