| PageMode | Agda.Utils.Pretty |
| par | Agda.Auto.Print |
| Paren | Agda.Syntax.Concrete |
| paren | Agda.Syntax.Concrete.Operators |
| ParenP | Agda.Syntax.Concrete |
| parens | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| Parent | Agda.Utils.Trace |
| ParentCall | Agda.Utils.Trace |
| ParenV | Agda.Syntax.Concrete.Operators.Parser |
| pargs | Agda.Auto.Print |
| parse | |
| 1 (Function) | Agda.Utils.ReadP |
| 2 (Function) | Agda.Syntax.Parser.Monad |
| 3 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| 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 | 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.Syntax.Parser.Monad |
| 2 (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 |
| PatSource | Agda.Syntax.Info |
| patsToTerms | Agda.TypeChecking.With |
| Pattern | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Internal |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| Pattern' | Agda.Syntax.Abstract |
| PatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PatternShadowsConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| patternViolation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PatVar | Agda.Auto.Syntax |
| PB | Agda.Auto.NarrowingSearch |
| PBlocked | Agda.Auto.NarrowingSearch |
| pcargs | Agda.Auto.Typecheck |
| pcexp | Agda.Auto.Typecheck |
| pconName | Agda.Compiler.MAlonzo.Primitives |
| PDoubleBlocked | Agda.Auto.NarrowingSearch |
| PEConApp | Agda.Auto.Typecheck |
| PEConPar | Agda.Auto.Typecheck |
| pelr | Agda.Auto.Print |
| PENo | Agda.Auto.Typecheck |
| Perm | Agda.Utils.Permutation |
| Permutation | Agda.Utils.Permutation |
| permute | Agda.Utils.Permutation |
| PersistentOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| PEval | Agda.Auto.Typecheck |
| pexp | Agda.Auto.Print |
| pfail | Agda.Utils.ReadP |
| pHidden | Agda.Syntax.Concrete.Pretty |
| phnargs | Agda.Auto.Typecheck |
| phnexp | Agda.Auto.Typecheck |
| 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 |
| piBrackets | Agda.Syntax.Fixity |
| pickid | Agda.Auto.Typecheck |
| pid | Agda.Auto.Print |
| piFreq | Agda.TypeChecking.Test.Generators |
| PiHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| plugHole | Agda.Syntax.Internal.Pattern |
| Plus | Agda.TypeChecking.Level |
| PlusView | Agda.TypeChecking.Level |
| PM | Agda.Compiler.Alonzo.PatternMonad |
| Pn | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| polarities | Agda.TypeChecking.Polarity |
| Polarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| polarity | Agda.TypeChecking.Polarity |
| 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 |
| 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 | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Precedence | Agda.Syntax.Fixity |
| Pred | Agda.TypeChecking.Primitive |
| Prefix | Agda.Utils.List |
| PrefixDef | Agda.Syntax.Common |
| prefixP | Agda.Syntax.Concrete.Operators.Parser |
| preMeta | Agda.Interaction.GhciTop |
| preop | Agda.Syntax.Concrete.Operators.Parser |
| preserveDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| Pretty | Agda.Utils.Pretty |
| pretty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyA | |
| 1 (Function) | Agda.Syntax.Abstract.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| PrettyContext | |
| 1 (Type/Class) | Agda.TypeChecking.Pretty |
| 2 (Data Constructor) | Agda.TypeChecking.Pretty |
| prettyContext | Agda.Interaction.GhciTop |
| prettyError | Agda.TypeChecking.Errors, Agda.Interaction.GhciTop |
| prettyGraph | Agda.TypeChecking.Positivity |
| prettyList | Agda.TypeChecking.Pretty |
| prettyPrec | Agda.Utils.Pretty |
| prettyPrint | Agda.Compiler.MAlonzo.Pretty |
| prettySplitError | Agda.Interaction.MakeCase |
| 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 |
| Prim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primBody | Agda.Compiler.MAlonzo.Primitives |
| primBool | Agda.TypeChecking.Monad.Builtin |
| primChar | Agda.TypeChecking.Monad.Builtin |
| primClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primCons | Agda.TypeChecking.Monad.Builtin |
| Prime | Agda.Utils.Suffix |
| primEquality | Agda.TypeChecking.Monad.Builtin |
| primFalse | 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 |
| primFunArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primFunImplementation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primFunName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PrimImpl | Agda.TypeChecking.Primitive |
| primInteger | Agda.TypeChecking.Monad.Builtin |
| primIO | 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 |
| 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 |
| 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 |
| primRefl | 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 |
| PrimTerm | Agda.TypeChecking.Primitive |
| primTerm | Agda.TypeChecking.Primitive |
| primTrue | Agda.TypeChecking.Monad.Builtin |
| primTrustMe | Agda.TypeChecking.Primitive |
| PrimType | Agda.TypeChecking.Primitive |
| primType | Agda.TypeChecking.Primitive |
| primZero | Agda.TypeChecking.Monad.Builtin |
| print | Agda.Utils.IO.Locale |
| printAlDecl | Agda.Compiler.Alonzo.Haskell |
| printAlModule | Agda.Compiler.Alonzo.Haskell |
| printCExp | Agda.Auto.Typecheck |
| printClause | Agda.Auto.Print |
| printConst | Agda.Auto.Print |
| printConstants | Agda.Compiler.Agate.Main |
| PrintConstr | Agda.Auto.NarrowingSearch |
| printCTree | Agda.Auto.NarrowingSearch |
| printCtx | Agda.Auto.Typecheck |
| printExp | Agda.Auto.Print |
| printHNExp | Agda.Auto.Typecheck |
| printHsDecls | Agda.Compiler.Alonzo.Haskell |
| printHsMain | Agda.Compiler.Alonzo.Haskell |
| printHsModule | Agda.Compiler.Alonzo.Haskell |
| printId | Agda.Auto.Print |
| printPat | Agda.Auto.Print |
| printPats | Agda.Auto.Print |
| printref | Agda.Auto.NarrowingSearch |
| printShowConstants | Agda.Compiler.Agate.Main |
| printUsage | Agda.Main |
| printVersion | Agda.Main |
| Prio | Agda.Auto.NarrowingSearch |
| prioCompare | Agda.Auto.SearchControl |
| prioCompareArgList | Agda.Auto.SearchControl |
| prioCompChoice | Agda.Auto.SearchControl |
| prioCompIota | Agda.Auto.SearchControl |
| prioInferredTypeUnknown | Agda.Auto.SearchControl |
| PrioMeta | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| prioNo | Agda.Auto.SearchControl |
| prioPreCompare | 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 |
| Problem | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| Problem' | Agda.TypeChecking.Rules.LHS.Problem |
| problemInPat | Agda.TypeChecking.Rules.LHS.Problem |
| problemOutPat | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemPart | Agda.TypeChecking.Rules.LHS.Problem |
| problemTel | Agda.TypeChecking.Rules.LHS.Problem |
| processArgPat | Agda.Compiler.Alonzo.Main |
| processArgPats | Agda.Compiler.Alonzo.Main |
| processBody | Agda.Compiler.Alonzo.Main |
| processClause | Agda.Compiler.Alonzo.Main |
| processCon | Agda.Compiler.Alonzo.Main |
| processDef | Agda.Compiler.Alonzo.Main |
| processDefWithDebug | Agda.Compiler.Alonzo.Main |
| processLit | Agda.Compiler.Alonzo.Main |
| processPat | Agda.Compiler.Alonzo.Main |
| processTerm | Agda.Compiler.Alonzo.Main |
| processVap | Agda.Compiler.Alonzo.Main |
| ProjectRoot | Agda.Interaction.Imports |
| 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_extractNthElement | Agda.Utils.List |
| prop_flattenTelInv | Agda.TypeChecking.Tests |
| prop_flattenTelScope | Agda.TypeChecking.Tests |
| 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_wellScopedVars | Agda.TypeChecking.Test.Generators |
| psep | Agda.Compiler.Agate.Common |
| PSt | Agda.Compiler.Alonzo.PatternMonad |
| PState | |
| 1 (Data Constructor) | Agda.Syntax.Parser.Monad |
| 2 (Type/Class) | Agda.Compiler.Alonzo.PatternMonad |
| PStr | Agda.Utils.Pretty |
| ptcCompare | Agda.Auto.Typecheck |
| ptcCompareArgList | Agda.Auto.Typecheck |
| ptcNoIotaStep | Agda.Auto.Typecheck |
| ptcTypeCheck | Agda.Auto.Typecheck |
| ptcTypecheckArgList | Agda.Auto.Typecheck |
| ptcTypeUnknown | Agda.Auto.Typecheck |
| 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 |
| 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 |
| putPcnt | Agda.Compiler.Alonzo.PatternMonad |
| putPlst | Agda.Compiler.Alonzo.PatternMonad |
| putStr | Agda.Utils.IO.Locale |
| putStrLn | Agda.Utils.IO.Locale |
| pwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |