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

Index - Q

QAgda.Interaction.EmacsCommand
QName 
1 (Type/Class)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qname 
1 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
2 (Function)Agda.Compiler.JS.Compiler
qnameCAgda.TypeChecking.Serialise.Base
QNamed 
1 (Type/Class)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qnameDAgda.TypeChecking.Serialise.Base
qnamedAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qnameFromListAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
QNameIdAgda.TypeChecking.Serialise.Base
qnameIdAgda.TypeChecking.Serialise.Base
qnameModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qnameNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qnamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qnameToConcreteAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qnameToListAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qnameToMNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qNameTypeAgda.TypeChecking.Unquote
QPBAgda.Auto.NarrowingSearch
QPBlockedAgda.Auto.NarrowingSearch
QPDoubleBlockedAgda.Auto.NarrowingSearch
QualAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
qualify 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qualifyMAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qualifyQAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
qualify_Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal
QuestionMark 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
quickCheckAgda.Utils.QuickCheck
quickCheck'Agda.Utils.QuickCheck
quickCheckAllAgda.Utils.QuickCheck
quickCheckResultAgda.Utils.QuickCheck
quickCheckWithAgda.Utils.QuickCheck
quickCheckWith'Agda.Utils.QuickCheck
quickCheckWithResultAgda.Utils.QuickCheck
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
quotedAgda.Compiler.JS.Parser
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