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