Agda-2.6.2.2.20221128: 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.Concrete.Operators.Parser
4 (Function)Agda.Syntax.Parser.Monad
5 (Function)Agda.Syntax.Parser
parseAndDoAtToplevelAgda.Interaction.InteractionTop
parseApplicationAgda.Syntax.Concrete.Operators
parseArgsAgda.Auto.Options
parseBackendOptionsAgda.Compiler.Backend
parseCohesionAgda.Syntax.Parser.Monad
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
parseIOTCMAgda.Interaction.Base
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.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
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.Base, Agda.TypeChecking.Primitive
PathConsAgda.TypeChecking.Rules.Data
pathLevelAgda.Syntax.Internal
pathLhsAgda.Syntax.Internal
pathNameAgda.Syntax.Internal
pathRhsAgda.Syntax.Internal
pathSortAgda.Syntax.Internal
pathTelescopeAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
pathTelescope'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PathTypeAgda.Syntax.Internal
pathTypeAgda.Syntax.Internal
pathUnviewAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PathViewAgda.Syntax.Internal
pathViewAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pathView'Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pathViewAsPiAgda.TypeChecking.Telescope
pathViewAsPi'Agda.TypeChecking.Telescope
pathViewAsPi'whnfAgda.TypeChecking.Telescope
PatInfoAgda.Syntax.Info
patmMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
patmRemainderAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
PatProjAgda.Auto.Syntax
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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
PatternSynDefSAgda.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.TypeChecking.Monad, Agda.Compiler.Backend
patternViolation'Agda.TypeChecking.MetaVars.Occurs
PattPartAgda.TypeChecking.Unquote
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.TypeChecking.Monad, Agda.Compiler.Backend
PConstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pDomAgda.Syntax.Internal
PDoubleBlockedAgda.Auto.NarrowingSearch
PEConAppAgda.Auto.Typecheck
PElimsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
performedSimplification'Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
PersistentTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Concrete
2 (Data Constructor)Agda.Auto.Syntax
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.TypeChecking.Monad, Agda.Compiler.Backend
PInfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PiNotLamAgda.TypeChecking.Rules.Term
PIntervalUnivAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
piOrPathAgda.TypeChecking.Telescope
PIrrPatAgda.Utils.Haskell.Syntax
PiSortAgda.Syntax.Internal
piSortAgda.TypeChecking.Substitute
piSort'Agda.TypeChecking.Substitute
PITo64Agda.Syntax.Treeless, Agda.Compiler.Backend
PiView 
1 (Type/Class)Agda.Syntax.Abstract.Views
2 (Data Constructor)Agda.Syntax.Abstract.Views
piViewAgda.Syntax.Abstract.Views
PlaceholderAgda.Syntax.Common
placeholderAgda.Syntax.Concrete.Operators.Parser
PlainJSAgda.Compiler.JS.Syntax
PLamAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PLitAgda.Utils.Haskell.Syntax
PLockUnivAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Concrete.Fixity
2 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
polaritiesFromAssignmentsAgda.TypeChecking.SizedTypes.Syntax
Polarity 
1 (Type/Class)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
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
postponeInstanceConstraintsAgda.TypeChecking.InstanceArguments
postponeTypeCheckingProblemAgda.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
postTraverseAPatternMAgda.Syntax.Abstract.Pattern
postTraverseCPatternMAgda.Syntax.Concrete.Pattern
postTraversePatternMAgda.Syntax.Internal.Pattern
Postulate 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Auto.Syntax
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
PostulateBlockAgda.Syntax.Concrete.Definitions.Types
PPiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pPi'Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
PPropAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
PragmaSAgda.Syntax.Abstract
PragmasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
prettyFinitenessAgda.Syntax.Concrete.Pretty
prettyGuardedRhsAgda.Compiler.MAlonzo.Pretty
prettyHidingAgda.Syntax.Concrete.Pretty
prettyInstalledLibrariesAgda.Interaction.Library.Base
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
prettyRangeConstraintAgda.TypeChecking.Pretty.Constraint
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.TypeChecking.Monad, Agda.Compiler.Backend
primAbsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbsAbsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseAbsurdAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseClauseAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionDataConstructorAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionDataDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionFunDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionPostulateAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionPrimitiveAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionRecordDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartPattAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartStringAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitCharAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLiteralAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitFloatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitMetaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitNatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitQNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitStringAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitWord64Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaMetaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatAbsurdAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatConAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatDotAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatLitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatProjAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatternAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatVarAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortInfAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortLitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortPropAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortPropLitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortSetAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortUnsupportedAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMBindAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMBlockOnMetaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCatchErrorAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCheckTypeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCommitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDebugPrintAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclareDataAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclareDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclarePostulateAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDefineDataAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDefineFunAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDontReduceDefsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMExecAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMExtendContextAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMFormatErrorPartsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMFreshNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetContextAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetDefinitionAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetInstancesAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetTypeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMInContextAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMInferTypeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMIsMacroAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMNoConstraintsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMNormaliseAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMOnlyReduceDefsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMQuoteOmegaTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMQuoteTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMReduceAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMReturnAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMRunSpeculativeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMTypeErrorAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMUnifyAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMUnquoteTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithNormalisationAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithReconsParamsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermConAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermExtLamAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermLamAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermLitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermMetaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermPiAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermSortAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermUnsupportedAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermVarAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgArgAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgArgInfoAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgInfoAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocLeftAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocNonAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocRightAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primBodyAgda.Compiler.MAlonzo.Primitives
primBoolAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCharAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCharToNatInjectiveAgda.TypeChecking.Primitive
primClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCompAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primConIdAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primConId'Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primConsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primDepIMin'Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimeAgda.Utils.Suffix
primEqualityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEqualityNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivFunAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivProofAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEraseEqualityAgda.TypeChecking.Primitive
primFaceForallAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFaceForall'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primFalseAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFixityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFixityFixityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFlatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFloatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFloatToWord64InjectiveAgda.TypeChecking.Primitive
primForceAgda.TypeChecking.Primitive
primForceLemmaAgda.TypeChecking.Primitive
primFromNatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFromNegAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFromStringAgda.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
primFunAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunArityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunImplementationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlueAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlue'Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primHCompAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHComp'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primHiddenAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHidingAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIdAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIdElimAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIdElim'Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIdFace'Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIdPath'Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIMaxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMax'Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIMinAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMin'Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimImplAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primINegAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primINeg'Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primInfAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInstanceAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerNegSucAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerPosAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntervalAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntervalTypeAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIntervalUnivAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIOAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIOneAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIrrelevantAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOneAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne1Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne2Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOneEmptyAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primItIsOneAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveBlockAgda.Syntax.Concrete.Definitions.Types
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
PrimitiveDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveFunctionAgda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
primitiveFunctionsAgda.TypeChecking.Primitive
PrimitiveImplAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primitiveModulesAgda.Interaction.Options.Lenses
PrimitiveSAgda.Syntax.Abstract
primitivesAgda.Compiler.JS.Compiler
PrimitiveSortAgda.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
PrimitiveSortDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveTypeAgda.Interaction.Highlighting.Precise
primIZeroAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primJustAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelMaxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelSucAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelZeroAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primListAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLockUnivAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLockUniv'Agda.TypeChecking.Primitive
primMaybeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primMetaToNatInjectiveAgda.TypeChecking.Primitive
primModalityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primModalityConstructorAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNameAgda.Syntax.Scope.Base
primNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatDivSucAuxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatEqualityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatLessAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatMinusAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatModSucAuxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatPlusAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatTimesAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNilAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNothingAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartialAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartial'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPartialPAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartialP'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPathAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPathPAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPOrAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPrecedenceAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPrecRelatedAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPrecUnrelatedAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPropAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQNameToWord64sInjectiveAgda.TypeChecking.Primitive
primQuantityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQuantity0Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQuantityωAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primReflAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRelevanceAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRelevantAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSetAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSetOmegaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSharpAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSigmaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeInfAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeLtAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeMaxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeSucAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeUnivAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSortNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSortSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSSetOmegaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStrictSetAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStringAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStringFromListInjectiveAgda.TypeChecking.Primitive
primStringToListInjectiveAgda.TypeChecking.Primitive
primSubAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubInAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubOutAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubOut'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primSucAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimTermAgda.TypeChecking.Primitive
primTermAgda.TypeChecking.Primitive
primTransAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrans'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primTransHCompAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primTranspProofAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrueAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimTypeAgda.TypeChecking.Primitive
primTypeAgda.TypeChecking.Primitive
primUnitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primUnitUnitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primVisibleAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primWord64Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primWord64ToNatInjectiveAgda.TypeChecking.Primitive
primZeroAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glueAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glue'Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
prim_glueUAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glueU'Agda.TypeChecking.Primitive.Cubical.HCompU, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
prim_unglueAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglue'Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
prim_unglueUAgda.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
printAgda.TypeChecking.Monad.Benchmark
printAgdaDirAgda.Main
printErrorInfoAgda.Interaction.Highlighting.Generate
printHighlightingInfoAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend
printLocalsAgda.Syntax.Scope.Monad
PrintRange 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
printScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
printStatisticsAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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
ProfileOptionAgda.Utils.ProfileOptions
ProfileOptionsAgda.Utils.ProfileOptions
profileOptionsFromListAgda.Utils.ProfileOptions
profileOptionsToListAgda.Utils.ProfileOptions
Proj 
1 (Data Constructor)Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract
projArgInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projCaseAgda.TypeChecking.CompiledClause
projDropParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.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
projectionArgsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionLikenessAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
ProjectionLikenessMissingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionView 
1 (Type/Class)Agda.TypeChecking.ProjectionLike
2 (Data Constructor)Agda.TypeChecking.ProjectionLike
projectRootAgda.Syntax.TopLevelModuleName
projectTypedAgda.TypeChecking.Records
ProjEliminatorAgda.TypeChecking.ProjectionLike
projFromTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projIndexAgda.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
projLamsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projOrigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
PropSAgda.Syntax.Reflected
prProjsAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
PSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PSSetAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
ptextAgda.Utils.Pretty
PtrAgda.Utils.Pointer
PTSInstanceAgda.Interaction.Base
ptsRuleAgda.TypeChecking.Sort
ptsRule'Agda.TypeChecking.Sort
PTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Pure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pureTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
purgeNonvariantAgda.TypeChecking.Polarity
pushBlockAgda.Syntax.Parser.Monad
pushLexStateAgda.Syntax.Parser.Monad
pushPrecedenceAgda.Syntax.Fixity
putAbsoluteIncludePathsAgda.Interaction.Options.Lenses
putAllConstraintsToSleepAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putAllowedReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putBenchmarkAgda.Utils.Benchmark
putConstraintsToSleepAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
putVerbosityAgda.Interaction.Options.Lenses
PVar 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pvIndexAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PWildCardAgda.Utils.Haskell.Syntax
pwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty