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

Index - P

pageAgda.Interaction.Highlighting.HTML
PageModeAgda.Utils.Pretty
Pair 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
pairwiseFilterAgda.Compiler.Epic.Interface
parallelSAgda.TypeChecking.Substitute
ParenAgda.Syntax.Concrete
parenedAgda.Compiler.JS.Parser
ParenPAgda.Syntax.Concrete
parens 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
parens'Agda.Interaction.InteractionTop
ParenVAgda.Syntax.Concrete.Operators.Parser
ParseAgda.Interaction.InteractionTop
parse 
1 (Function)Agda.Utils.ReadP
2 (Function)Agda.Compiler.JS.Parser
3 (Function)Agda.Syntax.Parser.Monad
4 (Function)Agda.Syntax.Parser
parse'Agda.Utils.ReadP
parseAndDoAtToplevelAgda.Interaction.InteractionTop
parseApplicationAgda.Syntax.Concrete.Operators
ParseError 
1 (Type/Class)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
parseErrorAgda.Syntax.Parser.Monad
parseError'Agda.Syntax.Parser.Monad
parseErrorAtAgda.Syntax.Parser.Monad
parseExpr 
1 (Function)Agda.Interaction.BasicOps
2 (Function)Agda.Interaction.CommandLine
parseExprInAgda.Interaction.BasicOps
ParseFailedAgda.Syntax.Parser.Monad
parseFileAgda.Syntax.Parser.Monad
parseFile'Agda.Syntax.Parser
ParseFlags 
1 (Type/Class)Agda.Syntax.Parser.Monad
2 (Data Constructor)Agda.Syntax.Parser.Monad
parseFlagsAgda.Syntax.Parser.Monad
parseInpAgda.Syntax.Parser.Monad
parseKeepCommentsAgda.Syntax.Parser.Monad
parseLastPosAgda.Syntax.Parser.Monad
parseLayoutAgda.Syntax.Parser.Monad
parseLexStateAgda.Syntax.Parser.Monad
parseLHSAgda.Syntax.Concrete.Operators
parseLiterateAgda.Syntax.Parser
parseModuleApplicationAgda.Syntax.Concrete.Operators
parseNameAgda.Interaction.BasicOps
ParseOkAgda.Syntax.Parser.Monad
parsePatternAgda.Syntax.Concrete.Operators
parsePatternSynAgda.Syntax.Concrete.Operators
parsePluginOptionsAgda.Interaction.Options
parsePosAgda.Syntax.Parser.Monad
parsePosString 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.Syntax.Parser
parsePragmaOptionsAgda.Interaction.Options
parsePrevCharAgda.Syntax.Parser.Monad
parsePrevTokenAgda.Syntax.Parser.Monad
Parser 
1 (Type/Class)Agda.Compiler.JS.Parser
2 (Type/Class)Agda.Syntax.Parser.Monad
3 (Type/Class)Agda.Syntax.Parser
ParseResultAgda.Syntax.Parser.Monad
parseStandardOptionsAgda.Interaction.Options
ParseStateAgda.Syntax.Parser.Monad
parseToReadsPrecAgda.Interaction.InteractionTop
parseVariablesAgda.Interaction.MakeCase
ParsingAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
PartialAgda.Interaction.Highlighting.Generate
PartialOrdAgda.Utils.PartialOrd
PartialOrderingAgda.Utils.PartialOrd
partitionMaybeAgda.Utils.List
partPAgda.Syntax.Concrete.Operators.Parser
PatAgda.Auto.Syntax
PatConAppAgda.Auto.Syntax
PatExpAgda.Auto.Syntax
PatInfoAgda.Syntax.Info
patInfoAgda.Syntax.Info
PatNameAgda.Syntax.Translation.ConcreteToAbstract
patNoRangeAgda.Syntax.Info
patOriginAgda.Syntax.Info
PatRangeAgda.Syntax.Info
patsAgda.Compiler.JS.Case
patsToElimsAgda.TypeChecking.With
PattAgda.Compiler.JS.Case
Pattern 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
3 (Type/Class)Agda.Syntax.Internal
patternAgda.Compiler.JS.Compiler
Pattern' 
1 (Type/Class)Agda.Syntax.Abstract
2 (Type/Class)Agda.Syntax.Internal
patternDepthAgda.Termination.Monad
PatternErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PatternFromAgda.TypeChecking.Rewriting.NonLinMatch
patternFromAgda.TypeChecking.Rewriting.NonLinMatch
patternNamesAgda.Syntax.Concrete
patternQNamesAgda.Syntax.Concrete
PatternsAgda.Syntax.Abstract
PatternShadowsConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
patternsToElimsAgda.Syntax.Internal.Pattern
PatternSyn 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
PatternSynDefAgda.Syntax.Abstract
PatternSynDefnAgda.Syntax.Abstract
PatternSynDefnsAgda.Syntax.Abstract
PatternSynNameAgda.Syntax.Scope.Base
PatternSynPAgda.Syntax.Abstract
PatternSynResNameAgda.Syntax.Scope.Monad
patternToExprAgda.Syntax.Abstract
patternToTermAgda.Compiler.Epic.Injection
patternVarsAgda.Syntax.Internal
patternViolationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
patternViolation'Agda.TypeChecking.MetaVars.Occurs
PatVarAgda.Auto.Syntax
PatVarNameAgda.Syntax.Internal
patVarNameToStringAgda.Syntax.Internal
PBAgda.Auto.NarrowingSearch
PBlockedAgda.Auto.NarrowingSearch
PBoundVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
pColorsAgda.Syntax.Concrete.Pretty
pconNameAgda.Compiler.MAlonzo.Primitives
PConstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PDoubleBlockedAgda.Auto.NarrowingSearch
PEConAppAgda.Auto.Typecheck
PElimsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PENoAgda.Auto.Typecheck
performedSimplificationAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
performedSimplification'Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
performKillAgda.TypeChecking.MetaVars.Occurs
PermAgda.Utils.Permutation
permPicksAgda.Utils.Permutation
permRangeAgda.Utils.Permutation
PermutationAgda.Utils.Permutation
permuteAgda.Utils.Permutation
PersistentTCStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PersistentTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PersistentVerbosityAgda.Interaction.Options.Lenses
PEvalAgda.Auto.Typecheck
pfailAgda.Utils.ReadP
PhaseAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Pi 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Internal
piAbstractTermAgda.TypeChecking.Abstract
piApplyAgda.TypeChecking.Substitute
piApply1Agda.TypeChecking.Telescope
piApplyMAgda.TypeChecking.Telescope
piApplyM'Agda.Compiler.Epic.Forcing
piBracketsAgda.Syntax.Fixity
pickidAgda.Auto.Typecheck
pickNameAgda.TypeChecking.Unquote
piFreqAgda.TypeChecking.Test.Generators
PiHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PiNotLamAgda.TypeChecking.Rules.Term
PiShAgda.TypeChecking.Rules.LHS.Unify
PLamAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
plugHoleAgda.Syntax.Internal.Pattern
Plus 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Utils
2 (Data Constructor)Agda.Syntax.Internal
plusAgda.TypeChecking.SizedTypes.Utils
PlusLevelAgda.Syntax.Internal
PnAgda.Syntax.Position
POAnyAgda.Utils.PartialOrd
POEQAgda.Utils.PartialOrd
POGEAgda.Utils.PartialOrd
POGTAgda.Utils.PartialOrd
pointerChainAgda.Syntax.Internal
Pointwise 
1 (Type/Class)Agda.Utils.PartialOrd
2 (Data Constructor)Agda.Utils.PartialOrd
pointwiseAgda.Utils.PartialOrd
PolaritiesAgda.TypeChecking.SizedTypes.Syntax
polaritiesAgda.TypeChecking.Polarity
polaritiesFromAssignmentsAgda.TypeChecking.SizedTypes.Syntax
Polarity 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
polarityAgda.TypeChecking.Polarity
PolarityAssignment 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
POLEAgda.Utils.PartialOrd
polFromCmpAgda.TypeChecking.Conversion
polFromOccAgda.TypeChecking.Polarity
POLTAgda.Utils.PartialOrd
polyQuickCheckAgda.Utils.QuickCheck
polyVerboseCheckAgda.Utils.QuickCheck
popAgda.Compiler.JS.Case
popContextAgda.Syntax.Parser.Monad
popLexStateAgda.Syntax.Parser.Monad
popMapSAgda.Auto.Convert
posColAgda.Syntax.Position
PositionAgda.Syntax.Position
Position'Agda.Syntax.Position
positionInvariantAgda.Syntax.Position
Positive 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
positiveAgda.Utils.TestHelpers
PositivityAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
positivityCheckEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
posLineAgda.Syntax.Position
posPosAgda.Syntax.Position
PossiblyAgda.TypeChecking.Rules.LHS.Unify
PostfixNotationAgda.Syntax.Notation
postfixPAgda.Syntax.Concrete.Operators.Parser
postopAgda.Syntax.Concrete.Operators.Parser
posToRangeAgda.Syntax.Position
PostponedCheckArgsAgda.Interaction.BasicOps
PostponedEquation 
1 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
2 (Data Constructor)Agda.TypeChecking.Rewriting.NonLinMatch
PostponedEquationsAgda.TypeChecking.Rewriting.NonLinMatch
PostponedTypeCheckingProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
postponeTypeCheckingProblemAgda.TypeChecking.MetaVars
postponeTypeCheckingProblem_Agda.TypeChecking.MetaVars
PostScopeState 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Postulate 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
PPiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Pragma 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Abstract
PragmaNoTerminationCheckAgda.Syntax.Concrete.Definitions
PragmaOptions 
1 (Type/Class)Agda.Interaction.Options
2 (Data Constructor)Agda.Interaction.Options
pragmaOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
PrecedenceAgda.Syntax.Fixity
PredAgda.TypeChecking.Primitive
PrefixAgda.Utils.List
prefixAgda.Compiler.JS.Compiler
PrefixDefAgda.Syntax.Common
PrefixNotationAgda.Syntax.Notation
prefixPAgda.Syntax.Concrete.Operators.Parser
PreOpAgda.Compiler.JS.Syntax
preop 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Concrete.Operators.Parser
PreOrSuffixAgda.Utils.List
preOrSuffixAgda.Utils.List
prependSAgda.TypeChecking.Substitute
PreScopeState 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PrettiesAgda.Compiler.JS.Pretty
prettiesAgda.Compiler.JS.Pretty
Pretty 
1 (Type/Class)Agda.Utils.Pretty
2 (Type/Class)Agda.Compiler.JS.Pretty
pretty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
prettyA 
1 (Function)Agda.Syntax.Abstract.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyAs 
1 (Function)Agda.Syntax.Abstract.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyATopAgda.Syntax.Abstract.Pretty
PrettyContext 
1 (Type/Class)Agda.TypeChecking.Pretty
2 (Data Constructor)Agda.TypeChecking.Pretty
prettyContextAgda.Interaction.InteractionTop
prettyEpicAgda.Compiler.Epic.Epic
prettyEpicFunAgda.Compiler.Epic.Epic
prettyErrorAgda.TypeChecking.Errors
prettyHidingAgda.Syntax.Concrete.Pretty
prettyListAgda.TypeChecking.Pretty
prettyList_Agda.TypeChecking.Pretty
prettyMapAgda.TypeChecking.CompiledClause
prettyOpAppAgda.Syntax.Concrete.Pretty
prettyPrecAgda.Utils.Pretty
prettyPrintAgda.Compiler.MAlonzo.Pretty
prettyRelevanceAgda.Syntax.Concrete.Pretty
prettyShowAgda.Utils.Pretty
PrettyTCMAgda.TypeChecking.Pretty
prettyTCMAgda.TypeChecking.Pretty
prettyTypeOfMetaAgda.Interaction.InteractionTop
PreviousInputAgda.Syntax.Parser.Alex
prFalseAgda.Compiler.Epic.Primitive
PrimAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primAgdaClauseAgda.TypeChecking.Monad.Builtin
primAgdaClauseAbsurdAgda.TypeChecking.Monad.Builtin
primAgdaClauseClauseAgda.TypeChecking.Monad.Builtin
primAgdaDataDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataConstructorAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionFunDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionPostulateAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionPrimitiveAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionRecordDefAgda.TypeChecking.Monad.Builtin
primAgdaFunDefAgda.TypeChecking.Monad.Builtin
primAgdaFunDefConAgda.TypeChecking.Monad.Builtin
primAgdaLitCharAgda.TypeChecking.Monad.Builtin
primAgdaLiteralAgda.TypeChecking.Monad.Builtin
primAgdaLitFloatAgda.TypeChecking.Monad.Builtin
primAgdaLitNatAgda.TypeChecking.Monad.Builtin
primAgdaLitQNameAgda.TypeChecking.Monad.Builtin
primAgdaLitStringAgda.TypeChecking.Monad.Builtin
primAgdaPatAbsurdAgda.TypeChecking.Monad.Builtin
primAgdaPatConAgda.TypeChecking.Monad.Builtin
primAgdaPatDotAgda.TypeChecking.Monad.Builtin
primAgdaPatLitAgda.TypeChecking.Monad.Builtin
primAgdaPatProjAgda.TypeChecking.Monad.Builtin
primAgdaPatternAgda.TypeChecking.Monad.Builtin
primAgdaPatVarAgda.TypeChecking.Monad.Builtin
primAgdaRecordDefAgda.TypeChecking.Monad.Builtin
primAgdaSortAgda.TypeChecking.Monad.Builtin
primAgdaSortLitAgda.TypeChecking.Monad.Builtin
primAgdaSortSetAgda.TypeChecking.Monad.Builtin
primAgdaSortUnsupportedAgda.TypeChecking.Monad.Builtin
primAgdaTermAgda.TypeChecking.Monad.Builtin
primAgdaTermConAgda.TypeChecking.Monad.Builtin
primAgdaTermDefAgda.TypeChecking.Monad.Builtin
primAgdaTermExtLamAgda.TypeChecking.Monad.Builtin
primAgdaTermLamAgda.TypeChecking.Monad.Builtin
primAgdaTermLitAgda.TypeChecking.Monad.Builtin
primAgdaTermPiAgda.TypeChecking.Monad.Builtin
primAgdaTermSortAgda.TypeChecking.Monad.Builtin
primAgdaTermUnsupportedAgda.TypeChecking.Monad.Builtin
primAgdaTermVarAgda.TypeChecking.Monad.Builtin
primAgdaTypeAgda.TypeChecking.Monad.Builtin
primAgdaTypeElAgda.TypeChecking.Monad.Builtin
primArgAgda.TypeChecking.Monad.Builtin
primArgArgAgda.TypeChecking.Monad.Builtin
primArgArgInfoAgda.TypeChecking.Monad.Builtin
primArgInfoAgda.TypeChecking.Monad.Builtin
primBodyAgda.Compiler.MAlonzo.Primitives
primBoolAgda.TypeChecking.Monad.Builtin
primCharAgda.TypeChecking.Monad.Builtin
primClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primConsAgda.TypeChecking.Monad.Builtin
primDataConstructorsAgda.TypeChecking.Primitive
PrimeAgda.Utils.Suffix
primEqualityAgda.TypeChecking.Monad.Builtin
primEqualityNameAgda.TypeChecking.Monad.Builtin
primExprAgda.Compiler.Epic.Primitive
primFalseAgda.TypeChecking.Monad.Builtin
primFlatAgda.TypeChecking.Monad.Builtin
primFloatAgda.TypeChecking.Monad.Builtin
PrimFun 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunAgda.Compiler.Epic.Primitive
primFunArityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunImplementationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primHiddenAgda.TypeChecking.Monad.Builtin
primHidingAgda.TypeChecking.Monad.Builtin
PrimImplAgda.TypeChecking.Primitive
primInfAgda.TypeChecking.Monad.Builtin
primInstanceAgda.TypeChecking.Monad.Builtin
primIntegerAgda.TypeChecking.Monad.Builtin
primIOAgda.TypeChecking.Monad.Builtin
primIrrAxiomAgda.TypeChecking.Monad.Builtin
primIrrelevantAgda.TypeChecking.Monad.Builtin
Primitive 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.Syntax.Abstract
4 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PrimitiveFunctionAgda.Syntax.Concrete.Definitions
primitiveFunctionsAgda.TypeChecking.Primitive
PrimitiveImplAgda.TypeChecking.Primitive
PrimitiveTypeAgda.Interaction.Highlighting.Precise
primitiviseAgda.Compiler.Epic.Primitive
primLevelAgda.TypeChecking.Monad.Builtin
primLevelMaxAgda.TypeChecking.Monad.Builtin
primLevelSucAgda.TypeChecking.Monad.Builtin
primLevelZeroAgda.TypeChecking.Monad.Builtin
primListAgda.TypeChecking.Monad.Builtin
primNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primNatAgda.TypeChecking.Monad.Builtin
primNatCaseZDAgda.Compiler.Epic.Primitive
primNatCaseZSAgda.Compiler.Epic.Primitive
primNatDivSucAuxAgda.TypeChecking.Monad.Builtin
primNatEqualityAgda.TypeChecking.Monad.Builtin
primNatLessAgda.TypeChecking.Monad.Builtin
primNatMinusAgda.TypeChecking.Monad.Builtin
primNatModSucAuxAgda.TypeChecking.Monad.Builtin
primNatPlusAgda.TypeChecking.Monad.Builtin
primNatTimesAgda.TypeChecking.Monad.Builtin
primNilAgda.TypeChecking.Monad.Builtin
primQNameAgda.TypeChecking.Monad.Builtin
primQNameDefinitionAgda.TypeChecking.Primitive
primQNameTypeAgda.TypeChecking.Primitive
primReflAgda.TypeChecking.Monad.Builtin
primRelevanceAgda.TypeChecking.Monad.Builtin
primRelevantAgda.TypeChecking.Monad.Builtin
primRewriteAgda.TypeChecking.Monad.Builtin
primSharpAgda.TypeChecking.Monad.Builtin
primSizeAgda.TypeChecking.Monad.Builtin
primSizeInfAgda.TypeChecking.Monad.Builtin
primSizeLtAgda.TypeChecking.Monad.Builtin
primSizeMaxAgda.TypeChecking.Monad.Builtin
primSizeSucAgda.TypeChecking.Monad.Builtin
primSizeUnivAgda.TypeChecking.Monad.Builtin
primStringAgda.TypeChecking.Monad.Builtin
primSucAgda.TypeChecking.Monad.Builtin
PrimTagAgda.Compiler.Epic.Interface
PrimTermAgda.TypeChecking.Primitive
primTermAgda.TypeChecking.Primitive
PrimTFAgda.Compiler.Epic.Primitive
PrimTransformAgda.Compiler.Epic.Primitive
primTrueAgda.TypeChecking.Monad.Builtin
primTrustMeAgda.TypeChecking.Primitive
PrimTypeAgda.TypeChecking.Primitive
primTypeAgda.TypeChecking.Primitive
primVisibleAgda.TypeChecking.Monad.Builtin
primZeroAgda.TypeChecking.Monad.Builtin
printAgda.TypeChecking.Monad.Benchmark
printErrorInfoAgda.Interaction.Highlighting.Generate
printHighlightingInfoAgda.Interaction.Highlighting.Generate
PrintRange 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
printScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
printStatisticsAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
printTestCaseAgda.Utils.QuickCheck
printUnsolvedInfoAgda.Interaction.Highlighting.Generate
printUsageAgda.Main
printVersionAgda.Main
PrioAgda.Auto.NarrowingSearch
prioAbsurdLambdaAgda.Auto.SearchControl
prioCompareArgListAgda.Auto.SearchControl
prioCompBetaAgda.Auto.SearchControl
prioCompBetaStructuredAgda.Auto.SearchControl
prioCompChoiceAgda.Auto.SearchControl
prioCompCopyAgda.Auto.SearchControl
prioCompIotaAgda.Auto.SearchControl
prioCompUnifAgda.Auto.SearchControl
prioInferredTypeUnknownAgda.Auto.SearchControl
PrioMeta 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
prioNoAgda.Auto.SearchControl
prioNoIotaAgda.Auto.SearchControl
prioProjIndexAgda.Auto.SearchControl
prioTypecheckAgda.Auto.SearchControl
prioTypecheckArgListAgda.Auto.SearchControl
prioTypeUnknownAgda.Auto.SearchControl
PrivateAgda.Syntax.Concrete
PrivateAccessAgda.Syntax.Common
PrivateNSAgda.Syntax.Scope.Base
prNatEqualityAgda.Compiler.Epic.Primitive
Problem 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
Problem'Agda.TypeChecking.Rules.LHS.Problem
ProblemConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
problemFromPatsAgda.TypeChecking.Rules.LHS.ProblemRest
ProblemId 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
problemInPatAgda.TypeChecking.Rules.LHS.Problem
problemOutPatAgda.TypeChecking.Rules.LHS.Problem
ProblemPartAgda.TypeChecking.Rules.LHS.Problem
ProblemRest 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
problemRestAgda.TypeChecking.Rules.LHS.Problem
problemTelAgda.TypeChecking.Rules.LHS.Problem
problemTypeAgda.TypeChecking.MetaVars
Proj 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Internal
projArgInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
projCaseAgda.TypeChecking.CompiledClause
ProjDBPAgda.Termination.Monad
projDropParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ProjectedVarAgda.TypeChecking.MetaVars
Projection 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
projectionArgsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ProjectionLikenessAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
projectionMismatchAgda.TypeChecking.Rules.LHS.Unify
ProjectionReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ProjectionView 
1 (Type/Class)Agda.TypeChecking.ProjectionLike
2 (Data Constructor)Agda.TypeChecking.ProjectionLike
ProjectRootAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
projectRootAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
projectTypedAgda.TypeChecking.Records
projFreqAgda.TypeChecking.Test.Generators
projFromTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
projIndexAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ProjMPAgda.TypeChecking.Coverage.Match
ProjName 
1 (Type/Class)Agda.TypeChecking.Test.Generators
2 (Data Constructor)Agda.TypeChecking.Test.Generators
ProjPAgda.Syntax.Internal
projPatternsAgda.TypeChecking.CompiledClause
projProperAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
projUseSizeLtAgda.Termination.Monad
ProjVarExc 
1 (Type/Class)Agda.TypeChecking.MetaVars
2 (Data Constructor)Agda.TypeChecking.MetaVars
projViewAgda.TypeChecking.ProjectionLike
projViewProjAgda.TypeChecking.ProjectionLike
projViewSelfAgda.TypeChecking.ProjectionLike
projViewSpineAgda.TypeChecking.ProjectionLike
proofIrrelevanceAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Prop 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Internal
propagatePrioAgda.Auto.NarrowingSearch
propAssociativeAgda.TypeChecking.SizedTypes.Tests
propBoundedSemiLatticeAgda.TypeChecking.SizedTypes.Tests
propCommutativeAgda.TypeChecking.SizedTypes.Tests
propDioidAgda.TypeChecking.SizedTypes.Tests
propDioid_GenAgda.TypeChecking.SizedTypes.Tests
propDistLAgda.TypeChecking.SizedTypes.Tests
propDistRAgda.TypeChecking.SizedTypes.Tests
propDistributiveAgda.TypeChecking.SizedTypes.Tests
properlyMatchingAgda.Syntax.Internal
properSplitAgda.TypeChecking.CompiledClause.Compile
PropertyAgda.Utils.QuickCheck
propertyAgda.Utils.QuickCheck
property_not_null_singletonAgda.Utils.Favorites
property_null_emptyAgda.Utils.Favorites
property_seqPOAgda.Utils.PartialOrd
propFreqAgda.TypeChecking.Test.Generators
propIdempotentAgda.TypeChecking.SizedTypes.Tests
propMonoidAgda.TypeChecking.SizedTypes.Tests
PropMustBeSingletonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
propSemiLatticeAgda.TypeChecking.SizedTypes.Tests
propUnitAgda.TypeChecking.SizedTypes.Tests
propZeroAgda.TypeChecking.SizedTypes.Tests
prop_associative_orPOAgda.Utils.PartialOrd
prop_associative_seqPOAgda.Utils.PartialOrd
prop_BiMap_invariantAgda.Utils.BiMap
prop_BoundedSemiLattice_LabelAgda.TypeChecking.SizedTypes.Tests
prop_commonPrefixAgda.Utils.List
prop_commonSuffixAgda.Utils.List
prop_commutative_orPOAgda.Utils.PartialOrd
prop_commutative_seqPOAgda.Utils.PartialOrd
prop_comparable_PartialOrderingAgda.Utils.PartialOrd
prop_comparable_relatedAgda.Utils.PartialOrd
prop_compareWithFavoritesAgda.Utils.Favorites
prop_ComposeCompleteAgda.TypeChecking.SizedTypes.Tests
prop_ComposeSoundAgda.TypeChecking.SizedTypes.Tests
prop_count_emptyAgda.Utils.Bag
prop_count_insertAgda.Utils.Bag
prop_count_singletonAgda.Utils.Bag
prop_Dioid_LabelAgda.TypeChecking.SizedTypes.Tests
prop_Dioid_WeightAgda.TypeChecking.SizedTypes.Tests
prop_disjointAgda.Utils.Warshall
prop_distinct_fastDistinctAgda.Utils.List
prop_DistL_LabelAgda.TypeChecking.SizedTypes.Tests
prop_distributive_seqPO_orPOAgda.Utils.PartialOrd
prop_DistR_LabelAgda.TypeChecking.SizedTypes.Tests
prop_Dist_LabelAgda.TypeChecking.SizedTypes.Tests
prop_extractNthElementAgda.Utils.List
prop_flattenTelInvAgda.TypeChecking.Tests
prop_flattenTelScopeAgda.TypeChecking.Tests
prop_fromList_after_toListAgda.Utils.Favorites
prop_fromList_toListAgda.Utils.Bag
prop_fromOrderings_after_toOrderingsAgda.Utils.PartialOrd
prop_galoisAgda.TypeChecking.Irrelevance
prop_genericElemIndexAgda.Utils.List
prop_groupBy'Agda.Utils.List
prop_idempotent_orPOAgda.Utils.PartialOrd
prop_idempotent_seqPOAgda.Utils.PartialOrd
prop_identity_seqPOAgda.Utils.PartialOrd
prop_keys_fromListAgda.Utils.Bag
prop_leqPO_soundAgda.Utils.PartialOrd
prop_map_composeAgda.Utils.Bag
prop_map_idAgda.Utils.Bag
prop_MeetCompleteAgda.TypeChecking.SizedTypes.Tests
prop_MeetSoundAgda.TypeChecking.SizedTypes.Tests
prop_Monoid_LabelAgda.TypeChecking.SizedTypes.Tests
prop_nonempty_groupsAgda.Utils.Bag
prop_Occurrence_distributiveAgda.TypeChecking.Positivity.Occurrence
prop_Occurrence_oplus_associativeAgda.TypeChecking.Positivity.Occurrence
prop_Occurrence_oplus_commutativeAgda.TypeChecking.Positivity.Occurrence
prop_Occurrence_oplus_ozeroAgda.TypeChecking.Positivity.Occurrence
prop_Occurrence_ostarAgda.TypeChecking.Positivity.Occurrence
prop_Occurrence_otimes_associativeAgda.TypeChecking.Positivity.Occurrence
prop_Occurrence_otimes_ooneAgda.TypeChecking.Positivity.Occurrence
prop_Occurrence_otimes_ozeroAgda.TypeChecking.Positivity.Occurrence
prop_oplus_Occurrence_EdgeAgda.TypeChecking.Positivity.Tests
prop_oppPOAgda.Utils.PartialOrd
prop_orPO_soundAgda.Utils.PartialOrd
prop_pathAgda.Utils.Warshall
prop_related_pairAgda.Utils.PartialOrd
prop_reorderTelStableAgda.TypeChecking.Tests
prop_SemiLattice_LabelAgda.TypeChecking.SizedTypes.Tests
prop_seqPOAgda.Utils.PartialOrd
prop_size_fromListAgda.Utils.Bag
prop_size_unionAgda.Utils.Bag
prop_smallerAgda.Utils.Warshall
prop_sorted_toOrderingsAgda.Utils.PartialOrd
prop_splitTelescopePermScopeAgda.TypeChecking.Tests
prop_splitTelescopeScopeAgda.TypeChecking.Tests
prop_stableAgda.Utils.Warshall
prop_telToListInvAgda.TypeChecking.Tests
prop_toList_fromListAgda.Utils.Bag
prop_toOrderings_after_fromOrderingAgda.Utils.PartialOrd
prop_toOrderings_after_fromOrderingsAgda.Utils.PartialOrd
prop_traverse_idAgda.Utils.Bag
prop_union_union2Agda.Utils.Favorites
prop_uniqOnAgda.Utils.List
prop_Unit_LabelAgda.TypeChecking.SizedTypes.Tests
prop_updateAtAgda.Utils.List
prop_updateHeadAgda.Utils.List
prop_updateLastAgda.Utils.List
prop_wellScopedVarsAgda.TypeChecking.Test.Generators
prop_Zero_LabelAgda.TypeChecking.SizedTypes.Tests
prop_zero_orPOAgda.Utils.PartialOrd
prop_zero_seqPOAgda.Utils.PartialOrd
prop_zipWith'Agda.Utils.List
prPredAgda.Compiler.Epic.Primitive
prSucAgda.Compiler.Epic.Primitive
prTrueAgda.Compiler.Epic.Primitive
pruneAgda.TypeChecking.MetaVars.Occurs
PrunedEverythingAgda.TypeChecking.MetaVars.Occurs
PrunedNothingAgda.TypeChecking.MetaVars.Occurs
PrunedSomethingAgda.TypeChecking.MetaVars.Occurs
PruneResultAgda.TypeChecking.MetaVars.Occurs
prZeroAgda.Compiler.Epic.Primitive
PStateAgda.Syntax.Parser.Monad
PStrAgda.Utils.Pretty
PTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ptextAgda.Utils.Pretty
PtrAgda.Utils.Pointer, Agda.Syntax.Internal
ptsAgda.TypeChecking.Substitute
ptsRuleAgda.TypeChecking.Rules.Term
PublicAccessAgda.Syntax.Common
publicModulesAgda.Syntax.Scope.Base
PublicNSAgda.Syntax.Scope.Base
publicOpenAgda.Syntax.Concrete
punctAgda.Compiler.JS.Parser
punctuate 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
pureTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
purgeNonvariantAgda.TypeChecking.Polarity
pushContextAgda.Syntax.Parser.Monad
pushCurrentContextAgda.Syntax.Parser.Monad
pushLexStateAgda.Syntax.Parser.Monad
putAllConstraintsToSleepAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
putAllowedReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
putBenchmarkAgda.Utils.Benchmark
putConArityAgda.Compiler.Epic.CompileState
putConstrTagAgda.Compiler.Epic.CompileState
putDelayedAgda.Compiler.Epic.CompileState
putForcedArgsAgda.Compiler.Epic.CompileState
putIncludeDirsAgda.Interaction.Options.Lenses
putMainAgda.Compiler.Epic.CompileState
putPersistentVerbosityAgda.Interaction.Options.Lenses
putResponse 
1 (Function)Agda.Interaction.EmacsCommand
2 (Function)Agda.Interaction.InteractionTop
putSafeModeAgda.Interaction.Options.Lenses
putVerbosityAgda.Interaction.Options.Lenses
PVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PWildAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
pwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty