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
package	Agda.Version
packUnquoteM	Agda.TypeChecking.Unquote
packW64	Agda.Utils.Word
pad	Agda.Utils.ListInf
PAdd	Agda.Syntax.Treeless, Agda.Compiler.Backend
PAdd64	Agda.Syntax.Treeless, Agda.Compiler.Backend
PageMode	Agda.Syntax.Common.Pretty
Pair
1 (Type/Class)	Agda.Utils.Tuple
2 (Data Constructor)	Agda.Utils.Tuple
3 (Data Constructor)	Agda.Utils.TypeLevel
PairInt	Agda.Utils.RangeMap
pairs	Agda.Interaction.JSON
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.Syntax.Common.Pretty
2 (Function)	Agda.Compiler.JS.Pretty
3 (Function)	Agda.TypeChecking.Pretty
parens'	Agda.Interaction.Base
parensNonEmpty
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.TypeChecking.Pretty
parentPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
parentProjectionOrigin	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ParenV	Agda.Syntax.Concrete.Operators.Parser
Parse	Agda.Interaction.Base
parse
1 (Function)	Agda.Utils.Parser.MemoisedCPS
2 (Function)	Agda.Syntax.Concrete.Operators.Parser.Monad
3 (Function)	Agda.Syntax.Concrete.Operators.Parser
4 (Function)	Agda.Syntax.Parser.Monad
5 (Function)	Agda.Syntax.Parser
parseAndDoAtToplevel	Agda.Interaction.InteractionTop
parseApplication	Agda.Syntax.Concrete.Operators
parseArguments	Agda.Syntax.Concrete.Operators
parseAttributes	Agda.Syntax.Parser.Monad
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	Agda.Interaction.BasicOps
parseExprFromAuto	Agda.Interaction.InteractionTop
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
parseIdiomBracketsSeq	Agda.Syntax.IdiomBrackets
parseIndexedJSON	Agda.Interaction.JSON
parseInp	Agda.Syntax.Parser.Monad
parseIOTCM	Agda.Interaction.Base
parseJSON	Agda.Interaction.JSON
parseJSON1	Agda.Interaction.JSON
parseJSON2	Agda.Interaction.JSON
parseJSONList	Agda.Interaction.JSON
parseKeepComments	Agda.Syntax.Parser.Monad
parseLastPos	Agda.Syntax.Parser.Monad
parseLayKw	Agda.Syntax.Parser.Monad
parseLayout	Agda.Syntax.Parser.Monad
parseLayStatus	Agda.Syntax.Parser.Monad
parseLexState	Agda.Syntax.Parser.Monad
parseLHS	Agda.Syntax.Concrete.Operators
parseLibFile	Agda.Interaction.Library.Parse
parseLibName	Agda.Interaction.Library.Base, Agda.Interaction.Library
parseName	Agda.Interaction.BasicOps
ParseOk	Agda.Syntax.Parser.Monad
parseOptions	Agda.Mimer.Options
parsePattern	Agda.Syntax.Concrete.Operators
parsePatternSyn	Agda.Syntax.Concrete.Operators
parsePluginOptions	Agda.Interaction.Options
parsePolarity	Agda.Syntax.Parser.Helpers
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
parseRangeString	Agda.Syntax.Parser
parserBased	Agda.Interaction.Highlighting.Precise
ParserClass	Agda.Utils.Parser.MemoisedCPS
ParserError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
parseSource	Agda.Interaction.Imports
parseSrcFile	Agda.Syntax.Parser.Monad
ParseState	Agda.Syntax.Parser.Monad
parseTime	Agda.Mimer.Options
parseToReadsPrec	Agda.Interaction.Base
parseVariables	Agda.Interaction.MakeCase
parseVerboseKey	Agda.Interaction.Options
ParseWarning
1 (Type/Class)	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
parseWarning	Agda.Syntax.Parser.Monad
parseWarningName	Agda.Syntax.Parser.Monad
parseWarnings	Agda.Syntax.Parser.Monad
Parsing	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Partial	Agda.Interaction.Highlighting.Generate
PartialOrd	Agda.Utils.PartialOrd
PartialOrdering	Agda.Utils.PartialOrd
partition
1 (Function)	Agda.Utils.List1
2 (Function)	Agda.Utils.Set1
3 (Function)	Agda.Utils.Map1
partition3	Agda.Utils.Three
partitionByKindOfForeignCode	Agda.Compiler.MAlonzo.Pragmas
partitionEithers	Agda.Utils.List1
partitionEithers3	Agda.Utils.Three
partitionImportedNames	Agda.Syntax.Common
partitionM	Agda.Utils.Monad
partitionMaybe	Agda.Utils.List
partitionStepResult	Agda.Mimer.Monad
partitionWithKey	Agda.Utils.Map1
partP	Agda.Syntax.Concrete.Operators.Parser
PAsPat	Agda.Utils.Haskell.Syntax
passCode	Agda.Compiler.ToTreeless
passName	Agda.Compiler.ToTreeless
passTag	Agda.Compiler.ToTreeless
passVerbosity	Agda.Compiler.ToTreeless
Pat	Agda.Utils.Haskell.Syntax
patAsNames	Agda.Syntax.Internal
path	Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
PathAbstractionFailed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PathAbstractionFailed_	Agda.Interaction.Options.Errors
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
pathTelescope'	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PathType	Agda.Syntax.Internal
pathType	Agda.Syntax.Internal
pathUnview	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PathView	Agda.Syntax.Internal
pathView	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pathView'	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pathViewAsPi	Agda.TypeChecking.Telescope
pathViewAsPi'	Agda.TypeChecking.Telescope
pathViewAsPi'whnf	Agda.TypeChecking.Telescope
PatInfo	Agda.Syntax.Info
PatLamWithoutClauses	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatLamWithoutClauses_	Agda.Interaction.Options.Errors
patmMetas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
patmRemainder	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Internal
PatOSplit	Agda.Syntax.Internal
PatOSplitArg	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.Internal
2 (Type/Class)	Agda.Syntax.Reflected
3 (Type/Class)	Agda.Syntax.Concrete
4 (Type/Class)	Agda.Syntax.Abstract
Pattern'
1 (Type/Class)	Agda.Syntax.Internal
2 (Type/Class)	Agda.Syntax.Abstract
patternAppView	Agda.Syntax.Concrete.Pattern
patternBinder	Agda.Syntax.Concrete.Operators.Parser
PatternBound	Agda.Syntax.Scope.Base
patternDepth	Agda.Termination.Monad
PatternErr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternFrom	Agda.TypeChecking.Rewriting.NonLinPattern
patternFrom	Agda.TypeChecking.Rewriting.NonLinPattern
PatternInfo
1 (Type/Class)	Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Internal
patternInfo	Agda.Syntax.Internal
PatternInPathLambda	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternInPathLambda_	Agda.Interaction.Options.Errors
PatternInSystem	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternInSystem_	Agda.Interaction.Options.Errors
patternInTeleName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternLambdas	Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternLike	Agda.Syntax.Internal.Pattern
PatternMatching	Agda.Syntax.Common
PatternMatchingAllowed	Agda.Syntax.Common
patternMatchingAllowed	Agda.Syntax.Common
patternNames	Agda.Syntax.Concrete.Pattern
PatternOrCopattern
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Concrete
patternOrigin	Agda.Syntax.Internal
patternQNames	Agda.Syntax.Concrete.Pattern
Patterns	Agda.Syntax.Abstract
PatternShadowsConstructor	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternShadowsConstructor_	Agda.Interaction.Options.Warnings
patternsToElims	Agda.Syntax.Internal.Pattern
PatternSubstitution	Agda.Syntax.Internal
PatternSyn
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
patternSynArgs	Agda.Syntax.Parser.Helpers
PatternSynDef	Agda.Syntax.Abstract
PatternSynDefn	Agda.Syntax.Abstract
PatternSynDefns	Agda.Syntax.Abstract
PatternSynDefS	Agda.Syntax.Abstract
PatternSynName	Agda.Syntax.Scope.Base
PatternSynonymArgumentShadows	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternSynonymArgumentShadows_	Agda.Interaction.Options.Errors
PatternSynP	Agda.Syntax.Abstract
PatternSynResName	Agda.Syntax.Scope.Base
patternToArgPattern	Agda.Syntax.Parser.Helpers
patternToElim	Agda.Syntax.Internal.Pattern
PatternToExpr	Agda.Syntax.Abstract.Pattern
patternToExpr	Agda.Syntax.Abstract.Pattern
patternToModuleBound	Agda.Syntax.Scope.Base
patternToNames	Agda.Syntax.Parser.Helpers
patternToTerm	Agda.Syntax.Internal.Pattern
patternVariables	Agda.TypeChecking.Rules.LHS.Problem
PatternVarModalities	Agda.Syntax.Internal.Pattern
patternVarModalities	Agda.Syntax.Internal.Pattern
PatternVarOut	Agda.Syntax.Internal, Agda.Syntax.Internal
PatternVars	Agda.Syntax.Internal
patternVars
1 (Function)	Agda.Syntax.Internal
2 (Function)	Agda.Syntax.Abstract.Pattern
patternView	Agda.Syntax.Concrete.Operators.Parser
patternViolation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
patternViolation'	Agda.TypeChecking.MetaVars.Occurs
patToExpr	Agda.Syntax.Abstract.Pattern
PattPart	Agda.TypeChecking.Unquote
PatTypeSig	Agda.Utils.Haskell.Syntax
PatVar	Agda.Syntax.Internal.Pattern
PatVarLabel	Agda.Syntax.Internal.Pattern
PatVarName	Agda.Syntax.Internal
patVarNameToString	Agda.Syntax.Internal
PBangPat	Agda.Utils.Haskell.Syntax
PBoundVar	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
Peano	Agda.Utils.Size
PElims	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
permutations	Agda.Utils.List1
permutations1	Agda.Utils.List1
Permute	Agda.Utils.GetOpt
permute	Agda.Utils.Permutation
permuteContext	Agda.TypeChecking.Telescope
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
PGeq	Agda.Syntax.Treeless, Agda.Compiler.Backend
Phase	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
pHasEta0	Agda.Syntax.Concrete.Pretty
Pi
1 (Data Constructor)	Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Reflected
3 (Data Constructor)	Agda.Syntax.Concrete
4 (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
piApplyM'	Agda.TypeChecking.Telescope
piBrackets	Agda.Syntax.Fixity
pickName	Agda.TypeChecking.Unquote
PIf	Agda.Syntax.Treeless, Agda.Compiler.Backend
PiHead	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PiK	Agda.TypeChecking.DiscrimTree.Types
PInf	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PiNotLam	Agda.TypeChecking.Rules.Term
PIntervalUniv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
piOrPath	Agda.TypeChecking.Telescope
pipe	Agda.Syntax.Common.Pretty
Pipeline	Agda.Compiler.ToTreeless
PIrrPat	Agda.Utils.Haskell.Syntax
PiSort	Agda.Syntax.Internal
piSort	Agda.TypeChecking.Substitute
piSort'	Agda.TypeChecking.Substitute
piSortM	Agda.TypeChecking.Substitute
PITo64	Agda.Syntax.Treeless, Agda.Compiler.Backend
PiView
1 (Type/Class)	Agda.Syntax.Abstract.Views
2 (Data Constructor)	Agda.Syntax.Abstract.Views
piView	Agda.Syntax.Abstract.Views
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
PlentyInHardCompileTimeMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PlentyInHardCompileTimeMode_	Agda.Interaction.Options.Warnings
PLevelUniv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PLit	Agda.Utils.Haskell.Syntax
PLockUniv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PLt	Agda.Syntax.Treeless, Agda.Compiler.Backend
PLt64	Agda.Syntax.Treeless, Agda.Compiler.Backend
plugHole	Agda.Utils.Zipper
pluralS
1 (Function)	Agda.Utils.String
2 (Function)	Agda.Syntax.Common.Pretty
3 (Function)	Agda.TypeChecking.Pretty
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
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
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.Syntax.Concrete.Fixity
2 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
polaritiesFromAssignments	Agda.TypeChecking.SizedTypes.Syntax
Polarity
1 (Type/Class)	Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
PolarityAssignment
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor)	Agda.TypeChecking.SizedTypes.Syntax
PolarityAttribute	Agda.Syntax.Concrete.Attribute
polarityAttributeTable	Agda.Syntax.Concrete.Attribute
PolarityModality
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
PolarityPragma	Agda.Syntax.Concrete
PolarityPragmasButNotPostulates	Agda.Syntax.Concrete.Definitions.Errors, 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
popBlock	Agda.Syntax.Parser.Monad
popCatchallPragma	Agda.Syntax.Concrete.Definitions.Monad
popLexState	Agda.Syntax.Parser.Monad
popnCallStack	Agda.Utils.CallStack
posCol	Agda.Syntax.Position
POSemigroup	Agda.Utils.POMonoid
Position	Agda.Syntax.Position
Position'	Agda.Syntax.Position
positionalModalityComponent	Agda.Syntax.Common
PositionInName	Agda.Syntax.Common
positionInvariant	Agda.Syntax.Position
PositionMap
1 (Type/Class)	Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
positionMap	Agda.Interaction.Highlighting.Precise
PositionWithoutFile	Agda.Syntax.Position
Positive	Agda.Syntax.Common
Positivity	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
PositivityCheck	Agda.Syntax.Common
positivityCheck	Agda.Syntax.Concrete.Definitions.Types
positivityCheckEnabled	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
positivityCheckPragma	Agda.Syntax.Concrete.Definitions.Monad
PositivityProblem	Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
posLine	Agda.Syntax.Position
posLineCol	Agda.Syntax.Position
posPos	Agda.Syntax.Position
PossiblyUnused	Agda.Compiler.MAlonzo.Misc
Post	Agda.Syntax.Concrete.Operators.Parser
postAction	Agda.TypeChecking.CheckInternal
postCompile	Agda.Compiler.Backend.Base, Agda.Compiler.Backend
PostfixNotation	Agda.Syntax.Notation
PostLeftsK	Agda.Syntax.Concrete.Operators.Parser.Monad
postModule	Agda.Compiler.Backend.Base, Agda.Compiler.Backend
posToInterval	Agda.Syntax.Position
posToRange	Agda.Syntax.Position
posToRange'	Agda.Syntax.Position
PostponedCheckArgs	Agda.Interaction.Base
PostponedCheckFunDef	Agda.Interaction.Base
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
postTraverseAPatternM	Agda.Syntax.Abstract.Pattern
postTraverseCPatternM	Agda.Syntax.Concrete.Pattern
postTraversePatternM	Agda.Syntax.Internal.Pattern
Postulate
1 (Data Constructor)	Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Syntax.Concrete
PostulateBlock	Agda.Syntax.Concrete.Definitions.Types
PostulatedSizeInModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PostulatedSizeInModule_	Agda.Interaction.Options.Errors
powerSet	Agda.Utils.Set1
PPi	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pPi'	Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
PProp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PQuot	Agda.Syntax.Treeless, Agda.Compiler.Backend
PQuot64	Agda.Syntax.Treeless, Agda.Compiler.Backend
Pragma
1 (Data Constructor)	Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Type/Class)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Syntax.Concrete
4 (Type/Class)	Agda.Syntax.Abstract
5 (Data Constructor)	Agda.Syntax.Abstract
PragmaCompiled	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
PragmaCompiled_	Agda.Interaction.Options.Warnings
PragmaCompileErased	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileErased_	Agda.Interaction.Options.Warnings
PragmaCompileList	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileList_	Agda.Interaction.Options.Warnings
PragmaCompileMaybe	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileMaybe_	Agda.Interaction.Options.Warnings
PragmaCompileUnparsable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileUnparsable_	Agda.Interaction.Options.Warnings
PragmaCompileWrong	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileWrongName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileWrongName_	Agda.Interaction.Options.Warnings
PragmaCompileWrong_	Agda.Interaction.Options.Warnings
PragmaExpectsDefinedSymbol	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaExpectsDefinedSymbol_	Agda.Interaction.Options.Warnings
PragmaExpectsUnambiguousConstructorOrFunction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaExpectsUnambiguousConstructorOrFunction_	Agda.Interaction.Options.Warnings
PragmaExpectsUnambiguousProjectionOrFunction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaExpectsUnambiguousProjectionOrFunction_	Agda.Interaction.Options.Warnings
PragmaNoTerminationCheck	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
PragmaNoTerminationCheck_	Agda.Interaction.Options.Warnings
PragmaOptions
1 (Type/Class)	Agda.Interaction.Options
2 (Data Constructor)	Agda.Interaction.Options
pragmaOptions	Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaPolarities	Agda.TypeChecking.Positivity.Occurrence
pragmaQName	Agda.Syntax.Parser.Helpers
pragmaRange	Agda.Interaction.Library.Base, Agda.Interaction.Library
PragmaS	Agda.Syntax.Abstract
Pragmas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pragmaStrings	Agda.Interaction.Library.Base, Agda.Interaction.Library
Pre	Agda.Syntax.Concrete.Operators.Parser
preAction	Agda.TypeChecking.CheckInternal
Precedence	Agda.Syntax.Fixity
PrecedenceKey	Agda.Syntax.Concrete.Operators.Parser.Monad
PrecedenceLevel	Agda.Syntax.Common
PrecedenceStack	Agda.Syntax.Fixity
preCompile	Agda.Compiler.Backend.Base, 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
pRecordDirective	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
prefixBy	Agda.Utils.Trie
PrefixDef	Agda.Syntax.Common
prefixedThings	Agda.Syntax.Common.Pretty
PrefixNotation	Agda.Syntax.Notation
PRem	Agda.Syntax.Treeless, Agda.Compiler.Backend
PRem64	Agda.Syntax.Treeless, Agda.Compiler.Backend
preModule	Agda.Compiler.Backend.Base, Agda.Compiler.Backend
PreOp	Agda.Compiler.JS.Syntax
prepareCommonAssets	Agda.Interaction.Highlighting.LaTeX.Base
prepareCommonDestinationAssets	Agda.Interaction.Highlighting.HTML.Base
prependList
1 (Function)	Agda.Utils.List1
2 (Function)	Agda.Utils.ListInf
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
preTraverseAPatternM	Agda.Syntax.Abstract.Pattern
preTraverseCPatternM	Agda.Syntax.Concrete.Pattern
preTraverseDecl	Agda.Syntax.Concrete.Generic
preTraversePatternM	Agda.Syntax.Internal.Pattern
Pretties	Agda.Compiler.JS.Pretty
pretties	Agda.Compiler.JS.Pretty
Pretty
1 (Type/Class)	Agda.Syntax.Common.Pretty
2 (Type/Class)	Agda.Compiler.JS.Pretty
pretty
1 (Function)	Agda.Syntax.Common.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
prettyAssign	Agda.Syntax.Common.Pretty
prettyATop	Agda.Syntax.Abstract.Pretty
prettyAttr	Agda.Syntax.Parser.Helpers
prettyAUnqualify	Agda.Syntax.Abstract.Pretty
prettyBranch	Agda.Mimer.Monad
prettyCallSite	Agda.Utils.CallStack
prettyCallStack	Agda.Utils.CallStack
prettyCohesion	Agda.Syntax.Common
prettyConstraint	Agda.TypeChecking.Pretty.Constraint
prettyConstraints	Agda.Interaction.BasicOps
PrettyContext
1 (Type/Class)	Agda.TypeChecking.Pretty
2 (Data Constructor)	Agda.TypeChecking.Pretty
prettyDocTree	Agda.Utils.DocTree
prettyDuplicateFields	Agda.TypeChecking.Pretty.Warning
prettyErased	Agda.Syntax.Common
prettyError	Agda.TypeChecking.Errors
prettyFiniteness	Agda.Syntax.Concrete.Pretty
prettyGoalInst	Agda.Mimer.Monad
prettyGoals	Agda.Interaction.BasicOps, Agda.Interaction.EmacsTop
prettyGuardedRhs	Agda.Compiler.MAlonzo.Pretty
prettyHiding	Agda.Syntax.Common
prettyInfoError	Agda.Interaction.EmacsTop
prettyInstalledLibraries	Agda.Interaction.Library.Base
prettyInterestingConstraints	Agda.TypeChecking.Pretty.Constraint
prettyLineColumn	Agda.Syntax.Common.Pretty
prettyList
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.TypeChecking.Pretty
prettyList_
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.TypeChecking.Pretty
prettyLock	Agda.Syntax.Common
prettyMap	Agda.Syntax.Common.Pretty
prettyMap_	Agda.TypeChecking.CompiledClause
prettyNameSpace	Agda.Syntax.Scope.Base
prettyOpApp	Agda.Syntax.Concrete.Pretty
prettyPolarity	Agda.Syntax.Common
prettyPrec
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.Compiler.JS.Pretty
prettyPrecLevelSucs	Agda.Syntax.Internal
prettyPrint	Agda.Compiler.MAlonzo.Pretty
prettyQName	Agda.Compiler.MAlonzo.Pretty
prettyQuantity	Agda.Syntax.Common
prettyR	Agda.TypeChecking.Pretty
prettyRangeConstraint	Agda.TypeChecking.Pretty.Constraint
prettyRelevance	Agda.Syntax.Common
prettyResponseContext	Agda.Interaction.EmacsTop
prettyRhs	Agda.Compiler.MAlonzo.Pretty
prettySet	Agda.Syntax.Common.Pretty
prettyShadowedModule	Agda.TypeChecking.Errors
prettyShow
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.Compiler.JS.Pretty
prettySigCubicalNotErasure	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prettySrcLoc	Agda.Utils.CallStack
prettyTactic	Agda.Syntax.Concrete.Pretty
prettyTactic'	Agda.Syntax.Concrete.Pretty
PrettyTCM	Agda.TypeChecking.Pretty
prettyTCM	Agda.TypeChecking.Pretty
prettyTCMCtx	Agda.TypeChecking.Pretty
prettyTCMPatternList	Agda.TypeChecking.Pretty
prettyTCMPatterns	Agda.TypeChecking.Pretty
PrettyTCMWithNode	Agda.TypeChecking.Pretty
prettyTCMWithNode	Agda.TypeChecking.Pretty
prettyTCWarnings	Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
prettyTCWarnings'	Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
prettyTooManyFields	Agda.TypeChecking.Pretty.Warning
prettyTypeOfMeta	Agda.Interaction.EmacsTop
prettyWarning	Agda.TypeChecking.Pretty.Warning
prettyWarningModeError	Agda.Interaction.Options.Warnings
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, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbsAbs	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbstr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaBlocker	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaBlockerAll	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaBlockerAny	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaBlockerMeta	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClause	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseAbsurd	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseClause	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinition	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionDataConstructor	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionDataDef	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionFunDef	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionPostulate	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionPrimitive	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionRecordDef	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPart	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartName	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartPatt	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartString	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartTerm	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitChar	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLiteral	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitFloat	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitMeta	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitNat	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitQName	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitString	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitWord64	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaMeta	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatAbsurd	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatCon	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatDot	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatLit	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatProj	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPattern	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatVar	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSort	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortInf	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortLit	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortProp	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortPropLit	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortSet	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortUnsupported	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCM	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAskExpandLast	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAskNormalisation	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAskReconstructed	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAskReduceDefs	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMBind	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMBlock	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCatchError	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCheckFromString	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCheckType	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCommit	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDebugPrint	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclareData	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclareDef	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclarePostulate	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDefineData	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDefineFun	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMExec	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMExtendContext	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMFormatErrorParts	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMFreshName	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetContext	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetDefinition	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetInstances	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetType	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMInContext	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMInferType	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMIsMacro	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMNoConstraints	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMNormalise	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMPragmaCompile	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMPragmaForeign	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMQuoteOmegaTerm	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMQuoteTerm	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMReduce	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMReturn	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMRunSpeculative	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMSolveInstances	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMTypeError	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMUnify	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMUnquoteTerm	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithExpandLast	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithNormalisation	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithReconstructed	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithReduceDefs	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWorkOnTypes	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTerm	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermCon	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermDef	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermExtLam	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermLam	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermLit	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermMeta	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermPi	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermSort	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermUnsupported	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermVar	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArg	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgArg	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgArgInfo	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgInfo	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssoc	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocLeft	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocNon	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocRight	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primBody	Agda.Compiler.MAlonzo.Primitives
primBool	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primChar	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimCharEquality	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimCharToNat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimCharToNatInjective	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCharToNatInjective	Agda.TypeChecking.Primitive
primClauses	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimComp	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primComp	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primCompiled	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCons	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Prime	Agda.Utils.Suffix
primEquality	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEqualityName	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquiv	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivFun	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivProof	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimErase	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimEraseEquality	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEraseEquality	Agda.TypeChecking.Primitive
PrimFaceForall	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFaceForall	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFaceForall'	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primFalse	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFixity	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFixityFixity	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFlat	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFloat	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatACos	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatACosh	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatASin	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatASinh	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatATan	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatATan2	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatATanh	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatCeiling	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatCos	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatCosh	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatDecode	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatDiv	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatEncode	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatEquality	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatExp	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatFloor	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatInequality	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatIsInfinite	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatIsNaN	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatIsNegativeZero	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatIsSafeInteger	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatLess	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatLog	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatMinus	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatNegate	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatPlus	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatPow	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatRound	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatSin	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatSinh	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatSqrt	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatTan	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatTanh	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatTimes	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatToRatio	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatToWord64	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatToWord64Injective	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFloatToWord64Injective	Agda.TypeChecking.Primitive
PrimForce	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primForce	Agda.TypeChecking.Primitive
PrimForceLemma	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primForceLemma	Agda.TypeChecking.Primitive
primFromNat	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFromNeg	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFromString	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
primFunArgOccurrences	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.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlue	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlue'	Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimHComp	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHComp	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHComp'	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primHidden	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHiding	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIMax	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMax	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMax'	Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimIMin	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMin	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMin'	Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimImpl	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimINeg	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primINeg	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primINeg'	Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primInf	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInstance	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInteger	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerNegSuc	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerPos	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInterval	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntervalType	Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIntervalUniv	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIntToFloat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIO	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIOne	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIrrelevant	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsAlpha	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsAscii	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsDigit	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsHexDigit	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsLatin1	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsLower	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne1	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne2	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOneEmpty	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsPrint	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsSpace	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primItIsOne	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Primitive
1 (Data Constructor)	Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Syntax.Reflected
3 (Data Constructor)	Agda.Syntax.Concrete
4 (Data Constructor)	Agda.Syntax.Abstract
5 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveBlock	Agda.Syntax.Concrete.Definitions.Types
primitiveById	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveData
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
PrimitiveDefn	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveFunction	Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
primitiveFunctions	Agda.TypeChecking.Primitive
PrimitiveId	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveImpl	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveLibDir	Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primitiveLibDir	Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primitiveModules	Agda.Interaction.Library
PrimitiveName	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveS	Agda.Syntax.Abstract
primitives	Agda.Compiler.JS.Compiler
PrimitiveSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveSortData
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
PrimitiveSortDefn	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveType	Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
primIZero	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primJust	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevel	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimLevelMax	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelMax	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimLevelSuc	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelSuc	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelUniv	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimLevelZero	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelZero	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primList	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimLockUniv	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLockUniv	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLockUniv'	Agda.TypeChecking.Primitive
primMaybe	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimMetaEquality	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimMetaLess	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimMetaToNat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimMetaToNatInjective	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primMetaToNatInjective	Agda.TypeChecking.Primitive
primModality	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primModalityConstructor	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimName	Agda.Syntax.Scope.Base
primName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNat	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatDivSucAux	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatDivSucAux	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatEquality	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatEquality	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatLess	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatLess	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatMinus	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatMinus	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatModSucAux	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatModSucAux	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatPlus	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatPlus	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatTimes	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatTimes	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatToChar	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatToFloat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNil	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNothing	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primOpaque	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimPartial	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartial	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartial'	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimPartialP	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartialP	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartialP'	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPath	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPathP	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimPOr	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPOr	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPrecedence	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPrecRelated	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPrecUnrelated	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primProp	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPropOmega	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQName	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameEquality	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameFixity	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameLess	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameToWord64s	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameToWord64sInjective	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQNameToWord64sInjective	Agda.TypeChecking.Primitive
primQuantity	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQuantity0	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQuantityω	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimRatioToFloat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRefl	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRelevance	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRelevant	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSet	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSetOmega	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSharp	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowChar	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowFloat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowInteger	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowMeta	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowNat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowQName	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowString	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSigma	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSize	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeInf	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeLt	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeMax	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeSuc	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeUniv	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSortName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSortSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSSetOmega	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStrictSet	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primString	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringAppend	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringEquality	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringFromList	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringFromListInjective	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStringFromListInjective	Agda.TypeChecking.Primitive
PrimStringToList	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringToListInjective	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStringToListInjective	Agda.TypeChecking.Primitive
PrimStringUncons	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSub	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubIn	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimSubOut	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubOut	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubOut'	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primSuc	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimTerm	Agda.TypeChecking.Primitive
primTerm	Agda.TypeChecking.Primitive
PrimToLower	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimToUpper	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimTrans	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrans	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrans'	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primTransHComp	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primTranspProof	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrue	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimType	Agda.TypeChecking.Primitive
primType	Agda.TypeChecking.Primitive
primUnit	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primUnitUnit	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primVisible	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primWord64	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimWord64FromNat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimWord64ToNat	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimWord64ToNatInjective	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primWord64ToNatInjective	Agda.TypeChecking.Primitive
primZero	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Prim_glue	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glue	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glue'	Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Prim_glueU	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glueU	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glueU'	Agda.TypeChecking.Primitive.Cubical.HCompU, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Prim_unglue	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglue	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglue'	Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Prim_unglueU	Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglueU	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglueU'	Agda.TypeChecking.Primitive.Cubical.HCompU, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrincipalArgTypeMetas
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
print	Agda.TypeChecking.Monad.Benchmark
printAccumulatedWarnings	Agda.Interaction.BuildLibrary
printAgdaAppDir	Agda.Main
printAgdaDataDir	Agda.Main
PrintAgdaNumericVersion	Agda.Interaction.Options
PrintAgdaVersion
1 (Type/Class)	Agda.Interaction.Options
2 (Data Constructor)	Agda.Interaction.Options
printedOptions	Agda.Interaction.Options.BashCompletion
printedOptionsWithHelp	Agda.Interaction.Options.BashCompletion
printEmacsModeFile	Agda.Setup.EmacsMode
printErrorInfo	Agda.Interaction.Highlighting.Generate
printHighlightingInfo	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend
printLocals	Agda.Syntax.Scope.Monad
printOptions
1 (Function)	Agda.Interaction.Options.BashCompletion
2 (Function)	Agda.Main
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
printTreeAnsi	Agda.Syntax.Common.Pretty.ANSI
printUnsolvedInfo	Agda.Interaction.Highlighting.Generate
printUsage	Agda.Main
printVersion	Agda.Main
Private	Agda.Syntax.Concrete
PrivateAccess	Agda.Syntax.Common
privateAccessInserted	Agda.Syntax.Common
PrivateNS	Agda.Syntax.Scope.Base
PrivateRecordField	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrivateRecordField_	Agda.Interaction.Options.Errors
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.Syntax.Common, Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Common, Agda.Syntax.Internal
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
profileArg	Agda.Interaction.Options.Arguments
ProfileOption	Agda.Interaction.Options.ProfileOptions
ProfileOptions	Agda.Interaction.Options.ProfileOptions
profileOptionsFromList	Agda.Interaction.Options.ProfileOptions
profileOptionsToList	Agda.Interaction.Options.ProfileOptions
profileValues	Agda.Interaction.Options.Arguments
Proj
1 (Data Constructor)	Agda.Syntax.Internal.Elim, 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
ProjectConfig
1 (Type/Class)	Agda.Interaction.Library.Base, Agda.Interaction.Library
2 (Data Constructor)	Agda.Interaction.Library.Base, Agda.Interaction.Library
projectConfigs	Agda.Interaction.Library.Base
ProjectedVar
1 (Type/Class)	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ProjectionIsIrrelevant	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionIsIrrelevant_	Agda.Interaction.Options.Errors
ProjectionLikeness	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
ProjectionLikenessMissing	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TopLevelModuleName
projectTyped	Agda.TypeChecking.Records
ProjEliminator	Agda.TypeChecking.ProjectionLike
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.Internal
2 (Data Constructor)	Agda.Syntax.Reflected
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
ProjVar	Agda.TypeChecking.MetaVars
projView	Agda.TypeChecking.ProjectionLike
projViewProj	Agda.TypeChecking.ProjectionLike
projViewSelf	Agda.TypeChecking.ProjectionLike
projViewSpine	Agda.TypeChecking.ProjectionLike
Prop	Agda.Syntax.Internal
properlyMatching	Agda.TypeChecking.Patterns.Match
properlyMatching'	Agda.TypeChecking.Patterns.Match
properSplit	Agda.TypeChecking.CompiledClause.Compile
PropLitS	Agda.Syntax.Reflected
PropS	Agda.Syntax.Reflected
propToType	Agda.Syntax.Internal
prProjs	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
pruneTemporaryInstances	Agda.TypeChecking.InstanceArguments
PSeq	Agda.Syntax.Treeless, Agda.Compiler.Backend
pshow
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.TypeChecking.Pretty
PSizeUniv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PSSet	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PState	Agda.Syntax.Parser.Monad
PStr	Agda.Syntax.Common.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.Syntax.Common.Pretty
PTSInstance	Agda.Interaction.Base
PType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PublicAccess	Agda.Syntax.Common
publicModules	Agda.Syntax.Scope.Base
publicNames	Agda.Syntax.Scope.Base
publicNamesOfModules	Agda.Syntax.Scope.Base
PublicNS	Agda.Syntax.Scope.Base
publicOpen	Agda.Syntax.Common
punctuate
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.Compiler.JS.Pretty
3 (Function)	Agda.TypeChecking.Pretty
PUniv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pureCompareAs	Agda.TypeChecking.Conversion.Pure
PureConversionT
1 (Type/Class)	Agda.TypeChecking.Conversion.Pure
2 (Data Constructor)	Agda.TypeChecking.Conversion.Pure
pureEqualTerm	Agda.TypeChecking.Conversion.Pure
pureEqualTermB	Agda.TypeChecking.Conversion.Pure
pureEqualType	Agda.TypeChecking.Conversion.Pure
pureEqualTypeB	Agda.TypeChecking.Conversion.Pure
PureTCM	Agda.TypeChecking.Monad.Pure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pureTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
purgeNonvariant	Agda.TypeChecking.Polarity
pushBlock	Agda.Syntax.Parser.Monad
pushLexState	Agda.Syntax.Parser.Monad
pushPrecedence	Agda.Syntax.Fixity
Put
1 (Type/Class)	Agda.Utils.Serialize
2 (Data Constructor)	Agda.Utils.Serialize
put
1 (Function)	Agda.Utils.Serialize
2 (Function)	Agda.Utils.StrictState
3 (Function)	Agda.Utils.StrictState2
put1	Agda.Utils.StrictState2
put2	Agda.Utils.StrictState2
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
putByteArray#	Agda.Utils.Serialize
putConstraintsToSleep	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putDocLn	Agda.Syntax.Common.Pretty.ANSI
putDocTree	Agda.Syntax.Common.Pretty.ANSI
putDocTreeLn	Agda.Syntax.Common.Pretty.ANSI
putPersistentVerbosity	Agda.Interaction.Options.Lenses
putResponse
1 (Function)	Agda.Interaction.Emacs.Lisp
2 (Function)	Agda.Interaction.InteractionTop
putSafeMode	Agda.Interaction.Options.Lenses
putTC	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putTCPreservingSession	Agda.TypeChecking.Monad.State, 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
pvIndex	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PWildCard	Agda.Utils.Haskell.Syntax
pwords
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.TypeChecking.Pretty