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

Index - P

P64ToIAgda.Syntax.Treeless, Agda.Compiler.Backend
packageAgda.Version
packUnquoteMAgda.TypeChecking.Unquote
PAddAgda.Syntax.Treeless, Agda.Compiler.Backend
PAdd64Agda.Syntax.Treeless, Agda.Compiler.Backend
PageModeAgda.Utils.Pretty
Pair 
1 (Type/Class)Agda.Utils.Tuple
2 (Data Constructor)Agda.Utils.Tuple
PairInt 
1 (Type/Class)Agda.Utils.RangeMap
2 (Data Constructor)Agda.Utils.RangeMap
pairsAgda.Interaction.JSON
PAppAgda.Utils.Haskell.Syntax
parallelSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
ParenAgda.Syntax.Concrete
ParenPAgda.Syntax.Concrete
ParenPreferenceAgda.Syntax.Fixity
parens 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
parens'Agda.Interaction.Base
parensNonEmpty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
ParenVAgda.Syntax.Concrete.Operators.Parser
ParseAgda.Interaction.Base
parse 
1 (Function)Agda.Utils.Parser.MemoisedCPS
2 (Function)Agda.Syntax.Concrete.Operators.Parser.Monad
3 (Function)Agda.Syntax.Parser.Monad
4 (Function)Agda.Syntax.Concrete.Operators.Parser
5 (Function)Agda.Syntax.Parser
parseAndDoAtToplevelAgda.Interaction.InteractionTop
parseApplicationAgda.Syntax.Concrete.Operators
parseArgsAgda.Auto.Options
parseBackendOptionsAgda.Compiler.Backend
ParseError 
1 (Type/Class)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
parseErrorAgda.Syntax.Parser.Monad
parseError'Agda.Syntax.Parser.Monad
parseErrorAtAgda.Syntax.Parser.Monad
parseErrorRangeAgda.Syntax.Parser.Monad
parseExprAgda.Interaction.BasicOps
parseExprInAgda.Interaction.BasicOps
ParseFailedAgda.Syntax.Parser.Monad
parseFileAgda.Syntax.Parser
ParseFlags 
1 (Type/Class)Agda.Syntax.Parser.Monad
2 (Data Constructor)Agda.Syntax.Parser.Monad
parseFlagsAgda.Syntax.Parser.Monad
parseFromSrcAgda.Syntax.Parser.Monad
parseHaskellPragmaAgda.Compiler.MAlonzo.Pragmas
parseIdiomBracketsSeqAgda.Syntax.IdiomBrackets
parseIndexedJSONAgda.Interaction.JSON
parseInpAgda.Syntax.Parser.Monad
parseJSONAgda.Interaction.JSON
parseJSON1Agda.Interaction.JSON
parseJSON2Agda.Interaction.JSON
parseJSONListAgda.Interaction.JSON
parseKeepCommentsAgda.Syntax.Parser.Monad
parseLastPosAgda.Syntax.Parser.Monad
parseLayKwAgda.Syntax.Parser.Monad
parseLayoutAgda.Syntax.Parser.Monad
parseLayStatusAgda.Syntax.Parser.Monad
parseLexStateAgda.Syntax.Parser.Monad
parseLHSAgda.Syntax.Concrete.Operators
parseLibFileAgda.Interaction.Library.Parse
parseModuleApplicationAgda.Syntax.Concrete.Operators
parseNameAgda.Interaction.BasicOps
ParseOkAgda.Syntax.Parser.Monad
parsePatternAgda.Syntax.Concrete.Operators
parsePatternSynAgda.Syntax.Concrete.Operators
parsePluginOptionsAgda.Interaction.Options
parsePosAgda.Syntax.Parser.Monad
parsePosString 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.Syntax.Parser
parsePragmaAgda.Compiler.MAlonzo.Pragmas
parsePragmaOptionsAgda.Interaction.Options
parsePrevCharAgda.Syntax.Parser.Monad
parsePrevTokenAgda.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
parserBasedAgda.Interaction.Highlighting.Precise
ParserClassAgda.Utils.Parser.MemoisedCPS
ParseResultAgda.Syntax.Parser.Monad
ParserWithGrammarAgda.Utils.Parser.MemoisedCPS
ParseSections 
1 (Type/Class)Agda.Syntax.Concrete.Operators.Parser
2 (Data Constructor)Agda.Syntax.Concrete.Operators.Parser
parseSourceAgda.Interaction.Imports
parseSrcFileAgda.Syntax.Parser.Monad
ParseStateAgda.Syntax.Parser.Monad
parseTimeAgda.Auto.Options
parseToReadsPrecAgda.Interaction.Base
parseVariablesAgda.Interaction.MakeCase
parseVerboseKeyAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ParseWarning 
1 (Type/Class)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
parseWarningAgda.Syntax.Parser.Monad
parseWarningNameAgda.Syntax.Parser.Monad
parseWarningsAgda.Syntax.Parser.Monad
ParsingAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
PartialAgda.Interaction.Highlighting.Generate
PartialOrdAgda.Utils.PartialOrd
PartialOrderingAgda.Utils.PartialOrd
partitionAgda.Utils.List1
partition3Agda.Utils.Three
partitionByKindOfForeignCodeAgda.Compiler.MAlonzo.Pragmas
partitionEithersAgda.Utils.List1
partitionEithers3Agda.Utils.Three
partitionImportedNamesAgda.Syntax.Common
partitionMAgda.Utils.Monad
partitionMaybeAgda.Utils.List
partPAgda.Syntax.Concrete.Operators.Parser
PAsPatAgda.Utils.Haskell.Syntax
Pat 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Type/Class)Agda.Auto.Syntax
patAsNamesAgda.Syntax.Internal
PatConAppAgda.Auto.Syntax
PatExpAgda.Auto.Syntax
pathAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
PathConsAgda.TypeChecking.Rules.Data
pathLevelAgda.Syntax.Internal
pathLhsAgda.Syntax.Internal
pathNameAgda.Syntax.Internal
pathRhsAgda.Syntax.Internal
pathSortAgda.Syntax.Internal
PathTypeAgda.Syntax.Internal
pathTypeAgda.Syntax.Internal
pathUnviewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
PathViewAgda.Syntax.Internal
pathViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
pathView'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
pathViewAsPiAgda.TypeChecking.Telescope
pathViewAsPi'Agda.TypeChecking.Telescope
pathViewAsPi'whnfAgda.TypeChecking.Telescope
PatInfoAgda.Syntax.Info
patmMetasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
patmRemainderAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PatNameAgda.Syntax.Translation.ConcreteToAbstract
patNoRangeAgda.Syntax.Info
PatOAbsurdAgda.Syntax.Internal
PatOConAgda.Syntax.Internal
PatODotAgda.Syntax.Internal
PatOLitAgda.Syntax.Internal
PatORecAgda.Syntax.Internal
PatOriginAgda.Syntax.Internal
patOriginAgda.Syntax.Internal
PatOSplitAgda.Syntax.Internal
PatOSystemAgda.Syntax.Internal
PatOVarAgda.Syntax.Internal
PatOWildAgda.Syntax.Internal
PatRangeAgda.Syntax.Info
patsToElimsAgda.TypeChecking.With
PatSynAgda.Utils.Haskell.Syntax
Pattern 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Reflected
4 (Type/Class)Agda.Syntax.Abstract
Pattern' 
1 (Type/Class)Agda.Syntax.Internal
2 (Type/Class)Agda.Syntax.Abstract
patternAppViewAgda.Syntax.Concrete.Pattern
patternBinderAgda.Syntax.Concrete.Operators.Parser
PatternBoundAgda.Syntax.Scope.Base
patternDepthAgda.Termination.Monad
PatternErrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PatternFromAgda.TypeChecking.Rewriting.NonLinPattern
patternFromAgda.TypeChecking.Rewriting.NonLinPattern
PatternInfo 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
patternInfoAgda.Syntax.Internal
patternInTeleNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PatternLikeAgda.Syntax.Internal.Pattern
PatternMatchingAgda.Syntax.Common
PatternMatchingAllowedAgda.Syntax.Common
patternMatchingAllowedAgda.Syntax.Common
patternNamesAgda.Syntax.Concrete.Pattern
PatternOrCopattern 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Concrete
patternOriginAgda.Syntax.Internal
patternQNamesAgda.Syntax.Concrete.Pattern
PatternsAgda.Syntax.Abstract
PatternShadowsConstructorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
patternsToElimsAgda.Syntax.Internal.Pattern
PatternSubstitutionAgda.Syntax.Internal
PatternSyn 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
PatternSynDefAgda.Syntax.Abstract
PatternSynDefnAgda.Syntax.Abstract
PatternSynDefnsAgda.Syntax.Abstract
PatternSynNameAgda.Syntax.Scope.Base
PatternSynPAgda.Syntax.Abstract
PatternSynResNameAgda.Syntax.Scope.Base
patternToElimAgda.Syntax.Internal.Pattern
patternToExprAgda.Syntax.Abstract
patternToModuleBoundAgda.Syntax.Scope.Base
patternToTermAgda.Syntax.Internal.Pattern
patternVariablesAgda.TypeChecking.Rules.LHS.Problem
PatternVarModalitiesAgda.Syntax.Internal.Pattern
patternVarModalitiesAgda.Syntax.Internal.Pattern
PatternVarOutAgda.Syntax.Internal, Agda.Syntax.Internal
PatternVarsAgda.Syntax.Internal
patternVars 
1 (Function)Agda.Syntax.Internal
2 (Function)Agda.Syntax.Abstract.Pattern
patternViewAgda.Syntax.Concrete.Operators.Parser
patternViolationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
patternViolation'Agda.TypeChecking.MetaVars.Occurs
PatTypeSigAgda.Utils.Haskell.Syntax
PatVar 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.Internal.Pattern
PatVarLabelAgda.Syntax.Internal.Pattern
PatVarNameAgda.Syntax.Internal
patVarNameToStringAgda.Syntax.Internal
PBAgda.Auto.NarrowingSearch
PBangPatAgda.Utils.Haskell.Syntax
PBlockedAgda.Auto.NarrowingSearch
PBoundVarAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PConstrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
pDomAgda.Syntax.Internal
PDoubleBlockedAgda.Auto.NarrowingSearch
PEConAppAgda.Auto.Typecheck
PElimsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PENoAgda.Auto.Typecheck
PEq64Agda.Syntax.Treeless, Agda.Compiler.Backend
PEqCAgda.Syntax.Treeless, Agda.Compiler.Backend
PEqFAgda.Syntax.Treeless, Agda.Compiler.Backend
PEqIAgda.Syntax.Treeless, Agda.Compiler.Backend
PEqQAgda.Syntax.Treeless, Agda.Compiler.Backend
PEqSAgda.Syntax.Treeless, Agda.Compiler.Backend
performedSimplificationAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
performedSimplification'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
performKillAgda.TypeChecking.MetaVars.Occurs
PermAgda.Utils.Permutation
permPicksAgda.Utils.Permutation
permRangeAgda.Utils.Permutation
PermutationAgda.Utils.Permutation
permuteAgda.Utils.Permutation
permuteTelAgda.TypeChecking.Telescope
PersistentTCStAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PersistentTCStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PersistentVerbosityAgda.Interaction.Options.Lenses
PEvalAgda.Auto.Typecheck
PGeqAgda.Syntax.Treeless, Agda.Compiler.Backend
PhaseAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
pHasEta0Agda.Syntax.Concrete.Pretty
Pi 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Reflected
5 (Data Constructor)Agda.Syntax.Abstract
piAbstractAgda.TypeChecking.Abstract
piAbstractTermAgda.TypeChecking.Abstract
piApplyAgda.TypeChecking.Substitute
PiApplyMAgda.TypeChecking.Telescope
piApplyMAgda.TypeChecking.Telescope
piApplyM'Agda.TypeChecking.Telescope
piBracketsAgda.Syntax.Fixity
pickidAgda.Auto.Typecheck
pickNameAgda.TypeChecking.Unquote
pickUidAgda.Auto.SearchControl
PIfAgda.Syntax.Treeless, Agda.Compiler.Backend
PiHeadAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PInfAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PiNotLamAgda.TypeChecking.Rules.Term
piOrPathAgda.TypeChecking.Telescope
PIrrPatAgda.Utils.Haskell.Syntax
PiSortAgda.Syntax.Internal
piSortAgda.TypeChecking.Substitute
piSort'Agda.TypeChecking.Substitute
PITo64Agda.Syntax.Treeless, Agda.Compiler.Backend
PlaceholderAgda.Syntax.Common
placeholderAgda.Syntax.Concrete.Operators.Parser
PlainJSAgda.Compiler.JS.Syntax
PLamAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PLitAgda.Utils.Haskell.Syntax
PLockUnivAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PLtAgda.Syntax.Treeless, Agda.Compiler.Backend
PLt64Agda.Syntax.Treeless, Agda.Compiler.Backend
plugHoleAgda.Utils.Zipper
Plus 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Utils
2 (Data Constructor)Agda.Syntax.Internal
plusAgda.TypeChecking.SizedTypes.Utils
plusKViewAgda.Syntax.Treeless, Agda.Compiler.Backend
PlusLevelAgda.Syntax.Internal
PlusLevel'Agda.Syntax.Internal
PM 
1 (Type/Class)Agda.Syntax.Parser
2 (Data Constructor)Agda.Syntax.Parser
PMulAgda.Syntax.Treeless, Agda.Compiler.Backend
PMul64Agda.Syntax.Treeless, Agda.Compiler.Backend
PnAgda.Syntax.Position
POAnyAgda.Utils.PartialOrd
POEQAgda.Utils.PartialOrd
POGEAgda.Utils.PartialOrd
POGTAgda.Utils.PartialOrd
PointConsAgda.TypeChecking.Rules.Data
Pointwise 
1 (Type/Class)Agda.Utils.PartialOrd
2 (Data Constructor)Agda.Utils.PartialOrd
pointwiseAgda.Utils.PartialOrd
Polarities 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.Syntax.Concrete.Fixity
polaritiesFromAssignmentsAgda.TypeChecking.SizedTypes.Syntax
Polarity 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PolarityAssignment 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
PolarityPragmaAgda.Syntax.Concrete
PolarityPragmasButNotPostulatesAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
PolarityPragmasButNotPostulates_Agda.Interaction.Options.Warnings
POLEAgda.Utils.PartialOrd
polFromCmpAgda.TypeChecking.Conversion
polFromOccAgda.TypeChecking.Polarity
POLTAgda.Utils.PartialOrd
POMonoidAgda.Utils.POMonoid
popBlockAgda.Syntax.Parser.Monad
popCatchallPragmaAgda.Syntax.Concrete.Definitions.Monad
popLexStateAgda.Syntax.Parser.Monad
popMapSAgda.Auto.Convert
popnCallStackAgda.Utils.CallStack
posColAgda.Syntax.Position
POSemigroupAgda.Utils.POMonoid
PositionAgda.Syntax.Position
Position'Agda.Syntax.Position
PositionInNameAgda.Syntax.Common
positionInvariantAgda.Syntax.Position
PositionMap 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
positionMapAgda.Interaction.Highlighting.Precise
PositionWithoutFileAgda.Syntax.Position
PositivityAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
PositivityCheckAgda.Syntax.Common
positivityCheckAgda.Syntax.Concrete.Definitions.Types
positivityCheckEnabledAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
positivityCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
PositivityProblemAgda.Interaction.Highlighting.Precise
posLineAgda.Syntax.Position
posPosAgda.Syntax.Position
PossiblyUnusedAgda.Compiler.MAlonzo.Misc
PostAgda.Syntax.Concrete.Operators.Parser
postActionAgda.TypeChecking.CheckInternal
postCompileAgda.Compiler.Backend
PostfixNotationAgda.Syntax.Notation
PostLeftsKAgda.Syntax.Concrete.Operators.Parser.Monad
postModuleAgda.Compiler.Backend
posToIntervalAgda.Syntax.Position
posToRangeAgda.Syntax.Position
posToRange'Agda.Syntax.Position
PostponedCheckArgsAgda.Interaction.Base
PostponedCheckFunDefAgda.Interaction.Base
PostponedEquation 
1 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
2 (Data Constructor)Agda.TypeChecking.Rewriting.NonLinMatch
PostponedEquationsAgda.TypeChecking.Rewriting.NonLinMatch
PostponedTypeCheckingProblemAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
postponeInstanceConstraintsAgda.TypeChecking.InstanceArguments
postponeTypeCheckingProblemAgda.TypeChecking.MetaVars
postponeTypeCheckingProblem_Agda.TypeChecking.MetaVars
PostScopeState 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
postTraverseAPatternMAgda.Syntax.Abstract.Pattern
postTraverseCPatternMAgda.Syntax.Concrete.Pattern
postTraversePatternMAgda.Syntax.Internal.Pattern
Postulate 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
PostulateBlockAgda.Syntax.Concrete.Definitions.Types
PPiAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
pPi'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
PPropAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PQuotAgda.Syntax.Treeless, Agda.Compiler.Backend
PQuot64Agda.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
PragmaCompiledAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
PragmaCompiled_Agda.Interaction.Options.Warnings
PragmaCompileErasedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PragmaCompileErased_Agda.Interaction.Options.Warnings
PragmaNoTerminationCheckAgda.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
pragmaOptionsAgda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PragmasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PreAgda.Syntax.Concrete.Operators.Parser
preActionAgda.TypeChecking.CheckInternal
PrecedenceAgda.Syntax.Fixity
PrecedenceKeyAgda.Syntax.Concrete.Operators.Parser.Monad
PrecedenceLevelAgda.Syntax.Common
PrecedenceStackAgda.Syntax.Fixity
preCompileAgda.Compiler.Backend
precomputedFreeVarsAgda.TypeChecking.Free.Precompute
PrecomputeFreeVarsAgda.TypeChecking.Free.Precompute
precomputeFreeVarsAgda.TypeChecking.Free.Precompute
precomputeFreeVars_Agda.TypeChecking.Free.Precompute
pRecordAgda.Syntax.Concrete.Pretty
pRecordDirectiveAgda.Syntax.Concrete.Pretty
PredAgda.TypeChecking.Primitive
PreferParenAgda.Syntax.Fixity
preferParenAgda.Syntax.Fixity
PreferParenlessAgda.Syntax.Fixity
preferParenlessAgda.Syntax.Fixity
PrefixAgda.Utils.List
prefixAgda.Compiler.JS.Compiler
PrefixDefAgda.Syntax.Common
prefixedThingsAgda.Utils.Pretty
PrefixNotationAgda.Syntax.Notation
PRemAgda.Syntax.Treeless, Agda.Compiler.Backend
PRem64Agda.Syntax.Treeless, Agda.Compiler.Backend
preModuleAgda.Compiler.Backend
PreOpAgda.Compiler.JS.Syntax
prependListAgda.Utils.List1
prependSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
preprocessAgda.TypeChecking.Positivity
PreRightsKAgda.Syntax.Concrete.Operators.Parser.Monad
PreScopeState 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
preserveInteractionIdsAgda.Syntax.Translation.AbstractToConcrete
preTraverseAPatternMAgda.Syntax.Abstract.Pattern
preTraverseCPatternMAgda.Syntax.Concrete.Pattern
preTraversePatternMAgda.Syntax.Internal.Pattern
PrettiesAgda.Compiler.JS.Pretty
prettiesAgda.Compiler.JS.Pretty
Pretty 
1 (Type/Class)Agda.Utils.Pretty
2 (Type/Class)Agda.Compiler.JS.Pretty
pretty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
prettyA 
1 (Function)Agda.Syntax.Abstract.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyAs 
1 (Function)Agda.Syntax.Abstract.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyAssignAgda.Utils.Pretty
prettyATopAgda.Syntax.Abstract.Pretty
prettyCallSiteAgda.Utils.CallStack
prettyCallStackAgda.Utils.CallStack
prettyCohesionAgda.Syntax.Concrete.Pretty
prettyConstraintAgda.TypeChecking.Pretty.Constraint
prettyConstraintsAgda.Interaction.BasicOps
PrettyContext 
1 (Type/Class)Agda.TypeChecking.Pretty
2 (Data Constructor)Agda.TypeChecking.Pretty
prettyDuplicateFieldsAgda.TypeChecking.Pretty.Warning
prettyErasedAgda.Syntax.Concrete.Pretty
prettyErrorAgda.TypeChecking.Errors
prettyErrorPartsAgda.TypeChecking.Unquote
prettyGuardedRhsAgda.Compiler.MAlonzo.Pretty
prettyHidingAgda.Syntax.Concrete.Pretty
prettyInterestingConstraintsAgda.TypeChecking.Pretty.Constraint
prettyList 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyList_ 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyMapAgda.Utils.Pretty
prettyMap_Agda.TypeChecking.CompiledClause
prettyNameSpaceAgda.Syntax.Scope.Base
prettyNotInScopeNamesAgda.TypeChecking.Pretty.Warning
prettyOpAppAgda.Syntax.Concrete.Pretty
prettyPrecAgda.Utils.Pretty
prettyPrecLevelSucsAgda.Syntax.Internal
prettyPrintAgda.Compiler.MAlonzo.Pretty
prettyQNameAgda.Compiler.MAlonzo.Pretty
prettyQuantityAgda.Syntax.Concrete.Pretty
prettyRAgda.TypeChecking.Pretty
prettyRecordFieldWarningAgda.TypeChecking.Pretty.Warning
prettyRelevanceAgda.Syntax.Concrete.Pretty
prettyRhsAgda.Compiler.MAlonzo.Pretty
prettySetAgda.Utils.Pretty
prettyShow 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
prettySrcLocAgda.Utils.CallStack
prettyTacticAgda.Syntax.Concrete.Pretty
prettyTactic'Agda.Syntax.Concrete.Pretty
PrettyTCMAgda.TypeChecking.Pretty
prettyTCMAgda.TypeChecking.Pretty
prettyTCMCtxAgda.TypeChecking.Pretty
prettyTCMPatternListAgda.TypeChecking.Pretty
prettyTCMPatternsAgda.TypeChecking.Pretty
PrettyTCMWithNodeAgda.TypeChecking.Pretty
prettyTCMWithNodeAgda.TypeChecking.Pretty
prettyTCWarningsAgda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
prettyTCWarnings'Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
prettyTooManyFieldsAgda.TypeChecking.Pretty.Warning
prettyTypeOfMetaAgda.Interaction.EmacsTop
prettyWarningAgda.TypeChecking.Pretty.Warning
prettyWarningModeErrorAgda.Interaction.Options.Warnings
prettyWhereAgda.Compiler.MAlonzo.Pretty
PreviousInputAgda.Syntax.Parser.Alex
PrimAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primAbsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAbsAbsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAbstrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primAgdaClauseAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaClauseAbsurdAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaClauseClauseAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataConstructorAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataDefAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionFunDefAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionPostulateAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionPrimitiveAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaDefinitionRecordDefAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaErrorPartAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaErrorPartNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaErrorPartStringAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaErrorPartTermAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaLitCharAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaLiteralAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaLitFloatAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaLitMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaLitNatAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaLitQNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaLitStringAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaLitWord64Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaPatAbsurdAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaPatConAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaPatDotAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaPatLitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaPatProjAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaPatternAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaPatVarAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaSortAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaSortInfAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaSortLitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaSortPropAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaSortPropLitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaSortSetAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaSortUnsupportedAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMBindAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMBlockOnMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMCatchErrorAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMCheckTypeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMCommitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMDebugPrintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMDeclareDefAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMDeclarePostulateAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMDefineFunAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMDontReduceDefsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMExecAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMExtendContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMFreshNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMGetContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMGetDefinitionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMGetTypeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMInContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMInferTypeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMIsMacroAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMNoConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMNormaliseAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMOnlyReduceDefsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMQuoteOmegaTermAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMQuoteTermAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMReduceAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMReturnAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMRunSpeculativeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMTypeErrorAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMUnifyAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMUnquoteTermAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMWithNormalisationAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTCMWithReconsParamsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermConAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermDefAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermExtLamAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermLamAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermLitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermPiAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermSortAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermUnsupportedAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAgdaTermVarAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primArgAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primArgArgAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primArgArgInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primArgInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAssocAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAssocLeftAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAssocNonAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primAssocRightAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primBodyAgda.Compiler.MAlonzo.Primitives
primBoolAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primCharAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primCharToNatInjectiveAgda.TypeChecking.Primitive
primClausesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primCompAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primCompiledAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primConIdAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primConsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primDepIMin'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
PrimeAgda.Utils.Suffix
primEqualityAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primEqualityNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primEquivAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primEquivFunAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primEquivProofAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primEraseEqualityAgda.TypeChecking.Primitive
primFaceForallAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primFaceForall'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primFalseAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primFixityAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primFixityFixityAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primFlatAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primFloatAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primFloatToWord64InjectiveAgda.TypeChecking.Primitive
primForceAgda.TypeChecking.Primitive
primForceLemmaAgda.TypeChecking.Primitive
primFromNatAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primFromNegAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primFromStringAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
PrimFun 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primFunAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primFunArityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primFunImplementationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primFunNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primGlueAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primGlue'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primHCompAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primHComp'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primHiddenAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primHidingAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIBinAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primIdAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIdElimAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIdElim'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primIdFace'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primIdJAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primIdPath'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primIMaxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIMax'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primIMinAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIMin'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
PrimImplAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primINegAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primINeg'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primInfAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primInstanceAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIntegerAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIntegerNegSucAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIntegerPosAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIntervalAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIntervalTypeAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primInvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primIOAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIOneAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIrrelevantAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIsOneAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIsOne1Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIsOne2Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primIsOneEmptyAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primItIsOneAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
Primitive 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.Syntax.Reflected
4 (Data Constructor)Agda.Syntax.Abstract
5 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PrimitiveBlockAgda.Syntax.Concrete.Definitions.Types
PrimitiveFunctionAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
primitiveFunctionsAgda.TypeChecking.Primitive
PrimitiveImplAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primitiveModulesAgda.Interaction.Options.Lenses
primitivesAgda.Compiler.JS.Compiler
PrimitiveSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PrimitiveTypeAgda.Interaction.Highlighting.Precise
primIZeroAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primJustAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primLevelAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primLevelMaxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primLevelSucAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primLevelZeroAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primListAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primLockUnivAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primLockUniv'Agda.TypeChecking.Primitive
primMaybeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primMetaToNatInjectiveAgda.TypeChecking.Primitive
primModalityAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primModalityConstructorAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
PrimNameAgda.Syntax.Scope.Base
primNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primNatAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNatDivSucAuxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNatEqualityAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNatLessAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNatMinusAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNatModSucAuxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNatPlusAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNatTimesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNilAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primNothingAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primPartialAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primPartial'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primPartialPAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primPartialP'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primPathAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primPathPAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primPOrAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primPrecedenceAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primPrecRelatedAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primPrecUnrelatedAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primPropAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primQNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primQNameToWord64sInjectiveAgda.TypeChecking.Primitive
primQuantityAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primQuantity0Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primQuantityωAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primReflAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primRelevanceAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primRelevantAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primRewriteAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSetAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSetOmegaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSharpAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSigmaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSizeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSizeInfAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSizeLtAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSizeMaxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSizeSucAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSizeUnivAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
primSSetOmegaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primStrictSetAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primStringAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primStringFromListInjectiveAgda.TypeChecking.Primitive
primStringToListInjectiveAgda.TypeChecking.Primitive
primSubAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSubInAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSubOutAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primSubOut'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primSucAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
PrimTermAgda.TypeChecking.Primitive
primTermAgda.TypeChecking.Primitive
primTransAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primTrans'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primTransHCompAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
primTranspProofAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primTrueAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
PrimTypeAgda.TypeChecking.Primitive
primTypeAgda.TypeChecking.Primitive
primUnitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primUnitUnitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primVisibleAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primWord64Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
primWord64ToNatInjectiveAgda.TypeChecking.Primitive
primZeroAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
prim_glueAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
prim_glue'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
prim_glueUAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
prim_glueU'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
prim_unglueAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
prim_unglue'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
prim_unglueUAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
prim_unglueU'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
PrincipalArgTypeMetas 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
printAgda.TypeChecking.Monad.Benchmark
printAgdaDirAgda.Main
printErrorInfoAgda.Interaction.Highlighting.Generate
printHighlightingInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace, Agda.Interaction.Highlighting.Generate
printLocalsAgda.Syntax.Scope.Monad
PrintRange 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
printScopeAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
printStatisticsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
printSyntaxInfoAgda.Interaction.Highlighting.Generate
printUnsolvedInfoAgda.Interaction.Highlighting.Generate
printUsageAgda.Main
printVersionAgda.Main
Prio 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
prioAbsurdLambdaAgda.Auto.SearchControl
prioCompareArgListAgda.Auto.SearchControl
prioCompBetaAgda.Auto.SearchControl
prioCompBetaStructuredAgda.Auto.SearchControl
prioCompChoiceAgda.Auto.SearchControl
prioCompCopyAgda.Auto.SearchControl
prioCompIotaAgda.Auto.SearchControl
prioCompUnifAgda.Auto.SearchControl
prioInferredTypeUnknownAgda.Auto.SearchControl
PrioMeta 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
prioNoAgda.Auto.SearchControl
prioNoIotaAgda.Auto.SearchControl
prioProjIndexAgda.Auto.SearchControl
prioTypecheckAgda.Auto.SearchControl
prioTypecheckArgListAgda.Auto.SearchControl
prioTypeUnknownAgda.Auto.SearchControl
PrivateAgda.Syntax.Concrete
PrivateAccessAgda.Syntax.Common
PrivateNSAgda.Syntax.Scope.Base
Problem 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
ProblemConstraintAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
problemContAgda.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
problemEqsAgda.TypeChecking.Rules.LHS.Problem
ProblemId 
1 (Type/Class)Agda.Syntax.Common, Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Common, Agda.Syntax.Internal
problemInPatAgda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
problemInPatsAgda.TypeChecking.Rules.LHS.Problem
problemInstAgda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
problemRestPatsAgda.TypeChecking.Rules.LHS.Problem
problemType 
1 (Function)Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
2 (Function)Agda.TypeChecking.MetaVars
ProcessorAgda.Syntax.Parser.Literate
productOfEdgesInBoundedWalkAgda.TypeChecking.Positivity.Occurrence
ProductsAgda.Utils.TypeLevel
Proj 
1 (Data Constructor)Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract
projArgInfoAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
projCaseAgda.TypeChecking.CompiledClause
projDropParsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
projDropParsApplyAgda.TypeChecking.Substitute
ProjectConfig 
1 (Type/Class)Agda.Interaction.Library.Base, Agda.Interaction.Library
2 (Data Constructor)Agda.Interaction.Library.Base, Agda.Interaction.Library
ProjectedVar 
1 (Type/Class)Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
2 (Data Constructor)Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
Projection 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
projectionArgsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
ProjectionLikenessAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
ProjectionReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ProjectionView 
1 (Type/Class)Agda.TypeChecking.ProjectionLike
2 (Data Constructor)Agda.TypeChecking.ProjectionLike
projectRootAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
projectTypedAgda.TypeChecking.Records
ProjEliminatorAgda.TypeChecking.ProjectionLike
projFromTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
projIndexAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ProjLams 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
projLamsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
projOrigAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ProjOriginAgda.Syntax.Common
ProjP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Reflected
3 (Data Constructor)Agda.Syntax.Abstract
projPatternsAgda.TypeChecking.CompiledClause
ProjPostfixAgda.Syntax.Common
ProjPrefixAgda.Syntax.Common
projProperAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ProjSystemAgda.Syntax.Common
ProjTAgda.TypeChecking.Records
projTFieldAgda.TypeChecking.Records
projTRecAgda.TypeChecking.Records
projUseSizeLtAgda.Termination.Monad
ProjVarAgda.TypeChecking.MetaVars
projViewAgda.TypeChecking.ProjectionLike
projViewProjAgda.TypeChecking.ProjectionLike
projViewSelfAgda.TypeChecking.ProjectionLike
projViewSpineAgda.TypeChecking.ProjectionLike
Prop 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Syntax.Internal
propagatePrioAgda.Auto.NarrowingSearch
properlyMatchingAgda.Syntax.Internal
properlyMatching'Agda.Syntax.Internal
properSplitAgda.TypeChecking.CompiledClause.Compile
PropLitSAgda.Syntax.Reflected
PropMustBeSingletonAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PropSAgda.Syntax.Reflected
prProjsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
pruneAgda.TypeChecking.MetaVars.Occurs
PrunedEverythingAgda.TypeChecking.MetaVars.Occurs
PrunedNothingAgda.TypeChecking.MetaVars.Occurs
PrunedSomethingAgda.TypeChecking.MetaVars.Occurs
PruneResultAgda.TypeChecking.MetaVars.Occurs
PSeqAgda.Syntax.Treeless, Agda.Compiler.Backend
pshow 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
PSizeUnivAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PStateAgda.Syntax.Parser.Monad
PStrAgda.Utils.Pretty
PSubAgda.Syntax.Treeless, Agda.Compiler.Backend
PSub64Agda.Syntax.Treeless, Agda.Compiler.Backend
PSyn 
1 (Type/Class)Agda.Syntax.Internal.Names
2 (Data Constructor)Agda.Syntax.Internal.Names
PTermAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ptextAgda.Utils.Pretty
PtrAgda.Utils.Pointer
PTSInstanceAgda.Interaction.Base
ptsRuleAgda.TypeChecking.Sort
ptsRule'Agda.TypeChecking.Sort
PTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
PublicAccessAgda.Syntax.Common
publicModulesAgda.Syntax.Scope.Base
publicNamesAgda.Syntax.Scope.Base
PublicNSAgda.Syntax.Scope.Base
publicOpenAgda.Syntax.Common
punctuate 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
pureCompareAsAgda.TypeChecking.Conversion.Pure
PureConversionT 
1 (Type/Class)Agda.TypeChecking.Conversion.Pure
2 (Data Constructor)Agda.TypeChecking.Conversion.Pure
pureEqualTermAgda.TypeChecking.Conversion.Pure
pureEqualTypeAgda.TypeChecking.Conversion.Pure
PureTCMAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Pure
pureTCMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
purgeNonvariantAgda.TypeChecking.Polarity
pushBlockAgda.Syntax.Parser.Monad
pushLexStateAgda.Syntax.Parser.Monad
pushPrecedenceAgda.Syntax.Fixity
putAbsoluteIncludePathsAgda.Interaction.Options.Lenses
putAllConstraintsToSleepAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
putAllowedReductionsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
putBenchmarkAgda.Utils.Benchmark
putConstraintsToSleepAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
putIncludePathsAgda.Interaction.Options.Lenses
putPersistentVerbosityAgda.Interaction.Options.Lenses
putResponse 
1 (Function)Agda.Interaction.EmacsCommand
2 (Function)Agda.Interaction.InteractionTop
putSafeModeAgda.Interaction.Options.Lenses
putTCAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
putVerbosityAgda.Interaction.Options.Lenses
PVar 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
pvIndexAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
PWildCardAgda.Utils.Haskell.Syntax
pwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty