| PageMode | Agda.Utils.Pretty |
| Pair | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| pairwiseFilter | Agda.Compiler.Epic.Interface |
| Paren | Agda.Syntax.Concrete |
| paren | Agda.Syntax.Concrete.Operators |
| parened | Agda.Compiler.JS.Parser |
| ParenP | Agda.Syntax.Concrete |
| parens | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| ParenV | Agda.Syntax.Concrete.Operators.Parser |
| parse | |
| 1 (Function) | Agda.Utils.ReadP |
| 2 (Function) | Agda.Compiler.JS.Parser |
| 3 (Function) | Agda.Syntax.Parser.Monad |
| 4 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| parse' | Agda.Utils.ReadP |
| parseAndDoAtToplevel | Agda.Interaction.GhciTop |
| parseApplication | Agda.Syntax.Concrete.Operators |
| ParseError | |
| 1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| parseError | Agda.Syntax.Parser.Monad |
| parseErrorAt | Agda.Syntax.Parser.Monad |
| parseExpr | |
| 1 (Function) | Agda.Interaction.BasicOps |
| 2 (Function) | Agda.Interaction.CommandLine.CommandLine |
| parseExprIn | Agda.Interaction.BasicOps |
| ParseFailed | Agda.Syntax.Parser.Monad |
| parseFile | Agda.Syntax.Parser.Monad |
| parseFile' | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| ParseFlags | |
| 1 (Type/Class) | Agda.Syntax.Parser.Monad |
| 2 (Data Constructor) | Agda.Syntax.Parser.Monad |
| parseFlags | Agda.Syntax.Parser.Monad |
| parseInp | Agda.Syntax.Parser.Monad |
| parseKeepComments | Agda.Syntax.Parser.Monad |
| parseLastPos | Agda.Syntax.Parser.Monad |
| parseLayout | Agda.Syntax.Parser.Monad |
| parseLexState | Agda.Syntax.Parser.Monad |
| parseLHS | Agda.Syntax.Concrete.Operators |
| parseLiterate | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| ParseOk | Agda.Syntax.Parser.Monad |
| parsePluginOptions | Agda.Interaction.Options |
| parsePos | Agda.Syntax.Parser.Monad |
| parsePosString | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| parsePragmaOptions | Agda.Interaction.Options |
| parsePrevChar | Agda.Syntax.Parser.Monad |
| parsePrevToken | Agda.Syntax.Parser.Monad |
| Parser | |
| 1 (Type/Class) | Agda.Compiler.JS.Parser |
| 2 (Type/Class) | Agda.Syntax.Parser.Monad |
| 3 (Type/Class) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| ParseResult | Agda.Syntax.Parser.Monad |
| parseStandardOptions | Agda.Interaction.Options |
| ParseState | Agda.Syntax.Parser.Monad |
| partP | Agda.Syntax.Concrete.Operators.Parser |
| Pat | Agda.Auto.Syntax |
| PatConApp | Agda.Auto.Syntax |
| PatExp | Agda.Auto.Syntax |
| PatInfo | Agda.Syntax.Info |
| PatName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| PatRange | Agda.Syntax.Info |
| pats | Agda.Compiler.JS.Case |
| PatSource | Agda.Syntax.Info |
| patsToTerms | Agda.TypeChecking.With |
| Patt | Agda.Compiler.JS.Case |
| Pattern | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Internal |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| pattern | Agda.Compiler.JS.Compiler |
| Pattern' | Agda.Syntax.Abstract |
| PatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| patternHead | Agda.Syntax.Concrete |
| patternNames | Agda.Syntax.Concrete |
| PatternShadowsConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| patternToTerm | Agda.Compiler.Epic.Injection |
| patternViolation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PatVar | Agda.Auto.Syntax |
| PB | Agda.Auto.NarrowingSearch |
| PBlocked | Agda.Auto.NarrowingSearch |
| pconName | Agda.Compiler.MAlonzo.Primitives |
| PConstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PDoubleBlocked | Agda.Auto.NarrowingSearch |
| PEConApp | Agda.Auto.Typecheck |
| PENo | Agda.Auto.Typecheck |
| performKill | Agda.TypeChecking.MetaVars.Occurs |
| Perm | Agda.Utils.Permutation |
| Permutation | Agda.Utils.Permutation |
| permute | Agda.Utils.Permutation |
| PersistentTCSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PersistentTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PEval | Agda.Auto.Typecheck |
| pfail | Agda.Utils.ReadP |
| pHidden | Agda.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.Abstract |
| piAbstractTerm | Agda.TypeChecking.Abstract |
| piApply | Agda.TypeChecking.Substitute |
| piApplyM | Agda.TypeChecking.Telescope |
| piApplyM' | Agda.Compiler.Epic.Forcing |
| piBrackets | Agda.Syntax.Fixity |
| pickid | Agda.Auto.Typecheck |
| piFreq | Agda.TypeChecking.Test.Generators |
| PiHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PiNotLam | Agda.TypeChecking.Rules.Term |
| PiSh | Agda.TypeChecking.Rules.LHS.Unify |
| plugHole | Agda.Syntax.Internal.Pattern |
| Plus | Agda.Syntax.Internal |
| PlusLevel | Agda.Syntax.Internal |
| Pn | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| polarities | Agda.TypeChecking.Polarity |
| Polarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| polarity | Agda.TypeChecking.Polarity |
| pop | Agda.Compiler.JS.Case |
| popContext | Agda.Syntax.Parser.Monad |
| popLexState | Agda.Syntax.Parser.Monad |
| popMapS | Agda.Auto.Convert |
| posCol | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| Position | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| positionInvariant | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| Positive | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| positive | Agda.Utils.TestHelpers |
| positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| posLine | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| posPos | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| Possibly | Agda.TypeChecking.Rules.LHS.Unify |
| postfixP | Agda.Syntax.Concrete.Operators.Parser |
| postop | Agda.Syntax.Concrete.Operators.Parser |
| posToRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| PostponedTypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| postponeTypeCheckingProblem | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| postponeTypeCheckingProblem_ | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| Postulate | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| Pragma | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| PragmaOptions | |
| 1 (Type/Class) | Agda.Interaction.Options |
| 2 (Data Constructor) | Agda.Interaction.Options |
| pragmaOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Precedence | Agda.Syntax.Fixity |
| Pred | Agda.TypeChecking.Primitive |
| Prefix | Agda.Utils.List |
| prefix | Agda.Compiler.JS.Compiler |
| PrefixDef | Agda.Syntax.Common |
| prefixP | Agda.Syntax.Concrete.Operators.Parser |
| pRelevance | Agda.Syntax.Concrete.Pretty |
| preMeta | Agda.Interaction.GhciTop |
| PreOp | Agda.Compiler.JS.Syntax |
| preop | |
| 1 (Function) | Agda.Compiler.JS.Parser |
| 2 (Function) | Agda.Syntax.Concrete.Operators.Parser |
| Pretties | Agda.Compiler.JS.Pretty |
| pretties | Agda.Compiler.JS.Pretty |
| Pretty | |
| 1 (Type/Class) | Agda.Utils.Pretty |
| 2 (Type/Class) | Agda.Compiler.JS.Pretty |
| pretty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| 3 (Function) | Agda.TypeChecking.Pretty |
| prettyA | |
| 1 (Function) | Agda.Syntax.Abstract.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyATop | Agda.Syntax.Abstract.Pretty |
| prettyBehaviour | Agda.Termination.CallGraph |
| PrettyContext | |
| 1 (Type/Class) | Agda.TypeChecking.Pretty |
| 2 (Data Constructor) | Agda.TypeChecking.Pretty |
| prettyContext | Agda.Interaction.GhciTop |
| prettyEpic | Agda.Compiler.Epic.Epic |
| prettyEpicFun | Agda.Compiler.Epic.Epic |
| prettyError | Agda.TypeChecking.Errors, Agda.Interaction.GhciTop |
| prettyGraph | Agda.TypeChecking.Positivity |
| prettyList | Agda.TypeChecking.Pretty |
| prettyPrec | Agda.Utils.Pretty |
| prettyPrint | Agda.Compiler.MAlonzo.Pretty |
| PrettyTCM | Agda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop |
| prettyTCM | Agda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop |
| prettyTypeOfMeta | Agda.Interaction.GhciTop |
| preUscore | Agda.Interaction.GhciTop |
| PreviousInput | Agda.Syntax.Parser.Alex |
| prFalse | Agda.Compiler.Epic.Primitive |
| Prim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primAgdaDataDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinition | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionDataConstructor | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionDataDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionFunDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionPostulate | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionPrimitive | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionRecordDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaFunDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaRecordDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaSort | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortLit | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortSet | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortUnsupported | Agda.TypeChecking.Monad.Builtin |
| primAgdaTerm | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermCon | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermLam | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermPi | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermSort | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermUnsupported | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermVar | Agda.TypeChecking.Monad.Builtin |
| primAgdaType | Agda.TypeChecking.Monad.Builtin |
| primAgdaTypeEl | Agda.TypeChecking.Monad.Builtin |
| primArg | Agda.TypeChecking.Monad.Builtin |
| primArgArg | Agda.TypeChecking.Monad.Builtin |
| primBody | Agda.Compiler.MAlonzo.Primitives |
| primBool | Agda.TypeChecking.Monad.Builtin |
| primChar | Agda.TypeChecking.Monad.Builtin |
| primClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primCons | Agda.TypeChecking.Monad.Builtin |
| primDataConstructors | Agda.TypeChecking.Primitive |
| Prime | Agda.Utils.Suffix |
| primEquality | Agda.TypeChecking.Monad.Builtin |
| primExpr | Agda.Compiler.Epic.Primitive |
| primFalse | Agda.TypeChecking.Monad.Builtin |
| primFlat | Agda.TypeChecking.Monad.Builtin |
| primFloat | Agda.TypeChecking.Monad.Builtin |
| PrimFun | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primFun | Agda.Compiler.Epic.Primitive |
| primFunArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primFunImplementation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primFunName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primHidden | Agda.TypeChecking.Monad.Builtin |
| primHiding | Agda.TypeChecking.Monad.Builtin |
| PrimImpl | Agda.TypeChecking.Primitive |
| primInf | Agda.TypeChecking.Monad.Builtin |
| primInstance | Agda.TypeChecking.Monad.Builtin |
| primInteger | Agda.TypeChecking.Monad.Builtin |
| primIO | Agda.TypeChecking.Monad.Builtin |
| primIrrelevant | Agda.TypeChecking.Monad.Builtin |
| Primitive | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PrimitiveFunction | Agda.Syntax.Concrete.Definitions |
| primitiveFunctions | Agda.TypeChecking.Primitive |
| PrimitiveImpl | Agda.TypeChecking.Primitive |
| PrimitiveType | Agda.Interaction.Highlighting.Precise |
| primitivise | Agda.Compiler.Epic.Primitive |
| primLevel | Agda.TypeChecking.Monad.Builtin |
| primLevelMax | Agda.TypeChecking.Monad.Builtin |
| primLevelSuc | Agda.TypeChecking.Monad.Builtin |
| primLevelZero | Agda.TypeChecking.Monad.Builtin |
| primList | Agda.TypeChecking.Monad.Builtin |
| primName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primNat | Agda.TypeChecking.Monad.Builtin |
| primNatCaseZD | Agda.Compiler.Epic.Primitive |
| primNatCaseZS | Agda.Compiler.Epic.Primitive |
| primNatDivSucAux | Agda.TypeChecking.Monad.Builtin |
| primNatEquality | Agda.TypeChecking.Monad.Builtin |
| primNatLess | Agda.TypeChecking.Monad.Builtin |
| primNatMinus | Agda.TypeChecking.Monad.Builtin |
| primNatModSucAux | Agda.TypeChecking.Monad.Builtin |
| primNatPlus | Agda.TypeChecking.Monad.Builtin |
| primNatTimes | Agda.TypeChecking.Monad.Builtin |
| primNil | Agda.TypeChecking.Monad.Builtin |
| primQName | Agda.TypeChecking.Monad.Builtin |
| primQNameDefinition | Agda.TypeChecking.Primitive |
| primQNameType | Agda.TypeChecking.Primitive |
| primRefl | Agda.TypeChecking.Monad.Builtin |
| primRelevant | Agda.TypeChecking.Monad.Builtin |
| primRelvance | Agda.TypeChecking.Monad.Builtin |
| primSharp | Agda.TypeChecking.Monad.Builtin |
| primSize | Agda.TypeChecking.Monad.Builtin |
| primSizeInf | Agda.TypeChecking.Monad.Builtin |
| primSizeSuc | Agda.TypeChecking.Monad.Builtin |
| primString | Agda.TypeChecking.Monad.Builtin |
| primSuc | Agda.TypeChecking.Monad.Builtin |
| PrimTag | Agda.Compiler.Epic.Interface |
| PrimTerm | Agda.TypeChecking.Primitive |
| primTerm | Agda.TypeChecking.Primitive |
| PrimTF | Agda.Compiler.Epic.Primitive |
| PrimTransform | Agda.Compiler.Epic.Primitive |
| primTrue | Agda.TypeChecking.Monad.Builtin |
| primTrustMe | Agda.TypeChecking.Primitive |
| PrimType | Agda.TypeChecking.Primitive |
| primType | Agda.TypeChecking.Primitive |
| primVisible | Agda.TypeChecking.Monad.Builtin |
| primZero | Agda.TypeChecking.Monad.Builtin |
| print | Agda.Utils.IO.Locale |
| printTestCase | Agda.Utils.QuickCheck |
| printUsage | Agda.Main |
| printVersion | Agda.Main |
| Prio | Agda.Auto.NarrowingSearch |
| prioAbsurdLambda | Agda.Auto.SearchControl |
| prioCompareArgList | Agda.Auto.SearchControl |
| prioCompBeta | Agda.Auto.SearchControl |
| prioCompBetaStructured | Agda.Auto.SearchControl |
| prioCompChoice | Agda.Auto.SearchControl |
| prioCompCopy | Agda.Auto.SearchControl |
| prioCompIota | Agda.Auto.SearchControl |
| prioCompUnif | Agda.Auto.SearchControl |
| prioInferredTypeUnknown | Agda.Auto.SearchControl |
| PrioMeta | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| prioNo | Agda.Auto.SearchControl |
| prioNoIota | Agda.Auto.SearchControl |
| prioProjIndex | Agda.Auto.SearchControl |
| prioTypecheck | Agda.Auto.SearchControl |
| prioTypecheckArgList | Agda.Auto.SearchControl |
| prioTypeUnknown | Agda.Auto.SearchControl |
| Private | Agda.Syntax.Concrete |
| PrivateAccess | Agda.Syntax.Common |
| PrivateNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| prNatEquality | Agda.Compiler.Epic.Primitive |
| Problem | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| Problem' | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ProblemId | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| problemInPat | Agda.TypeChecking.Rules.LHS.Problem |
| problemOutPat | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemPart | Agda.TypeChecking.Rules.LHS.Problem |
| problemTel | Agda.TypeChecking.Rules.LHS.Problem |
| Proj | Agda.Syntax.Internal |
| ProjectRoot | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| projectRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| promote | Agda.Utils.QuickCheck |
| proofIrrelevance | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Prop | |
| 1 (Type/Class) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Auto.NarrowingSearch |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| prop | Agda.Syntax.Internal |
| propagatePrio | Agda.Auto.NarrowingSearch |
| Property | Agda.Utils.QuickCheck |
| property | Agda.Utils.QuickCheck |
| propFreq | Agda.TypeChecking.Test.Generators |
| PropMustBeSingleton | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| prop_disjoint | Agda.Utils.Warshall |
| prop_distinct_fastDistinct | Agda.Utils.List |
| prop_extractNthElement | Agda.Utils.List |
| prop_flattenTelInv | Agda.TypeChecking.Tests |
| prop_flattenTelScope | Agda.TypeChecking.Tests |
| prop_genericElemIndex | Agda.Utils.List |
| prop_groupBy' | Agda.Utils.List |
| prop_path | Agda.Utils.Warshall |
| prop_reorderTelStable | Agda.TypeChecking.Tests |
| prop_smaller | Agda.Utils.Warshall |
| prop_splitTelescopePermScope | Agda.TypeChecking.Tests |
| prop_splitTelescopeScope | Agda.TypeChecking.Tests |
| prop_stable | Agda.Utils.Warshall |
| prop_telToListInv | Agda.TypeChecking.Tests |
| prop_uniqBy | Agda.Utils.List |
| prop_wellScopedVars | Agda.TypeChecking.Test.Generators |
| prop_zipWith' | Agda.Utils.List |
| prPred | Agda.Compiler.Epic.Primitive |
| prSuc | Agda.Compiler.Epic.Primitive |
| prTrue | Agda.Compiler.Epic.Primitive |
| prune | Agda.TypeChecking.MetaVars.Occurs |
| PrunedEverything | Agda.TypeChecking.MetaVars.Occurs |
| PrunedNothing | Agda.TypeChecking.MetaVars.Occurs |
| PrunedSomething | Agda.TypeChecking.MetaVars.Occurs |
| PruneResult | Agda.TypeChecking.MetaVars.Occurs |
| prZero | Agda.Compiler.Epic.Primitive |
| PState | Agda.Syntax.Parser.Monad |
| PStr | Agda.Utils.Pretty |
| ptext | Agda.Utils.Pretty |
| Ptr | Agda.Utils.Pointer |
| PublicAccess | Agda.Syntax.Common |
| publicModules | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| PublicNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| publicOpen | Agda.Syntax.Concrete |
| punct | Agda.Compiler.JS.Parser |
| punctuate | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| pureTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| pushContext | Agda.Syntax.Parser.Monad |
| pushCurrentContext | Agda.Syntax.Parser.Monad |
| pushLexState | Agda.Syntax.Parser.Monad |
| putConArity | Agda.Compiler.Epic.CompileState |
| putConstrTag | Agda.Compiler.Epic.CompileState |
| putDelayed | Agda.Compiler.Epic.CompileState |
| putForcedArgs | Agda.Compiler.Epic.CompileState |
| putMain | Agda.Compiler.Epic.CompileState |
| putResponse | Agda.Interaction.EmacsCommand |
| putStr | Agda.Utils.IO.Locale |
| putStrLn | Agda.Utils.IO.Locale |
| pwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |