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

Index - Q

QAgda.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
qnameCAgda.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
qnameDAgda.TypeChecking.Serialise.Base
qnamedAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameFromListAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
QNameIdAgda.TypeChecking.Serialise.Base
qnameIdAgda.TypeChecking.Serialise.Base
qnameModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qnameToConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameToListAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qnameToMNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qNameTypeAgda.TypeChecking.Unquote
QOpAgda.Utils.Haskell.Syntax
QPBAgda.Auto.NarrowingSearch
QPBlockedAgda.Auto.NarrowingSearch
QPDoubleBlockedAgda.Auto.NarrowingSearch
Qual 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
QualifierAgda.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
qualifyMAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
qualifyQAgda.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
QuestionMark 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
QuickLaTeXAgda.Interaction.InteractionTop
QuotableNameAgda.Syntax.Scope.Base
Quote 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quoteAgda.Utils.String
quoteClauseWithKitAgda.TypeChecking.Quote
quoteConNameAgda.TypeChecking.Quote
QuoteContext 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quoteContextAgda.TypeChecking.Rules.Term
quoteDefnAgda.TypeChecking.Quote
quoteDefnWithKitAgda.TypeChecking.Quote
quoteDomAgda.TypeChecking.Quote
quoteDomWithKitAgda.TypeChecking.Quote
QuoteGoal 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quoteGoalAgda.TypeChecking.Rules.Term
quoteListAgda.TypeChecking.Quote
quoteListWithKitAgda.TypeChecking.Quote
quoteMetaAgda.TypeChecking.Quote
quoteNameAgda.TypeChecking.Quote
quoteNatAgda.TypeChecking.Quote
QuotePAgda.Syntax.Concrete
quotesAgda.Utils.Pretty
quoteStringAgda.TypeChecking.Quote
QuoteTerm 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quoteTermAgda.TypeChecking.Quote
quoteTermWithKitAgda.TypeChecking.Quote
quoteTypeAgda.TypeChecking.Quote
quoteTypeWithKitAgda.TypeChecking.Quote
QuotingKit 
1 (Type/Class)Agda.TypeChecking.Quote
2 (Data Constructor)Agda.TypeChecking.Quote
quotingKitAgda.TypeChecking.Quote
QVarOpAgda.Utils.Haskell.Syntax