Agda-2.2.10: A dependently typed functional programming language and proof assistantContentsIndex
ABCDEFGHIJKLMNOPQRSTUVWXYZ:!$&+./<=>|-
Index (P)
PageMode
Pair
1 (Type/Class)
2 (Data Constructor)
pairwiseFilter
Paren
paren
ParenP
parens
1 (Function)
2 (Function)
ParenV
parse
1 (Function)
2 (Function)
3 (Function)
parseAndDoAtToplevel
parseApplication
ParseError
1 (Type/Class)
2 (Data Constructor)
parseError
parseErrorAt
parseExpr
1 (Function)
2 (Function)
parseExprIn
ParseFailed
parseFile
parseFile'
ParseFlags
1 (Type/Class)
2 (Data Constructor)
parseFlags
parseInp
parseKeepComments
parseLastPos
parseLayout
parseLexState
parseLHS
parseLiterate
ParseOk
parsePluginOptions
parsePos
parsePosString
1 (Function)
2 (Function)
parsePragmaOptions
parsePrevChar
parsePrevToken
Parser
1 (Type/Class)
2 (Type/Class)
ParseResult
parseStandardOptions
ParseState
partP
Pat
PatConApp
PatExp
PatInfo
PatName
PatRange
PatSource
patsToTerms
Pattern
1 (Type/Class)
2 (Type/Class)
3 (Type/Class)
Pattern'
PatternErr
PatternShadowsConstructor
patternViolation
PatVar
PB
PBlocked
pconName
PDoubleBlocked
PEConApp
PENo
performKill
Perm
Permutation
permute
PEval
pfail
pHidden
Pi
1 (Data Constructor)
2 (Data Constructor)
3 (Data Constructor)
4 (Data Constructor)
piAbstractTerm
piApply
piApplyM
piBrackets
pickid
piFreq
PiHead
plugHole
Plus
PlusView
Pn
polarities
Polarity
polarity
popContext
popLexState
popMapS
posCol
Position
positionInvariant
Positive
1 (Data Constructor)
2 (Type/Class)
3 (Data Constructor)
positive
positivityCheckEnabled
posLine
posPos
postfixP
postop
posToRange
PostponedTypeCheckingProblem
postponeTypeCheckingProblem
postponeTypeCheckingProblem_
Postulate
1 (Data Constructor)
2 (Data Constructor)
3 (Data Constructor)
Pragma
1 (Type/Class)
2 (Data Constructor)
3 (Type/Class)
4 (Data Constructor)
PragmaOptions
1 (Type/Class)
2 (Data Constructor)
pragmaOptions
Precedence
Pred
Prefix
PrefixDef
prefixP
pRelevance
preMeta
preop
preserveDecodedModules
Pretty
pretty
1 (Function)
2 (Function)
prettyA
1 (Function)
2 (Function)
prettyATop
prettyBehaviour
PrettyContext
1 (Type/Class)
2 (Data Constructor)
prettyContext
prettyEpicFun
prettyError
prettyGraph
prettyList
prettyPrec
prettyPrint
PrettyTCM
prettyTCM
prettyTypeOfMeta
preUscore
PreviousInput
Prim
primAbstr
primAgdaTerm
primAgdaTermCon
primAgdaTermDef
primAgdaTermLam
primAgdaTermPi
primAgdaTermSort
primAgdaTermUnsupported
primAgdaTermVar
primArg
primArgArg
primBody
primBool
primChar
primClauses
primCompiled
primCons
Prime
primEquality
primExpr
primFalse
primFlat
primFloat
PrimFun
1 (Type/Class)
2 (Data Constructor)
primFun
primFunArity
primFunImplementation
primFunName
PrimImpl
primInf
primInteger
primIO
Primitive
1 (Data Constructor)
2 (Data Constructor)
3 (Data Constructor)
4 (Data Constructor)
PrimitiveFunction
primitiveFunctions
PrimitiveImpl
PrimitiveType
primitivise
primLevel
primLevelMax
primLevelSuc
primLevelZero
primList
primLists
primName
primNat
primNatCaseZD
primNatCaseZS
primNatDivSucAux
primNatEquality
primNatLess
primNatMinus
primNatModSucAux
primNatPlus
primNatTimes
primNil
primQName
primRefl
primSharp
primSize
primSizeInf
primSizeSuc
primString
primSuc
PrimTerm
primTerm
PrimTF
PrimTransform
primTrue
primTrustMe
PrimType
primType
primZero
print
printUsage
printVersion
Prio
prioAbsurdLambda
prioCompareArgList
prioCompBeta
prioCompBetaStructured
prioCompChoice
prioCompCopy
prioCompIota
prioCompUnif
prioInferredTypeUnknown
PrioMeta
1 (Type/Class)
2 (Data Constructor)
prioNo
prioNoIota
prioProjIndex
prioTypecheck
prioTypecheckArgList
prioTypeUnknown
Private
PrivateAccess
PrivateNS
Problem
1 (Type/Class)
2 (Data Constructor)
Problem'
problemInPat
problemOutPat
ProblemPart
problemTel
ProjectRoot
projectRoot
promote
proofIrrelevance
Prop
1 (Type/Class)
2 (Type/Class)
3 (Data Constructor)
4 (Data Constructor)
5 (Data Constructor)
prop
propagatePrio
Property
property
propFreq
PropMustBeSingleton
prop_disjoint
prop_distinct_fastDistinct
prop_extractNthElement
prop_flattenTelInv
prop_flattenTelScope
prop_genericElemIndex
prop_groupBy'
prop_path
prop_reorderTelStable
prop_smaller
prop_splitTelescopePermScope
prop_splitTelescopeScope
prop_stable
prop_telToListInv
prop_wellScopedVars
PState
PStr
ptext
Ptr
PublicAccess
publicModules
PublicNS
publicOpen
punctuate
1 (Function)
2 (Function)
pureTCM
pushContext
pushCurrentContext
pushLexState
putConPar
putDelayed
putIrrFilter
putMain
putStr
putStrLn
pwords
1 (Function)
2 (Function)