Index - P
| P | Core.TT |
| pAccess | Idris.IBC |
| PageMode | Util.Pretty |
| pairCon | Idris.AbsSyntax |
| pairDecl | Idris.AbsSyntax |
| pairTy | Idris.AbsSyntax |
| PAlternative | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PAppBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| params | |
| 1 (Function) | Idris.ElabTerm |
| 2 (Function) | Idris.Parser |
| param_pos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parens | Util.Pretty |
| ParentN | Core.TT |
| PArg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PArg' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pargdoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| parseArgs | Idris.REPL |
| parseCmd | Idris.REPLParser |
| parseCodegen | Idris.REPL |
| parseDesc | Pkg.PParser |
| parseExpr | Idris.Parser |
| parseImports | Idris.Parser |
| parseMessage | Idris.IdeSlave |
| parseProg | Idris.Parser |
| parseTactic | Idris.Parser |
| Partial | Core.Evaluate |
| PartialFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| partial_eval | Idris.PartialEval |
| PatBind | Core.ProofState, Core.Elaborate |
| patbind | Core.Elaborate |
| Pattelab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pattern | Idris.Parser |
| PatternSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PatVar | Core.ProofState, Core.Elaborate |
| patvar | Core.Elaborate |
| pbinds | Idris.ElabDecls |
| pbty | Idris.ElabDecls |
| PCAF | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pCG | Idris.IBC |
| pCGFlags | Idris.IBC |
| PClass | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pClasses | Idris.IBC |
| PClause | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pClause | Pkg.PParser |
| PClause' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PClauseR | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PClauses | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PCoerced | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pCoercions | Idris.IBC |
| pconst | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PConstant | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PConstraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PData | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PData' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDatadecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pDatatypes | Idris.IBC |
| PDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDecl' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pDefs | Idris.IBC |
| PDirective | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDo' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDoBlock | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pDocs | Idris.IBC |
| pdocstr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDPair | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pDSLs | Idris.IBC |
| pDyLibs | Idris.IBC |
| PEArgType | Idris.PartialEval |
| PElabError | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PEq | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PExp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pexp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PFalse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PFix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pFixes | Idris.IBC |
| pFlags | Idris.IBC |
| PGoal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Phase | Core.CaseTree |
| pHdrs | Idris.IBC |
| PHidden | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Pi | Core.TT |
| pi | Idris.ParseExpr, Idris.Parser |
| piBind | Idris.AbsSyntax |
| piBindp | Idris.AbsSyntax |
| PIdiom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pImports | Idris.IBC |
| PImpossible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pImps | Idris.IBC |
| PInferRef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pInstances | Idris.IBC |
| pKeywords | Idris.IBC |
| Pkg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgBuild | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgClean | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PkgDesc | |
| 1 (Type/Class) | Pkg.PParser |
| 2 (Data Constructor) | Pkg.PParser |
| PkgInstall | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pkgname | Pkg.PParser |
| Placeholder | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PLam | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pLangExt | Idris.Parser |
| PLaterdecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| plazy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PLet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pLibs | Idris.IBC |
| Plicity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pLineApps | Idris.IBC |
| plog | Core.ProofState, Core.Elaborate |
| ploop | Idris.Prover |
| pmap | Core.TT |
| PMatchApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PMetavar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PMutual | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pname | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PNamespace | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PNoImplicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pObjs | Idris.IBC |
| pomString | IRTS.Java.Pom |
| popIndent | Idris.ParseHelpers, Idris.Parser |
| pOptimise | Idris.IBC |
| postulate | Idris.Parser |
| PPair | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pparam | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PParams | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PParser | Pkg.PParser |
| PPatvar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PPi | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pPkg | Pkg.PParser |
| PPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PProvider | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PQuote | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PReason | Core.Evaluate |
| prec | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PRecord | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PRef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prefix | Idris.ParseOps, Idris.Parser |
| prefixCallNamespaces | IRTS.Java.Mangling |
| PrefixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PRefl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| premises | Core.ProofState, Core.Elaborate |
| prepare_apply | Core.Elaborate |
| PrepFill | Core.ProofState, Core.Elaborate |
| prep_fill | Core.Elaborate |
| PResolveTC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Pretty | Util.Pretty |
| pretty | Util.Pretty |
| prettyEnv | Core.TT |
| prettyImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PReturn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| previous | Core.ProofState, Core.Elaborate |
| PRewrite | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Prim | |
| 1 (Type/Class) | Idris.Primitives |
| 2 (Data Constructor) | Idris.Primitives |
| primDefs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PrimFn | IRTS.Lang, IRTS.Defunctionalise |
| primFnType | IRTS.Java.JTypes |
| primitives | Idris.Primitives |
| primNames | Idris.AbsSyntax |
| Core.Elaborate | |
| priority | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| problems | Core.ProofState, Core.Elaborate |
| process | |
| 1 (Function) | Idris.IBC |
| 2 (Function) | Idris.REPL |
| processInput | Idris.REPL |
| processNetCmd | Idris.REPL |
| processTactic | Core.ProofState, Core.Elaborate |
| processTactic' | Core.Elaborate |
| Productive | Core.Evaluate |
| prog | Idris.Parser |
| ProgramLineComment | Core.TT |
| Proj | Core.TT |
| ProjCase | Core.CaseTree |
| PROJECT | IRTS.Bytecode |
| PROJECTINTO | IRTS.Bytecode |
| PromptColour | Idris.Colours |
| promptColour | Idris.Colours |
| proof | Core.Elaborate |
| proofExpr | Idris.ParseExpr, Idris.Parser |
| proofFail | Core.Elaborate |
| Proofs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proofs | Idris.REPL |
| ProofSearch | |
| 1 (Data Constructor) | Idris.IdeSlave |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proofSearch | Idris.ProofSearch |
| proofSearch' | Idris.ElabTerm |
| ProofSearchFail | Core.TT |
| ProofState | |
| 1 (Data Constructor) | Core.ProofState, Core.Elaborate |
| 2 (Type/Class) | Core.ProofState, Core.Elaborate |
| 3 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proofstate | Core.Elaborate |
| ProofTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| proof_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Prove | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| prove | Idris.Prover |
| prover | Idris.Prover |
| proverCompletion | Idris.Completion |
| proverSettings | Idris.Prover |
| provider | Idris.Parser |
| ProviderError | Core.TT |
| providerTy | Idris.Providers |
| pruneAlt | Idris.ElabTerm |
| pruneByType | Idris.ElabTerm |
| prunStateT | Core.Elaborate |
| PS | Core.ProofState, Core.Elaborate |
| pscript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pshow | Idris.Delaborate |
| psolve | Idris.ElabDecls |
| pstatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pStatics | Idris.IBC |
| PStr | Util.Pretty |
| PSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pSyntax | Idris.IBC |
| ptacimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTacImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTactic' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTactics | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pterm | Core.ProofState, Core.Elaborate |
| ptext | Util.Pretty |
| pTotal | Idris.IBC |
| pToV | Core.TT |
| pToV' | Core.TT |
| pToVs | Core.TT |
| pTrans | Idris.IBC |
| PTransform | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PtrType | Core.TT |
| PTrue | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ptype | Core.ProofState, Core.Elaborate |
| PTyped | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Public | Core.Evaluate |
| punctuate | Util.Pretty |
| PUnifyLog | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| pureTerm | Core.TT |
| pushIndent | Idris.ParseHelpers, Idris.Parser |
| putIState | Idris.AbsSyntax |
| PVar | Core.TT |
| pvars | Idris.ElabDecls |
| PVTy | Core.TT |
| PWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| PWithR | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| p_arity | Idris.Primitives |
| p_def | Idris.Primitives |
| p_lexp | Idris.Primitives |
| p_name | Idris.Primitives |
| p_total | Idris.Primitives |
| p_type | Idris.Primitives |