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

P64ToI	Agda.Syntax.Treeless, Agda.Compiler.Backend
packUnquoteM	Agda.TypeChecking.Unquote
PAdd	Agda.Syntax.Treeless, Agda.Compiler.Backend
PAdd64	Agda.Syntax.Treeless, Agda.Compiler.Backend
page	Agda.Interaction.Highlighting.HTML
PageMode	Agda.Utils.Pretty
PApp	Agda.Utils.Haskell.Syntax
parallelS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Paren	Agda.Syntax.Concrete
ParenP	Agda.Syntax.Concrete
ParenPreference	Agda.Syntax.Fixity
parens
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
parens'	Agda.Interaction.InteractionTop
ParenV	Agda.Syntax.Concrete.Operators.Parser
Parse	Agda.Interaction.InteractionTop
parse
1 (Function)	Agda.Utils.Parser.ReadP
2 (Function)	Agda.Utils.Parser.MemoisedCPS
3 (Function)	Agda.Syntax.Concrete.Operators.Parser.Monad
4 (Function)	Agda.Syntax.Parser.Monad
5 (Function)	Agda.Syntax.Concrete.Operators.Parser
6 (Function)	Agda.Syntax.Parser
parse'	Agda.Utils.Parser.ReadP
parseAndDoAtToplevel	Agda.Interaction.InteractionTop
parseApplication	Agda.Syntax.Concrete.Operators
parseArgs	Agda.Auto.Options
parseBackendOptions	Agda.Compiler.Backend
ParseError
1 (Type/Class)	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor)	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
parseError	Agda.Syntax.Parser.Monad
parseError'	Agda.Syntax.Parser.Monad
parseErrorAt	Agda.Syntax.Parser.Monad
parseErrorRange	Agda.Syntax.Parser.Monad
parseExpr
1 (Function)	Agda.Interaction.BasicOps
2 (Function)	Agda.Interaction.CommandLine
parseExprIn	Agda.Interaction.BasicOps
ParseFailed	Agda.Syntax.Parser.Monad
parseFile	Agda.Syntax.Parser
ParseFlags
1 (Type/Class)	Agda.Syntax.Parser.Monad
2 (Data Constructor)	Agda.Syntax.Parser.Monad
parseFlags	Agda.Syntax.Parser.Monad
parseFromSrc	Agda.Syntax.Parser.Monad
parseHaskellPragma	Agda.Compiler.MAlonzo.Pragmas
parseIdiomBrackets	Agda.Syntax.IdiomBrackets
parseInp	Agda.Syntax.Parser.Monad
parseKeepComments	Agda.Syntax.Parser.Monad
parseLastPos	Agda.Syntax.Parser.Monad
parseLayout	Agda.Syntax.Parser.Monad
parseLexState	Agda.Syntax.Parser.Monad
parseLHS	Agda.Syntax.Concrete.Operators
parseLibFile	Agda.Interaction.Library.Parse
parseModuleApplication	Agda.Syntax.Concrete.Operators
parseName	Agda.Interaction.BasicOps
ParseOk	Agda.Syntax.Parser.Monad
parsePattern	Agda.Syntax.Concrete.Operators
parsePatternSyn	Agda.Syntax.Concrete.Operators
parsePluginOptions	Agda.Interaction.Options
parsePos	Agda.Syntax.Parser.Monad
parsePosString
1 (Function)	Agda.Syntax.Parser.Monad
2 (Function)	Agda.Syntax.Parser
parsePragma	Agda.Compiler.MAlonzo.Pragmas
parsePragmaOptions	Agda.Interaction.Options
parsePrevChar	Agda.Syntax.Parser.Monad
parsePrevToken	Agda.Syntax.Parser.Monad
Parser
1 (Type/Class)	Agda.Utils.Parser.MemoisedCPS
2 (Type/Class)	Agda.Syntax.Concrete.Operators.Parser.Monad
3 (Type/Class)	Agda.Syntax.Parser.Monad
4 (Type/Class)	Agda.Syntax.Parser
parserBased	Agda.Interaction.Highlighting.Precise
ParserClass	Agda.Utils.Parser.MemoisedCPS
ParseResult	Agda.Syntax.Parser.Monad
ParserWithGrammar	Agda.Utils.Parser.MemoisedCPS
ParseSections
1 (Type/Class)	Agda.Syntax.Concrete.Operators.Parser
2 (Data Constructor)	Agda.Syntax.Concrete.Operators.Parser
parseSrcFile	Agda.Syntax.Parser.Monad
ParseState	Agda.Syntax.Parser.Monad
parseTime	Agda.Auto.Options
parseToReadsPrec	Agda.Interaction.InteractionTop
parseVariables	Agda.Interaction.MakeCase
parseVerboseKey	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ParseWarning
1 (Type/Class)	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
parseWarningName	Agda.Syntax.Parser.Monad
Parsing	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Partial	Agda.Interaction.Highlighting.Generate
PartialOrd	Agda.Utils.PartialOrd
PartialOrdering	Agda.Utils.PartialOrd
partition3	Agda.Utils.Three
partitionByKindOfForeignCode	Agda.Compiler.MAlonzo.Pragmas
partitionEithers3	Agda.Utils.Three
partitionM	Agda.Utils.Monad
partitionMaybe	Agda.Utils.List
partP	Agda.Syntax.Concrete.Operators.Parser
PAsPat	Agda.Utils.Haskell.Syntax
Pat
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Type/Class)	Agda.Auto.Syntax
PatConApp	Agda.Auto.Syntax
PatExp	Agda.Auto.Syntax
path	Agda.TypeChecking.Primitive
PathCons	Agda.TypeChecking.Rules.Data
pathLevel	Agda.Syntax.Internal
pathLhs	Agda.Syntax.Internal
pathName	Agda.Syntax.Internal
pathRhs	Agda.Syntax.Internal
pathSort	Agda.Syntax.Internal
PathType	Agda.Syntax.Internal
pathType	Agda.Syntax.Internal
pathUnview	Agda.TypeChecking.Monad.Builtin
PathView	Agda.Syntax.Internal
pathView	Agda.TypeChecking.Monad.Builtin
pathView'	Agda.TypeChecking.Monad.Builtin
pathViewAsPi	Agda.TypeChecking.Telescope
pathViewAsPi'	Agda.TypeChecking.Telescope
pathViewAsPi'whnf	Agda.TypeChecking.Telescope
PatInfo	Agda.Syntax.Info
patInfo	Agda.Syntax.Info
patLazy	Agda.Syntax.Info
PatName	Agda.Syntax.Translation.ConcreteToAbstract
patNoRange	Agda.Syntax.Info
PatOAbsurd	Agda.Syntax.Internal
PatOCon	Agda.Syntax.Internal
PatODot	Agda.Syntax.Internal
PatOLit	Agda.Syntax.Internal
PatORec	Agda.Syntax.Internal
PatOrigin	Agda.Syntax.Internal
patOrigin	Agda.Syntax.Info
PatOSplit	Agda.Syntax.Internal
PatOSystem	Agda.Syntax.Internal
PatOVar	Agda.Syntax.Internal
PatOWild	Agda.Syntax.Internal
PatRange	Agda.Syntax.Info
patsToElims	Agda.TypeChecking.With
PatSyn	Agda.Utils.Haskell.Syntax
Pattern
1 (Type/Class)	Agda.Syntax.Reflected
2 (Type/Class)	Agda.Syntax.Concrete
3 (Type/Class)	Agda.Syntax.Internal
4 (Type/Class)	Agda.Syntax.Abstract
Pattern'
1 (Type/Class)	Agda.Syntax.Internal
2 (Type/Class)	Agda.Syntax.Abstract
PatternBound	Agda.Syntax.Scope.Base
patternDepth	Agda.Termination.Monad
PatternErr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternFrom	Agda.TypeChecking.Rewriting.NonLinMatch
patternFrom	Agda.TypeChecking.Rewriting.NonLinMatch
PatternLike	Agda.Syntax.Internal.Pattern
patternNames	Agda.Syntax.Concrete.Pattern
patternOrigin	Agda.Syntax.Internal
patternQNames	Agda.Syntax.Concrete.Pattern
Patterns	Agda.Syntax.Abstract
PatternShadowsConstructor	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
patternsToElims	Agda.Syntax.Internal.Pattern
PatternSubstitution	Agda.Syntax.Internal
PatternSyn
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
PatternSynDef	Agda.Syntax.Abstract
PatternSynDefn	Agda.Syntax.Abstract
PatternSynDefns	Agda.Syntax.Abstract
PatternSynName	Agda.Syntax.Scope.Base
PatternSynP	Agda.Syntax.Abstract
PatternSynResName	Agda.Syntax.Scope.Base
patternToElim	Agda.Syntax.Internal.Pattern
patternToExpr	Agda.Syntax.Abstract
patternToModuleBound	Agda.Syntax.Scope.Base
patternToTerm	Agda.Syntax.Internal.Pattern
PatternVarModalities	Agda.Syntax.Internal.Pattern
patternVarModalities	Agda.Syntax.Internal.Pattern
PatternVars	Agda.Syntax.Internal
patternVars
1 (Function)	Agda.Syntax.Internal
2 (Function)	Agda.Syntax.Abstract.Pattern
patternViolation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
patternViolation'	Agda.TypeChecking.MetaVars.Occurs
PatTypeSig	Agda.Utils.Haskell.Syntax
PatVar	Agda.Auto.Syntax
PatVarName	Agda.Syntax.Internal
patVarNameToString	Agda.Syntax.Internal
PB	Agda.Auto.NarrowingSearch
PBangPat	Agda.Utils.Haskell.Syntax
PBlocked	Agda.Auto.NarrowingSearch
PBoundVar	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pconName	Agda.Compiler.MAlonzo.Primitives
PConstr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pDom	Agda.Syntax.Internal
PDoubleBlocked	Agda.Auto.NarrowingSearch
PEConApp	Agda.Auto.Typecheck
PElims	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PENo	Agda.Auto.Typecheck
PEq64	Agda.Syntax.Treeless, Agda.Compiler.Backend
PEqC	Agda.Syntax.Treeless, Agda.Compiler.Backend
PEqF	Agda.Syntax.Treeless, Agda.Compiler.Backend
PEqI	Agda.Syntax.Treeless, Agda.Compiler.Backend
PEqQ	Agda.Syntax.Treeless, Agda.Compiler.Backend
PEqS	Agda.Syntax.Treeless, Agda.Compiler.Backend
performedSimplification	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
performedSimplification'	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
performKill	Agda.TypeChecking.MetaVars.Occurs
Perm	Agda.Utils.Permutation
permPicks	Agda.Utils.Permutation
permRange	Agda.Utils.Permutation
Permutation	Agda.Utils.Permutation
permute	Agda.Utils.Permutation
permuteTel	Agda.TypeChecking.Telescope
PersistentTCSt	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PersistentTCState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PersistentVerbosity	Agda.Interaction.Options.Lenses
PEval	Agda.Auto.Typecheck
pfail	Agda.Utils.Parser.ReadP
PGeq	Agda.Syntax.Treeless, Agda.Compiler.Backend
Phase	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Pi
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Reflected
3 (Data Constructor)	Agda.Syntax.Concrete
4 (Data Constructor)	Agda.Syntax.Internal
5 (Data Constructor)	Agda.Syntax.Abstract
piAbstract	Agda.TypeChecking.Abstract
piAbstractTerm	Agda.TypeChecking.Abstract
piApply	Agda.TypeChecking.Substitute
PiApplyM	Agda.TypeChecking.Telescope
piApplyM	Agda.TypeChecking.Telescope
piBrackets	Agda.Syntax.Fixity
pickid	Agda.Auto.Typecheck
pickName	Agda.TypeChecking.Unquote
pickUid	Agda.Auto.SearchControl
PIf	Agda.Syntax.Treeless, Agda.Compiler.Backend
PiHead	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PiNotLam	Agda.TypeChecking.Rules.Term
piOrPath	Agda.TypeChecking.Telescope
PIrrPat	Agda.Utils.Haskell.Syntax
PiSort	Agda.Syntax.Internal
piSort	Agda.TypeChecking.Substitute
piSort'	Agda.TypeChecking.Substitute
PITo64	Agda.Syntax.Treeless, Agda.Compiler.Backend
Placeholder	Agda.Syntax.Common
placeholder	Agda.Syntax.Concrete.Operators.Parser
PlainJS	Agda.Compiler.JS.Syntax
PLam	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PLit	Agda.Utils.Haskell.Syntax
PLt	Agda.Syntax.Treeless, Agda.Compiler.Backend
PLt64	Agda.Syntax.Treeless, Agda.Compiler.Backend
plugHole	Agda.Utils.Zipper
Plus
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Utils
2 (Data Constructor)	Agda.Syntax.Internal
plus	Agda.TypeChecking.SizedTypes.Utils
plusKView	Agda.Syntax.Treeless, Agda.Compiler.Backend
PlusLevel	Agda.Syntax.Internal
PM
1 (Type/Class)	Agda.Syntax.Parser
2 (Data Constructor)	Agda.Syntax.Parser
PMul	Agda.Syntax.Treeless, Agda.Compiler.Backend
PMul64	Agda.Syntax.Treeless, Agda.Compiler.Backend
Pn	Agda.Syntax.Position
POAny	Agda.Utils.PartialOrd
POEQ	Agda.Utils.PartialOrd
POGE	Agda.Utils.PartialOrd
POGT	Agda.Utils.PartialOrd
PointCons	Agda.TypeChecking.Rules.Data
Pointwise
1 (Type/Class)	Agda.Utils.PartialOrd
2 (Data Constructor)	Agda.Utils.PartialOrd
pointwise	Agda.Utils.PartialOrd
Polarities
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)	Agda.Syntax.Concrete.Fixity
polarities	Agda.TypeChecking.Polarity
polaritiesFromAssignments	Agda.TypeChecking.SizedTypes.Syntax
Polarity
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
polarity	Agda.TypeChecking.Polarity
PolarityAssignment
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor)	Agda.TypeChecking.SizedTypes.Syntax
polarityFromPositivity	Agda.TypeChecking.Polarity
PolarityPragma	Agda.Syntax.Concrete
PolarityPragmasButNotPostulates	Agda.Syntax.Concrete.Definitions
PolarityPragmasButNotPostulates_	Agda.Interaction.Options.Warnings
POLE	Agda.Utils.PartialOrd
polFromCmp	Agda.TypeChecking.Conversion
polFromOcc	Agda.TypeChecking.Polarity
POLT	Agda.Utils.PartialOrd
POMonoid	Agda.Utils.POMonoid
popContext	Agda.Syntax.Parser.Monad
popLexState	Agda.Syntax.Parser.Monad
popMapS	Agda.Auto.Convert
posCol	Agda.Syntax.Position
POSemigroup	Agda.Utils.POMonoid
Position	Agda.Syntax.Position
Position'	Agda.Syntax.Position
PositionInName	Agda.Syntax.Common
positionInvariant	Agda.Syntax.Position
PositionWithoutFile	Agda.Syntax.Position
Positivity	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
PositivityCheck	Agda.Syntax.Common
positivityCheckEnabled	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PositivityProblem	Agda.Interaction.Highlighting.Precise
posLine	Agda.Syntax.Position
posPos	Agda.Syntax.Position
Post	Agda.Syntax.Concrete.Operators.Parser
postAction	Agda.TypeChecking.CheckInternal
postCompile	Agda.Compiler.Backend
PostfixNotation	Agda.Syntax.Notation
PostLeftsK	Agda.Syntax.Concrete.Operators.Parser.Monad
postModule	Agda.Compiler.Backend
posToInterval	Agda.Syntax.Position
posToRange	Agda.Syntax.Position
posToRange'	Agda.Syntax.Position
PostponedCheckArgs	Agda.Interaction.BasicOps
PostponedCheckFunDef	Agda.Interaction.BasicOps
PostponedEquation
1 (Type/Class)	Agda.TypeChecking.Rewriting.NonLinMatch
2 (Data Constructor)	Agda.TypeChecking.Rewriting.NonLinMatch
PostponedEquations	Agda.TypeChecking.Rewriting.NonLinMatch
PostponedTypeCheckingProblem	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
postponeInstanceConstraints	Agda.TypeChecking.InstanceArguments
postponeTypeCheckingProblem	Agda.TypeChecking.MetaVars
postponeTypeCheckingProblem_	Agda.TypeChecking.MetaVars
PostScopeState
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
postscript	Agda.Compiler.JS.Syntax
postTraverseAPatternM	Agda.Syntax.Abstract.Pattern
postTraverseCPatternM	Agda.Syntax.Concrete.Pattern
postTraversePatternM	Agda.Syntax.Internal.Pattern
Postulate
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Interaction.Highlighting.Precise
PPi	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pPi'	Agda.TypeChecking.Primitive
PQuot	Agda.Syntax.Treeless, Agda.Compiler.Backend
PQuot64	Agda.Syntax.Treeless, Agda.Compiler.Backend
Pragma
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Interaction.Highlighting.Precise
4 (Type/Class)	Agda.Syntax.Abstract
5 (Data Constructor)	Agda.Syntax.Abstract
PragmaCompiled	Agda.Syntax.Concrete.Definitions
PragmaCompiled_	Agda.Interaction.Options.Warnings
PragmaNoTerminationCheck	Agda.Syntax.Concrete.Definitions
PragmaNoTerminationCheck_	Agda.Interaction.Options.Warnings
PragmaOptions
1 (Type/Class)	Agda.Interaction.Options
2 (Data Constructor)	Agda.Interaction.Options
pragmaOptions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Pragmas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Pre	Agda.Syntax.Concrete.Operators.Parser
preAction	Agda.TypeChecking.CheckInternal
Precedence	Agda.Syntax.Fixity
PrecedenceLevel	Agda.Syntax.Fixity
PrecedenceStack	Agda.Syntax.Fixity
preCompile	Agda.Compiler.Backend
precomputedFreeVars	Agda.TypeChecking.Free.Precompute
PrecomputeFreeVars	Agda.TypeChecking.Free.Precompute
precomputeFreeVars	Agda.TypeChecking.Free.Precompute
precomputeFreeVars_	Agda.TypeChecking.Free.Precompute
pRecord	Agda.Syntax.Concrete.Pretty
Pred	Agda.TypeChecking.Primitive
PreferParen	Agda.Syntax.Fixity
preferParen	Agda.Syntax.Fixity
PreferParenless	Agda.Syntax.Fixity
preferParenless	Agda.Syntax.Fixity
Prefix	Agda.Utils.List
prefix	Agda.Compiler.JS.Compiler
PrefixDef	Agda.Syntax.Common
PrefixNotation	Agda.Syntax.Notation
PRem	Agda.Syntax.Treeless, Agda.Compiler.Backend
PRem64	Agda.Syntax.Treeless, Agda.Compiler.Backend
preModule	Agda.Compiler.Backend
PreOp	Agda.Compiler.JS.Syntax
prependS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
preprocess	Agda.TypeChecking.Positivity
PreRightsK	Agda.Syntax.Concrete.Operators.Parser.Monad
PreScopeState
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
preserveInteractionIds	Agda.Syntax.Translation.AbstractToConcrete
preTraverseAPatternM	Agda.Syntax.Abstract.Pattern
preTraverseCPatternM	Agda.Syntax.Concrete.Pattern
preTraversePatternM	Agda.Syntax.Internal.Pattern
Pretties	Agda.Compiler.JS.Pretty
pretties	Agda.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
prettyATop	Agda.Syntax.Abstract.Pretty
PrettyContext
1 (Type/Class)	Agda.TypeChecking.Pretty
2 (Data Constructor)	Agda.TypeChecking.Pretty
prettyContext	Agda.Interaction.InteractionTop
prettyError	Agda.TypeChecking.Errors
prettyGuardedRhs	Agda.Compiler.MAlonzo.Pretty
prettyHiding	Agda.Syntax.Concrete.Pretty
prettyList
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
prettyList_
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
prettyMap	Agda.TypeChecking.CompiledClause
prettyNameSpace	Agda.Syntax.Scope.Base
prettyOpApp	Agda.Syntax.Concrete.Pretty
prettyPrec	Agda.Utils.Pretty
prettyPrint	Agda.Compiler.MAlonzo.Pretty
prettyQName	Agda.Compiler.MAlonzo.Pretty
prettyRelevance	Agda.Syntax.Concrete.Pretty
prettyRhs	Agda.Compiler.MAlonzo.Pretty
prettyShow	Agda.Utils.Pretty
PrettyTCM	Agda.TypeChecking.Pretty
prettyTCM	Agda.TypeChecking.Pretty
prettyTCMCtx	Agda.TypeChecking.Pretty
prettyTCMPatternList	Agda.TypeChecking.Pretty
prettyTCMPatterns	Agda.TypeChecking.Pretty
prettyTCWarnings	Agda.TypeChecking.Errors
prettyTCWarnings'	Agda.TypeChecking.Errors
prettyTypeOfMeta	Agda.Interaction.InteractionTop
prettyWarning	Agda.TypeChecking.Errors
prettyWhere	Agda.Compiler.MAlonzo.Pretty
PreviousInput	Agda.Syntax.Parser.Alex
Prim	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbs	Agda.TypeChecking.Monad.Builtin
primAbsAbs	Agda.TypeChecking.Monad.Builtin
primAbstr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClause	Agda.TypeChecking.Monad.Builtin
primAgdaClauseAbsurd	Agda.TypeChecking.Monad.Builtin
primAgdaClauseClause	Agda.TypeChecking.Monad.Builtin
primAgdaDefinition	Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataConstructor	Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataDef	Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionFunDef	Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionPostulate	Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionPrimitive	Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionRecordDef	Agda.TypeChecking.Monad.Builtin
primAgdaErrorPart	Agda.TypeChecking.Monad.Builtin
primAgdaErrorPartName	Agda.TypeChecking.Monad.Builtin
primAgdaErrorPartString	Agda.TypeChecking.Monad.Builtin
primAgdaErrorPartTerm	Agda.TypeChecking.Monad.Builtin
primAgdaLitChar	Agda.TypeChecking.Monad.Builtin
primAgdaLiteral	Agda.TypeChecking.Monad.Builtin
primAgdaLitFloat	Agda.TypeChecking.Monad.Builtin
primAgdaLitMeta	Agda.TypeChecking.Monad.Builtin
primAgdaLitNat	Agda.TypeChecking.Monad.Builtin
primAgdaLitQName	Agda.TypeChecking.Monad.Builtin
primAgdaLitString	Agda.TypeChecking.Monad.Builtin
primAgdaLitWord64	Agda.TypeChecking.Monad.Builtin
primAgdaMeta	Agda.TypeChecking.Monad.Builtin
primAgdaPatAbsurd	Agda.TypeChecking.Monad.Builtin
primAgdaPatCon	Agda.TypeChecking.Monad.Builtin
primAgdaPatDot	Agda.TypeChecking.Monad.Builtin
primAgdaPatLit	Agda.TypeChecking.Monad.Builtin
primAgdaPatProj	Agda.TypeChecking.Monad.Builtin
primAgdaPattern	Agda.TypeChecking.Monad.Builtin
primAgdaPatVar	Agda.TypeChecking.Monad.Builtin
primAgdaSort	Agda.TypeChecking.Monad.Builtin
primAgdaSortLit	Agda.TypeChecking.Monad.Builtin
primAgdaSortSet	Agda.TypeChecking.Monad.Builtin
primAgdaSortUnsupported	Agda.TypeChecking.Monad.Builtin
primAgdaTCM	Agda.TypeChecking.Monad.Builtin
primAgdaTCMBind	Agda.TypeChecking.Monad.Builtin
primAgdaTCMBlockOnMeta	Agda.TypeChecking.Monad.Builtin
primAgdaTCMCatchError	Agda.TypeChecking.Monad.Builtin
primAgdaTCMCheckType	Agda.TypeChecking.Monad.Builtin
primAgdaTCMCommit	Agda.TypeChecking.Monad.Builtin
primAgdaTCMDebugPrint	Agda.TypeChecking.Monad.Builtin
primAgdaTCMDeclareDef	Agda.TypeChecking.Monad.Builtin
primAgdaTCMDeclarePostulate	Agda.TypeChecking.Monad.Builtin
primAgdaTCMDefineFun	Agda.TypeChecking.Monad.Builtin
primAgdaTCMExtendContext	Agda.TypeChecking.Monad.Builtin
primAgdaTCMFreshName	Agda.TypeChecking.Monad.Builtin
primAgdaTCMGetContext	Agda.TypeChecking.Monad.Builtin
primAgdaTCMGetDefinition	Agda.TypeChecking.Monad.Builtin
primAgdaTCMGetType	Agda.TypeChecking.Monad.Builtin
primAgdaTCMInContext	Agda.TypeChecking.Monad.Builtin
primAgdaTCMInferType	Agda.TypeChecking.Monad.Builtin
primAgdaTCMIsMacro	Agda.TypeChecking.Monad.Builtin
primAgdaTCMNoConstraints	Agda.TypeChecking.Monad.Builtin
primAgdaTCMNormalise	Agda.TypeChecking.Monad.Builtin
primAgdaTCMQuoteTerm	Agda.TypeChecking.Monad.Builtin
primAgdaTCMReduce	Agda.TypeChecking.Monad.Builtin
primAgdaTCMReturn	Agda.TypeChecking.Monad.Builtin
primAgdaTCMRunSpeculative	Agda.TypeChecking.Monad.Builtin
primAgdaTCMTypeError	Agda.TypeChecking.Monad.Builtin
primAgdaTCMUnify	Agda.TypeChecking.Monad.Builtin
primAgdaTCMUnquoteTerm	Agda.TypeChecking.Monad.Builtin
primAgdaTCMWithNormalisation	Agda.TypeChecking.Monad.Builtin
primAgdaTerm	Agda.TypeChecking.Monad.Builtin
primAgdaTermCon	Agda.TypeChecking.Monad.Builtin
primAgdaTermDef	Agda.TypeChecking.Monad.Builtin
primAgdaTermExtLam	Agda.TypeChecking.Monad.Builtin
primAgdaTermLam	Agda.TypeChecking.Monad.Builtin
primAgdaTermLit	Agda.TypeChecking.Monad.Builtin
primAgdaTermMeta	Agda.TypeChecking.Monad.Builtin
primAgdaTermPi	Agda.TypeChecking.Monad.Builtin
primAgdaTermSort	Agda.TypeChecking.Monad.Builtin
primAgdaTermUnsupported	Agda.TypeChecking.Monad.Builtin
primAgdaTermVar	Agda.TypeChecking.Monad.Builtin
primArg	Agda.TypeChecking.Monad.Builtin
primArgArg	Agda.TypeChecking.Monad.Builtin
primArgArgInfo	Agda.TypeChecking.Monad.Builtin
primArgInfo	Agda.TypeChecking.Monad.Builtin
primAssoc	Agda.TypeChecking.Monad.Builtin
primAssocLeft	Agda.TypeChecking.Monad.Builtin
primAssocNon	Agda.TypeChecking.Monad.Builtin
primAssocRight	Agda.TypeChecking.Monad.Builtin
primBody	Agda.Compiler.MAlonzo.Primitives
primBool	Agda.TypeChecking.Monad.Builtin
primChar	Agda.TypeChecking.Monad.Builtin
primCharToNatInjective	Agda.TypeChecking.Primitive
primClauses	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primComp	Agda.TypeChecking.Primitive
primCompiled	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primConId	Agda.TypeChecking.Monad.Builtin
primCons	Agda.TypeChecking.Monad.Builtin
primDepIMin'	Agda.TypeChecking.Primitive
Prime	Agda.Utils.Suffix
primEquality	Agda.TypeChecking.Monad.Builtin
primEqualityName	Agda.TypeChecking.Monad.Builtin
primEquiv	Agda.TypeChecking.Monad.Builtin
primEquivFun	Agda.TypeChecking.Monad.Builtin
primEquivProof	Agda.TypeChecking.Monad.Builtin
primEraseEquality	Agda.TypeChecking.Primitive
primFaceForall	Agda.TypeChecking.Monad.Builtin
primFaceForall'	Agda.TypeChecking.Primitive
primFalse	Agda.TypeChecking.Monad.Builtin
primFixity	Agda.TypeChecking.Monad.Builtin
primFixityFixity	Agda.TypeChecking.Monad.Builtin
primFlat	Agda.TypeChecking.Monad.Builtin
primFloat	Agda.TypeChecking.Monad.Builtin
primForce	Agda.TypeChecking.Primitive
primForceLemma	Agda.TypeChecking.Primitive
primFromNat	Agda.TypeChecking.Monad.Builtin
primFromNeg	Agda.TypeChecking.Monad.Builtin
primFromString	Agda.TypeChecking.Monad.Builtin
PrimFun
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFun	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunArity	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunImplementation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlue	Agda.TypeChecking.Monad.Builtin
primGlue'	Agda.TypeChecking.Primitive
primHComp	Agda.TypeChecking.Monad.Builtin
primHComp'	Agda.TypeChecking.Primitive
primHidden	Agda.TypeChecking.Monad.Builtin
primHiding	Agda.TypeChecking.Monad.Builtin
primIBin	Agda.TypeChecking.Primitive
primId	Agda.TypeChecking.Monad.Builtin
primIdElim	Agda.TypeChecking.Monad.Builtin
primIdElim'	Agda.TypeChecking.Primitive
primIdFace'	Agda.TypeChecking.Primitive
primIdJ	Agda.TypeChecking.Primitive
primIdPath'	Agda.TypeChecking.Primitive
primIMax	Agda.TypeChecking.Monad.Builtin
primIMax'	Agda.TypeChecking.Primitive
primIMin	Agda.TypeChecking.Monad.Builtin
primIMin'	Agda.TypeChecking.Primitive
PrimImpl	Agda.TypeChecking.Primitive
primINeg	Agda.TypeChecking.Monad.Builtin
primINeg'	Agda.TypeChecking.Primitive
primInf	Agda.TypeChecking.Monad.Builtin
primInstance	Agda.TypeChecking.Monad.Builtin
primInteger	Agda.TypeChecking.Monad.Builtin
primIntegerNegSuc	Agda.TypeChecking.Monad.Builtin
primIntegerPos	Agda.TypeChecking.Monad.Builtin
primInterval	Agda.TypeChecking.Monad.Builtin
primInv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIO	Agda.TypeChecking.Monad.Builtin
primIOne	Agda.TypeChecking.Monad.Builtin
primIrrelevant	Agda.TypeChecking.Monad.Builtin
primIsOne	Agda.TypeChecking.Monad.Builtin
primIsOne1	Agda.TypeChecking.Monad.Builtin
primIsOne2	Agda.TypeChecking.Monad.Builtin
primIsOneEmpty	Agda.TypeChecking.Monad.Builtin
primItIsOne	Agda.TypeChecking.Monad.Builtin
Primitive
1 (Data Constructor)	Agda.Syntax.Reflected
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Interaction.Highlighting.Precise
4 (Data Constructor)	Agda.Syntax.Abstract
5 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveFunction	Agda.Syntax.Concrete.Definitions
primitiveFunctions	Agda.TypeChecking.Primitive
PrimitiveImpl	Agda.TypeChecking.Primitive
primitiveModules	Agda.Interaction.Options.Lenses
primitives	Agda.Compiler.JS.Compiler
PrimitiveType	Agda.Interaction.Highlighting.Precise
primIZero	Agda.TypeChecking.Monad.Builtin
primLevel	Agda.TypeChecking.Monad.Builtin
primLevelMax	Agda.TypeChecking.Monad.Builtin
primLevelSuc	Agda.TypeChecking.Monad.Builtin
primLevelZero	Agda.TypeChecking.Monad.Builtin
primList	Agda.TypeChecking.Monad.Builtin
primName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNat	Agda.TypeChecking.Monad.Builtin
primNatDivSucAux	Agda.TypeChecking.Monad.Builtin
primNatEquality	Agda.TypeChecking.Monad.Builtin
primNatLess	Agda.TypeChecking.Monad.Builtin
primNatMinus	Agda.TypeChecking.Monad.Builtin
primNatModSucAux	Agda.TypeChecking.Monad.Builtin
primNatPlus	Agda.TypeChecking.Monad.Builtin
primNatTimes	Agda.TypeChecking.Monad.Builtin
primNil	Agda.TypeChecking.Monad.Builtin
primPartial	Agda.TypeChecking.Monad.Builtin
primPartial'	Agda.TypeChecking.Primitive
primPartialP	Agda.TypeChecking.Monad.Builtin
primPartialP'	Agda.TypeChecking.Primitive
primPath	Agda.TypeChecking.Monad.Builtin
primPathP	Agda.TypeChecking.Monad.Builtin
primPathToEquiv	Agda.TypeChecking.Monad.Builtin
primPOr	Agda.TypeChecking.Primitive
primPrecedence	Agda.TypeChecking.Monad.Builtin
primPrecRelated	Agda.TypeChecking.Monad.Builtin
primPrecUnrelated	Agda.TypeChecking.Monad.Builtin
primQName	Agda.TypeChecking.Monad.Builtin
primRefl	Agda.TypeChecking.Monad.Builtin
primRelevance	Agda.TypeChecking.Monad.Builtin
primRelevant	Agda.TypeChecking.Monad.Builtin
primRewrite	Agda.TypeChecking.Monad.Builtin
primSetOmega	Agda.TypeChecking.Monad.Builtin
primSharp	Agda.TypeChecking.Monad.Builtin
primSigma	Agda.TypeChecking.Monad.Builtin
primSize	Agda.TypeChecking.Monad.Builtin
primSizeInf	Agda.TypeChecking.Monad.Builtin
primSizeLt	Agda.TypeChecking.Monad.Builtin
primSizeMax	Agda.TypeChecking.Monad.Builtin
primSizeSuc	Agda.TypeChecking.Monad.Builtin
primSizeUniv	Agda.TypeChecking.Monad.Builtin
primString	Agda.TypeChecking.Monad.Builtin
primStringToListInjective	Agda.TypeChecking.Primitive
primSub	Agda.TypeChecking.Monad.Builtin
primSubIn	Agda.TypeChecking.Monad.Builtin
primSubOut	Agda.TypeChecking.Monad.Builtin
primSubOut'	Agda.TypeChecking.Primitive
primSuc	Agda.TypeChecking.Monad.Builtin
PrimTerm	Agda.TypeChecking.Primitive
primTerm	Agda.TypeChecking.Primitive
primTrans	Agda.TypeChecking.Monad.Builtin
primTrans'	Agda.TypeChecking.Primitive
primTransHComp	Agda.TypeChecking.Primitive
primTrue	Agda.TypeChecking.Monad.Builtin
PrimType	Agda.TypeChecking.Primitive
primType	Agda.TypeChecking.Primitive
primUnit	Agda.TypeChecking.Monad.Builtin
primUnitUnit	Agda.TypeChecking.Monad.Builtin
primVisible	Agda.TypeChecking.Monad.Builtin
primWord64	Agda.TypeChecking.Monad.Builtin
primWord64ToNatInjective	Agda.TypeChecking.Primitive
primZero	Agda.TypeChecking.Monad.Builtin
prim_glue	Agda.TypeChecking.Monad.Builtin
prim_glue'	Agda.TypeChecking.Primitive
prim_unglue	Agda.TypeChecking.Monad.Builtin
prim_unglue'	Agda.TypeChecking.Primitive
print	Agda.TypeChecking.Monad.Benchmark
printErrorInfo	Agda.Interaction.Highlighting.Generate
printHighlightingInfo	Agda.Interaction.Highlighting.Generate
printLocals	Agda.Syntax.Scope.Monad
PrintRange
1 (Type/Class)	Agda.Syntax.Position
2 (Data Constructor)	Agda.Syntax.Position
printScope	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
printStatistics	Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
printSyntaxInfo	Agda.Interaction.Highlighting.Generate
printUnsolvedInfo	Agda.Interaction.Highlighting.Generate
printUsage	Agda.Main
printVersion	Agda.Main
Prio
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
prioAbsurdLambda	Agda.Auto.SearchControl
prioCompareArgList	Agda.Auto.SearchControl
prioCompBeta	Agda.Auto.SearchControl
prioCompBetaStructured	Agda.Auto.SearchControl
prioCompChoice	Agda.Auto.SearchControl
prioCompCopy	Agda.Auto.SearchControl
prioCompIota	Agda.Auto.SearchControl
prioCompUnif	Agda.Auto.SearchControl
prioInferredTypeUnknown	Agda.Auto.SearchControl
PrioMeta
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
prioNo	Agda.Auto.SearchControl
prioNoIota	Agda.Auto.SearchControl
prioProjIndex	Agda.Auto.SearchControl
prioTypecheck	Agda.Auto.SearchControl
prioTypecheckArgList	Agda.Auto.SearchControl
prioTypeUnknown	Agda.Auto.SearchControl
Private	Agda.Syntax.Concrete
PrivateAccess	Agda.Syntax.Common
PrivateNS	Agda.Syntax.Scope.Base
Problem
1 (Type/Class)	Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)	Agda.TypeChecking.Rules.LHS.Problem
ProblemConstraint	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
problemCont	Agda.TypeChecking.Rules.LHS.Problem
ProblemEq
1 (Type/Class)	Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)	Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
problemEqs	Agda.TypeChecking.Rules.LHS.Problem
ProblemId
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
problemInPat	Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
problemInPats	Agda.TypeChecking.Rules.LHS.Problem
problemInst	Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
problemRestPats	Agda.TypeChecking.Rules.LHS.Problem
problemType
1 (Function)	Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
2 (Function)	Agda.TypeChecking.MetaVars
Processor	Agda.Syntax.Parser.Literate
productOfEdgesInBoundedWalk	Agda.TypeChecking.Positivity.Occurrence
Products	Agda.Utils.TypeLevel
Proj
1 (Data Constructor)	Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Abstract
projArgInfo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projCase	Agda.TypeChecking.CompiledClause
projDropPars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projDropParsApply	Agda.TypeChecking.Substitute
ProjectedVar	Agda.TypeChecking.MetaVars
Projection
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projectionArgs	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionLikeness	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
ProjectionReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionView
1 (Type/Class)	Agda.TypeChecking.ProjectionLike
2 (Data Constructor)	Agda.TypeChecking.ProjectionLike
projectRoot	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
projectTyped	Agda.TypeChecking.Records
projFromType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projIndex	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjLams
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projLams	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projOrig	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjOrigin	Agda.Syntax.Common
ProjP
1 (Data Constructor)	Agda.Syntax.Reflected
2 (Data Constructor)	Agda.Syntax.Internal
3 (Data Constructor)	Agda.Syntax.Abstract
projPatterns	Agda.TypeChecking.CompiledClause
ProjPostfix	Agda.Syntax.Common
ProjPrefix	Agda.Syntax.Common
projProper	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjSystem	Agda.Syntax.Common
ProjT	Agda.TypeChecking.Records
projTField	Agda.TypeChecking.Records
projTRec	Agda.TypeChecking.Records
projUseSizeLt	Agda.Termination.Monad
ProjVarExc
1 (Type/Class)	Agda.TypeChecking.MetaVars
2 (Data Constructor)	Agda.TypeChecking.MetaVars
projView	Agda.TypeChecking.ProjectionLike
projViewProj	Agda.TypeChecking.ProjectionLike
projViewSelf	Agda.TypeChecking.ProjectionLike
projViewSpine	Agda.TypeChecking.ProjectionLike
Prop
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Syntax.Internal
4 (Data Constructor)	Agda.Syntax.Abstract
propagatePrio	Agda.Auto.NarrowingSearch
properlyMatching	Agda.Syntax.Internal
properSplit	Agda.TypeChecking.CompiledClause.Compile
PropMustBeSingleton	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PropN	Agda.Syntax.Concrete
prune	Agda.TypeChecking.MetaVars.Occurs
PrunedEverything	Agda.TypeChecking.MetaVars.Occurs
PrunedNothing	Agda.TypeChecking.MetaVars.Occurs
PrunedSomething	Agda.TypeChecking.MetaVars.Occurs
PruneResult	Agda.TypeChecking.MetaVars.Occurs
PSeq	Agda.Syntax.Treeless, Agda.Compiler.Backend
pshow
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
PState	Agda.Syntax.Parser.Monad
PStr	Agda.Utils.Pretty
PSub	Agda.Syntax.Treeless, Agda.Compiler.Backend
PSub64	Agda.Syntax.Treeless, Agda.Compiler.Backend
PSyn
1 (Type/Class)	Agda.Syntax.Internal.Names
2 (Data Constructor)	Agda.Syntax.Internal.Names
PTerm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ptext	Agda.Utils.Pretty
Ptr	Agda.Utils.Pointer
PTSInstance	Agda.Interaction.BasicOps
ptsRule	Agda.TypeChecking.Sort
ptsRule'	Agda.TypeChecking.Sort
PublicAccess	Agda.Syntax.Common
publicModules	Agda.Syntax.Scope.Base
publicNames	Agda.Syntax.Scope.Base
PublicNS	Agda.Syntax.Scope.Base
publicOpen	Agda.Syntax.Common
punctuate
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
pureTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
purgeNonvariant	Agda.TypeChecking.Polarity
pushContext	Agda.Syntax.Parser.Monad
pushContextPrecedence	Agda.Syntax.Scope.Monad
pushCurrentContext	Agda.Syntax.Parser.Monad
pushLexState	Agda.Syntax.Parser.Monad
pushPrecedence	Agda.Syntax.Fixity
putAbsoluteIncludePaths	Agda.Interaction.Options.Lenses
putAllConstraintsToSleep	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putAllowedReductions	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putBenchmark	Agda.Utils.Benchmark
putConstraintsToSleep	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putIncludePaths	Agda.Interaction.Options.Lenses
putPersistentVerbosity	Agda.Interaction.Options.Lenses
putResponse
1 (Function)	Agda.Interaction.EmacsCommand
2 (Function)	Agda.Interaction.InteractionTop
putSafeMode	Agda.Interaction.Options.Lenses
putTC	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putVerbosity	Agda.Interaction.Options.Lenses
PVar
1 (Data Constructor)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PWild	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PWildCard	Agda.Utils.Haskell.Syntax
pwords
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty