idris-1.2.0: Functional Programming Language with Dependent Types

Index - P

PIdris.Core.TT
packageNameIdris.Parser.Helpers
pairConIdris.AbsSyntaxTree, Idris.AbsSyntax
pairTyIdris.AbsSyntaxTree, Idris.AbsSyntax
PAlternativeIdris.AbsSyntaxTree, Idris.AbsSyntax
PAltTypeIdris.AbsSyntaxTree, Idris.AbsSyntax
PAppIdris.AbsSyntaxTree, Idris.AbsSyntax
PAppBindIdris.AbsSyntaxTree, Idris.AbsSyntax
PAppImplIdris.AbsSyntaxTree, Idris.AbsSyntax
ParaIdris.Docstrings
paramNamesIdris.Elab.Utils
paramsIdris.AbsSyntaxTree, Idris.AbsSyntax
param_posIdris.Core.TT
ParentNIdris.Core.TT
PArgIdris.AbsSyntaxTree, Idris.AbsSyntax
PArg'Idris.AbsSyntaxTree, Idris.AbsSyntax
pargoptsIdris.AbsSyntaxTree, Idris.AbsSyntax
parseCmdIdris.REPL.Parser
parseConstIdris.Parser
parseDescIdris.Package.Parser
parseDocstringIdris.Docstrings
parseElabShellStepIdris.Parser
ParseErrorIdris.Parser.Stack, Idris.Parser.Helpers, Idris.Parser
parseErrorDocIdris.Parser.Helpers, Idris.Parser
parseExprIdris.Parser
parseImportsIdris.Parser
parseMessageIdris.IdeMode
ParserIdris.Parser.Stack, Idris.Parser.Helpers
parserCatsIdris.Options
parserWarningIdris.Parser.Helpers
parserWarningsIdris.AbsSyntaxTree, Idris.AbsSyntax
parseTacticIdris.Parser
ParsingIdris.Parser.Stack, Idris.Parser.Helpers
Partial 
1 (Data Constructor)Idris.Core.Evaluate
2 (Type/Class)IRTS.JavaScript.Name
3 (Data Constructor)IRTS.JavaScript.Name
partialApplicationsIRTS.JavaScript.Codegen
PartialFnIdris.AbsSyntaxTree, Idris.AbsSyntax
partial_evalIdris.PartialEval
PAsIdris.AbsSyntaxTree, Idris.AbsSyntax
PatBindIdris.Core.ProofState, Idris.Core.Elaborate
patbindIdris.Core.Elaborate
PattelabIdris.REPL.Commands
PatternSyntaxIdris.AbsSyntaxTree, Idris.AbsSyntax
PatVarIdris.Core.ProofState, Idris.Core.Elaborate
patvarIdris.Core.Elaborate
patvar'Idris.Core.Elaborate
pbindsIdris.Elab.Utils
pbtyIdris.Elab.Utils
PCAFIdris.AbsSyntaxTree, Idris.AbsSyntax
PCaseIdris.AbsSyntaxTree, Idris.AbsSyntax
PClause 
1 (Type/Class)Idris.AbsSyntaxTree, Idris.AbsSyntax
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
pClauseIdris.Package.Parser
PClause'Idris.AbsSyntaxTree, Idris.AbsSyntax
PClauseRIdris.AbsSyntaxTree, Idris.AbsSyntax
PClausesIdris.AbsSyntaxTree, Idris.AbsSyntax
PCoercedIdris.AbsSyntaxTree, Idris.AbsSyntax
pconstIdris.AbsSyntaxTree, Idris.AbsSyntax
PConstantIdris.AbsSyntaxTree, Idris.AbsSyntax
PConstraintIdris.AbsSyntaxTree, Idris.AbsSyntax
PConstSugarIdris.AbsSyntaxTree, Idris.AbsSyntax
pcountIdris.AbsSyntaxTree, Idris.AbsSyntax
PData 
1 (Type/Class)Idris.AbsSyntaxTree, Idris.AbsSyntax
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
PData'Idris.AbsSyntaxTree, Idris.AbsSyntax
PDatadeclIdris.AbsSyntaxTree, Idris.AbsSyntax
PDeclIdris.AbsSyntaxTree, Idris.AbsSyntax
PDecl'Idris.AbsSyntaxTree, Idris.AbsSyntax
PDirectiveIdris.AbsSyntaxTree, Idris.AbsSyntax
PDisambIdris.AbsSyntaxTree, Idris.AbsSyntax
PDoIdris.AbsSyntaxTree, Idris.AbsSyntax
PDo'Idris.AbsSyntaxTree, Idris.AbsSyntax
PDoBlockIdris.AbsSyntaxTree, Idris.AbsSyntax
PDPairIdris.AbsSyntaxTree, Idris.AbsSyntax
PDSLIdris.AbsSyntaxTree, Idris.AbsSyntax
PEArgTypeIdris.PartialEval
PEGeneratedIdris.AbsSyntaxTree, Idris.AbsSyntax
PElabErrorIdris.AbsSyntaxTree, Idris.AbsSyntax
pEraseTypeIdris.Core.TT
performUsageAnalysisIdris.Erasure
PETransformIdris.Options
PExpIdris.AbsSyntaxTree, Idris.AbsSyntax
pexpIdris.AbsSyntaxTree, Idris.AbsSyntax
pe_appIdris.PartialEval
pe_clausesIdris.PartialEval
pe_defIdris.PartialEval
pe_depthIdris.AbsSyntaxTree, Idris.AbsSyntax
pe_simpleIdris.PartialEval
PFixIdris.AbsSyntaxTree, Idris.AbsSyntax
PGoalIdris.AbsSyntaxTree, Idris.AbsSyntax
PhaseIdris.Core.CaseTree
PHiddenIdris.AbsSyntaxTree, Idris.AbsSyntax
PiIdris.Core.TT
piIdris.Parser.Expr
piBindIdris.AbsSyntaxTree, Idris.AbsSyntax
piBindpIdris.AbsSyntaxTree, Idris.AbsSyntax
PIdiomIdris.AbsSyntaxTree, Idris.AbsSyntax
PIfThenElseIdris.AbsSyntaxTree, Idris.AbsSyntax
PImpIdris.AbsSyntaxTree, Idris.AbsSyntax
pimpIdris.AbsSyntaxTree, Idris.AbsSyntax
PImplementationIdris.AbsSyntaxTree, Idris.AbsSyntax
PImpossibleIdris.AbsSyntaxTree, Idris.AbsSyntax
PInferRefIdris.AbsSyntaxTree, Idris.AbsSyntax
pinsourceIdris.AbsSyntaxTree, Idris.AbsSyntax
PInterfaceIdris.AbsSyntaxTree, Idris.AbsSyntax
piOptsIdris.Parser.Expr
PkgIdris.Options
PkgArgsIdris.Help
pkgauthorIdris.Package.Common
pkgbriefIdris.Package.Common
pkgbugtrackerIdris.Package.Common
PkgBuildIdris.Options
PkgCheckIdris.Options
PkgCleanIdris.Options
pkgdepsIdris.Package.Common
PkgDesc 
1 (Type/Class)Idris.Package.Common
2 (Data Constructor)Idris.Package.Common
PkgDocBuildIdris.Options
PkgDocInstallIdris.Options
pkghomepageIdris.Package.Common
PkgIndexIdris.Options
pkgIndexIdris.Imports
PkgInstallIdris.Options
pkglicenseIdris.Package.Common
pkgmaintainerIdris.Package.Common
PkgNameIdris.Imports
pkgNameIdris.Imports
pkgnameIdris.Package.Common
pkgreadmeIdris.Package.Common
PkgREPLIdris.Options
pkgsourcelocIdris.Package.Common
PkgTestIdris.Options
pkgversionIdris.Package.Common
PlaceholderIdris.AbsSyntaxTree, Idris.AbsSyntax
PLamIdris.AbsSyntaxTree, Idris.AbsSyntax
PLaterdeclIdris.AbsSyntaxTree, Idris.AbsSyntax
PLetIdris.AbsSyntaxTree, Idris.AbsSyntax
PlicityIdris.AbsSyntaxTree, Idris.AbsSyntax
plogIdris.Core.ProofState, Idris.Core.Elaborate
pmapIdris.Core.TT
PMatchAppIdris.AbsSyntaxTree, Idris.AbsSyntax
PMetavarIdris.AbsSyntaxTree, Idris.AbsSyntax
PMutualIdris.AbsSyntaxTree, Idris.AbsSyntax
pnameIdris.AbsSyntaxTree, Idris.AbsSyntax
PNamespaceIdris.AbsSyntaxTree, Idris.AbsSyntax
PNoImplicitsIdris.AbsSyntaxTree, Idris.AbsSyntax
POpenInterfacesIdris.AbsSyntaxTree, Idris.AbsSyntax
popIndentIdris.Parser.Helpers
pop_estackIdris.AbsSyntax
PortIdris.Options
PostulateColourIdris.Colours
postulateColourIdris.Colours
PostulateOutputIdris.Core.TT
PPairIdris.AbsSyntaxTree, Idris.AbsSyntax
pparamIdris.AbsSyntaxTree, Idris.AbsSyntax
PParamsIdris.AbsSyntaxTree, Idris.AbsSyntax
PParserIdris.Package.Parser
PPatvarIdris.AbsSyntaxTree, Idris.AbsSyntax
PPiIdris.AbsSyntaxTree, Idris.AbsSyntax
pPkgIdris.Package.Parser
pPkgNameIdris.Package.Parser
PPOption 
1 (Type/Class)Idris.AbsSyntaxTree, Idris.AbsSyntax
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
ppOptionIdris.AbsSyntaxTree, Idris.AbsSyntax
ppOptionIstIdris.AbsSyntaxTree, Idris.AbsSyntax
ppopt_depthIdris.AbsSyntaxTree, Idris.AbsSyntax
ppopt_desugarnatsIdris.AbsSyntaxTree, Idris.AbsSyntax
ppopt_displayrigIdris.AbsSyntaxTree, Idris.AbsSyntax
ppopt_implIdris.AbsSyntaxTree, Idris.AbsSyntax
ppopt_pinamesIdris.AbsSyntaxTree, Idris.AbsSyntax
PPostulateIdris.AbsSyntaxTree, Idris.AbsSyntax
PPrintIdris.REPL.Commands
pprintConstDocsIdris.Docs
pprintDelabIdris.Delaborate
pprintDelabTyIdris.Delaborate
pprintDocsIdris.Docs
pprintErrIdris.Delaborate
pprintNoDelabIdris.Delaborate
pprintPTermIdris.AbsSyntaxTree, Idris.AbsSyntax
pprintRawIdris.Core.TT
pprintTTIdris.Core.TT
pprintTTClauseIdris.Core.TT
pprintTypeDocIdris.Docs
PProofIdris.AbsSyntaxTree, Idris.AbsSyntax
PProviderIdris.AbsSyntaxTree, Idris.AbsSyntax
PQuasiquoteIdris.AbsSyntaxTree, Idris.AbsSyntax
PQuoteIdris.AbsSyntaxTree, Idris.AbsSyntax
PQuoteNameIdris.AbsSyntaxTree, Idris.AbsSyntax
PReasonIdris.Core.Evaluate
precIdris.AbsSyntaxTree, Idris.AbsSyntax
PRecordIdris.AbsSyntaxTree, Idris.AbsSyntax
PRefIdris.AbsSyntaxTree, Idris.AbsSyntax
PrefixNIdris.AbsSyntaxTree, Idris.AbsSyntax
premisesIdris.Core.ProofTerm, Idris.Core.ProofState, Idris.Core.Elaborate
prepare_applyIdris.Core.Elaborate
PrepFillIdris.Core.ProofState, Idris.Core.Elaborate
prep_fillIdris.Core.Elaborate
PResolveTCIdris.AbsSyntaxTree, Idris.AbsSyntax
prettyDocumentedIstIdris.Output
prettyEnvIdris.Core.TT
prettyErrorIdris.Parser.Stack, Idris.Parser.Helpers
prettyImpIdris.AbsSyntaxTree, Idris.AbsSyntax
prettyIstIdris.AbsSyntaxTree, Idris.AbsSyntax
prettyNameIdris.AbsSyntaxTree, Idris.AbsSyntax
previousIdris.Core.ProofState, Idris.Core.Elaborate
PRewriteIdris.AbsSyntaxTree, Idris.AbsSyntax
Prim 
1 (Type/Class)Idris.Primitives
2 (Data Constructor)Idris.Primitives
primDBIRTS.JavaScript.PrimOp
PrimDecIRTS.JavaScript.PrimOp
primDefsIdris.AbsSyntaxTree, Idris.AbsSyntax
PrimFIRTS.JavaScript.PrimOp
primfcIdris.AbsSyntaxTree, Idris.AbsSyntax
PrimFnIRTS.Lang, IRTS.Defunctionalise
primitivesIdris.Primitives
primNamesIdris.AbsSyntaxTree, Idris.AbsSyntax
PrintDef 
1 (Data Constructor)Idris.IdeMode
2 (Data Constructor)Idris.REPL.Commands
printUndefinedNamesIdris.Output
priorityIdris.AbsSyntaxTree, Idris.AbsSyntax
PrivateIdris.Core.Evaluate
problemsIdris.Core.ProofState, Idris.Core.Elaborate
processIdris.REPL
processTacticIdris.Core.ProofState, Idris.Core.Elaborate
processTactic'Idris.Core.Elaborate
processTacticDeclsIdris.Elab.Term
ProductiveIdris.Core.Evaluate
ProgramLineCommentIdris.Core.TT
ProjIdris.Core.TT
ProjCaseIdris.Core.CaseTree
PROJECTIRTS.Bytecode
PROJECTINTOIRTS.Bytecode
PromptColourIdris.Colours
promptColourIdris.Colours
proofIdris.Core.Elaborate
proofExprIdris.Parser.Expr
proofFailIdris.Core.Elaborate
ProofsIdris.REPL.Commands
proofsIdris.REPL
ProofSearch 
1 (Data Constructor)Idris.IdeMode
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
proofSearchIdris.ProofSearch
proofSearch'Idris.Elab.Term
ProofSearchFailIdris.Core.TT
ProofState 
1 (Data Constructor)Idris.Core.ProofState, Idris.Core.Elaborate
2 (Type/Class)Idris.Core.ProofState, Idris.Core.Elaborate
3 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
proofstateIdris.Core.Elaborate
ProofTerm 
1 (Type/Class)Idris.Core.ProofTerm
2 (Data Constructor)Idris.AbsSyntaxTree, Idris.AbsSyntax
proof_listIdris.AbsSyntaxTree, Idris.AbsSyntax
propagateParamsIdris.Elab.Utils
ProveIdris.REPL.Commands
ProvenanceIdris.Core.TT
proverIdris.Prover
proverCompletionIdris.Completion
ProvideIdris.Providers
ProvidedIdris.Providers
ProviderErrorIdris.Core.TT
providerTyIdris.Providers
ProvideWhatIdris.AbsSyntaxTree, Idris.AbsSyntax
ProvideWhat'Idris.AbsSyntaxTree, Idris.AbsSyntax
ProvPostulateIdris.AbsSyntaxTree, Idris.AbsSyntax
ProvTermIdris.AbsSyntaxTree, Idris.AbsSyntax
pruneAltIdris.Elab.Term
pruneByTypeIdris.Elab.Utils
PRunElabIdris.AbsSyntaxTree, Idris.AbsSyntax
PRunElabDeclIdris.AbsSyntaxTree, Idris.AbsSyntax
prunStateTIdris.Core.Elaborate
PSIdris.Core.ProofState, Idris.Core.Elaborate
pscopedIdris.AbsSyntaxTree, Idris.AbsSyntax
pscriptIdris.AbsSyntaxTree, Idris.AbsSyntax
pshowIdris.Output
psnamesIdris.Core.ProofState, Idris.Core.Elaborate
psolveIdris.Elab.Utils
pstaticIdris.AbsSyntaxTree, Idris.AbsSyntax
psubstIdris.Core.TT
PSyntaxIdris.AbsSyntaxTree, Idris.AbsSyntax
ptacimpIdris.AbsSyntaxTree, Idris.AbsSyntax
PTacImplicitIdris.AbsSyntaxTree, Idris.AbsSyntax
PTacticIdris.AbsSyntaxTree, Idris.AbsSyntax
PTactic'Idris.AbsSyntaxTree, Idris.AbsSyntax
PTacticsIdris.AbsSyntaxTree, Idris.AbsSyntax
PTAnyIRTS.JavaScript.PrimOp
PTBoolIRTS.JavaScript.PrimOp
PTermIdris.AbsSyntaxTree, Idris.AbsSyntax
ptermIdris.Core.ProofState, Idris.Core.Elaborate
pToVIdris.Core.TT
pToVsIdris.Core.TT
PTransformIdris.AbsSyntaxTree, Idris.AbsSyntax
PTrueIdris.AbsSyntaxTree, Idris.AbsSyntax
PTyIdris.AbsSyntaxTree, Idris.AbsSyntax
PTypeIdris.AbsSyntaxTree, Idris.AbsSyntax
ptypeIdris.Core.ProofState, Idris.Core.Elaborate
PTypedIdris.AbsSyntaxTree, Idris.AbsSyntax
PublicIdris.Core.Evaluate
PUnifyLogIdris.AbsSyntaxTree, Idris.AbsSyntax
PunInfoIdris.AbsSyntaxTree, Idris.AbsSyntax
PUniverseIdris.AbsSyntaxTree, Idris.AbsSyntax
PUnquoteIdris.AbsSyntaxTree, Idris.AbsSyntax
pureArgParserIdris.CmdOptions
pureTermIdris.Core.TT
pushIndentIdris.Parser.Helpers
push_estackIdris.AbsSyntax
putIStateIdris.AbsSyntax
PVarIdris.Core.TT
pvarsIdris.Elab.Utils
PVTyIdris.Core.TT
PWithIdris.AbsSyntaxTree, Idris.AbsSyntax
PWithAppIdris.AbsSyntaxTree, Idris.AbsSyntax
PWithRIdris.AbsSyntaxTree, Idris.AbsSyntax
p_arityIdris.Primitives
p_defIdris.Primitives
p_lexpIdris.Primitives
p_nameIdris.Primitives
p_totalIdris.Primitives
p_typeIdris.Primitives