A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
$
&
+
.
/
<
=
>
|
-
All

Index - P

PageMode	Agda.Utils.Pretty
Pair
1 (Type/Class)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Auto.NarrowingSearch
pairwiseFilter	Agda.Compiler.Epic.AuxAST
Paren	Agda.Syntax.Concrete
paren	Agda.Syntax.Concrete.Operators
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.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
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.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
pconName	Agda.Compiler.MAlonzo.Primitives
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
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
piBrackets	Agda.Syntax.Fixity
pickid	Agda.Auto.Typecheck
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
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
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
PrefixDef	Agda.Syntax.Common
prefixP	Agda.Syntax.Concrete.Operators.Parser
pRelevance	Agda.Syntax.Concrete.Pretty
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
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
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
Prim	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primAbstr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
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
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
PrimImpl	Agda.TypeChecking.Primitive
primInf	Agda.TypeChecking.Monad.Builtin
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
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
primLists	Agda.Compiler.Epic.Primitive
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
primRefl	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
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
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
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
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_wellScopedVars	Agda.TypeChecking.Test.Generators
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
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
putConPar	Agda.Compiler.Epic.CompileState
putDelayed	Agda.Compiler.Epic.CompileState
putIrrFilter	Agda.Compiler.Epic.CompileState
putMain	Agda.Compiler.Epic.CompileState
putStr	Agda.Utils.IO.Locale
putStrLn	Agda.Utils.IO.Locale
pwords
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty