Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Index - P

PageModeAgda.Utils.Pretty
Pair 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
pairwiseFilterAgda.Compiler.Epic.Interface
ParenAgda.Syntax.Concrete
parenAgda.Syntax.Concrete.Operators
parenedAgda.Compiler.JS.Parser
ParenPAgda.Syntax.Concrete
parens 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
ParenVAgda.Syntax.Concrete.Operators.Parser
parse 
1 (Function)Agda.Utils.ReadP
2 (Function)Agda.Compiler.JS.Parser
3 (Function)Agda.Syntax.Parser.Monad
4 (Function)Agda.Syntax.Parser, Agda.Interaction.GhciTop
parse'Agda.Utils.ReadP
parseAndDoAtToplevelAgda.Interaction.GhciTop
parseApplicationAgda.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
parseErrorAgda.Syntax.Parser.Monad
parseErrorAtAgda.Syntax.Parser.Monad
parseExpr 
1 (Function)Agda.Interaction.BasicOps
2 (Function)Agda.Interaction.CommandLine.CommandLine
parseExprInAgda.Interaction.BasicOps
ParseFailedAgda.Syntax.Parser.Monad
parseFileAgda.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
parseFlagsAgda.Syntax.Parser.Monad
parseInpAgda.Syntax.Parser.Monad
parseKeepCommentsAgda.Syntax.Parser.Monad
parseLastPosAgda.Syntax.Parser.Monad
parseLayoutAgda.Syntax.Parser.Monad
parseLexStateAgda.Syntax.Parser.Monad
parseLHSAgda.Syntax.Concrete.Operators
parseLiterateAgda.Syntax.Parser, Agda.Interaction.GhciTop
ParseOkAgda.Syntax.Parser.Monad
parsePluginOptionsAgda.Interaction.Options
parsePosAgda.Syntax.Parser.Monad
parsePosString 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.Syntax.Parser, Agda.Interaction.GhciTop
parsePragmaOptionsAgda.Interaction.Options
parsePrevCharAgda.Syntax.Parser.Monad
parsePrevTokenAgda.Syntax.Parser.Monad
Parser 
1 (Type/Class)Agda.Compiler.JS.Parser
2 (Type/Class)Agda.Syntax.Parser.Monad
3 (Type/Class)Agda.Syntax.Parser, Agda.Interaction.GhciTop
ParseResultAgda.Syntax.Parser.Monad
parseStandardOptionsAgda.Interaction.Options
ParseStateAgda.Syntax.Parser.Monad
partPAgda.Syntax.Concrete.Operators.Parser
PatAgda.Auto.Syntax
PatConAppAgda.Auto.Syntax
PatExpAgda.Auto.Syntax
PatInfoAgda.Syntax.Info
PatNameAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
PatRangeAgda.Syntax.Info
patsAgda.Compiler.JS.Case
PatSourceAgda.Syntax.Info
patsToTermsAgda.TypeChecking.With
PattAgda.Compiler.JS.Case
Pattern 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Abstract
patternAgda.Compiler.JS.Compiler
Pattern'Agda.Syntax.Abstract
PatternErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
patternHeadAgda.Syntax.Concrete
patternNamesAgda.Syntax.Concrete
PatternShadowsConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
patternToTermAgda.Compiler.Epic.Injection
patternViolationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PatVarAgda.Auto.Syntax
PBAgda.Auto.NarrowingSearch
PBlockedAgda.Auto.NarrowingSearch
pconNameAgda.Compiler.MAlonzo.Primitives
PConstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PDoubleBlockedAgda.Auto.NarrowingSearch
PEConAppAgda.Auto.Typecheck
PENoAgda.Auto.Typecheck
performKillAgda.TypeChecking.MetaVars.Occurs
PermAgda.Utils.Permutation
PermutationAgda.Utils.Permutation
permuteAgda.Utils.Permutation
PersistentTCStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PersistentTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PEvalAgda.Auto.Typecheck
pfailAgda.Utils.ReadP
pHiddenAgda.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
piAbstractTermAgda.TypeChecking.Abstract
piApplyAgda.TypeChecking.Substitute
piApplyMAgda.TypeChecking.Telescope
piApplyM'Agda.Compiler.Epic.Forcing
piBracketsAgda.Syntax.Fixity
pickidAgda.Auto.Typecheck
piFreqAgda.TypeChecking.Test.Generators
PiHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
PiNotLamAgda.TypeChecking.Rules.Term
PiShAgda.TypeChecking.Rules.LHS.Unify
plugHoleAgda.Syntax.Internal.Pattern
PlusAgda.Syntax.Internal
PlusLevelAgda.Syntax.Internal
PnAgda.Syntax.Position, Agda.Interaction.GhciTop
polaritiesAgda.TypeChecking.Polarity
PolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
polarityAgda.TypeChecking.Polarity
popAgda.Compiler.JS.Case
popContextAgda.Syntax.Parser.Monad
popLexStateAgda.Syntax.Parser.Monad
popMapSAgda.Auto.Convert
posColAgda.Syntax.Position, Agda.Interaction.GhciTop
PositionAgda.Syntax.Position, Agda.Interaction.GhciTop
positionInvariantAgda.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
positiveAgda.Utils.TestHelpers
positivityCheckEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
posLineAgda.Syntax.Position, Agda.Interaction.GhciTop
posPosAgda.Syntax.Position, Agda.Interaction.GhciTop
PossiblyAgda.TypeChecking.Rules.LHS.Unify
postfixPAgda.Syntax.Concrete.Operators.Parser
postopAgda.Syntax.Concrete.Operators.Parser
posToRangeAgda.Syntax.Position, Agda.Interaction.GhciTop
PostponedTypeCheckingProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
postponeTypeCheckingProblemAgda.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
pragmaOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
PrecedenceAgda.Syntax.Fixity
PredAgda.TypeChecking.Primitive
PrefixAgda.Utils.List
prefixAgda.Compiler.JS.Compiler
PrefixDefAgda.Syntax.Common
prefixPAgda.Syntax.Concrete.Operators.Parser
pRelevanceAgda.Syntax.Concrete.Pretty
preMetaAgda.Interaction.GhciTop
PreOpAgda.Compiler.JS.Syntax
preop 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Concrete.Operators.Parser
PrettiesAgda.Compiler.JS.Pretty
prettiesAgda.Compiler.JS.Pretty
Pretty 
1 (Type/Class)Agda.Utils.Pretty
2 (Type/Class)Agda.Compiler.JS.Pretty
pretty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
prettyA 
1 (Function)Agda.Syntax.Abstract.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyATopAgda.Syntax.Abstract.Pretty
prettyBehaviourAgda.Termination.CallGraph
PrettyContext 
1 (Type/Class)Agda.TypeChecking.Pretty
2 (Data Constructor)Agda.TypeChecking.Pretty
prettyContextAgda.Interaction.GhciTop
prettyEpicAgda.Compiler.Epic.Epic
prettyEpicFunAgda.Compiler.Epic.Epic
prettyErrorAgda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyGraphAgda.TypeChecking.Positivity
prettyListAgda.TypeChecking.Pretty
prettyPrecAgda.Utils.Pretty
prettyPrintAgda.Compiler.MAlonzo.Pretty
PrettyTCMAgda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyTCMAgda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop
prettyTypeOfMetaAgda.Interaction.GhciTop
preUscoreAgda.Interaction.GhciTop
PreviousInputAgda.Syntax.Parser.Alex
prFalseAgda.Compiler.Epic.Primitive
PrimAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primAgdaDataDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataConstructorAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionDataDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionFunDefAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionPostulateAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionPrimitiveAgda.TypeChecking.Monad.Builtin
primAgdaDefinitionRecordDefAgda.TypeChecking.Monad.Builtin
primAgdaFunDefAgda.TypeChecking.Monad.Builtin
primAgdaRecordDefAgda.TypeChecking.Monad.Builtin
primAgdaSortAgda.TypeChecking.Monad.Builtin
primAgdaSortLitAgda.TypeChecking.Monad.Builtin
primAgdaSortSetAgda.TypeChecking.Monad.Builtin
primAgdaSortUnsupportedAgda.TypeChecking.Monad.Builtin
primAgdaTermAgda.TypeChecking.Monad.Builtin
primAgdaTermConAgda.TypeChecking.Monad.Builtin
primAgdaTermDefAgda.TypeChecking.Monad.Builtin
primAgdaTermLamAgda.TypeChecking.Monad.Builtin
primAgdaTermPiAgda.TypeChecking.Monad.Builtin
primAgdaTermSortAgda.TypeChecking.Monad.Builtin
primAgdaTermUnsupportedAgda.TypeChecking.Monad.Builtin
primAgdaTermVarAgda.TypeChecking.Monad.Builtin
primAgdaTypeAgda.TypeChecking.Monad.Builtin
primAgdaTypeElAgda.TypeChecking.Monad.Builtin
primArgAgda.TypeChecking.Monad.Builtin
primArgArgAgda.TypeChecking.Monad.Builtin
primBodyAgda.Compiler.MAlonzo.Primitives
primBoolAgda.TypeChecking.Monad.Builtin
primCharAgda.TypeChecking.Monad.Builtin
primClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primConsAgda.TypeChecking.Monad.Builtin
primDataConstructorsAgda.TypeChecking.Primitive
PrimeAgda.Utils.Suffix
primEqualityAgda.TypeChecking.Monad.Builtin
primExprAgda.Compiler.Epic.Primitive
primFalseAgda.TypeChecking.Monad.Builtin
primFlatAgda.TypeChecking.Monad.Builtin
primFloatAgda.TypeChecking.Monad.Builtin
PrimFun 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunAgda.Compiler.Epic.Primitive
primFunArityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunImplementationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primFunNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primHiddenAgda.TypeChecking.Monad.Builtin
primHidingAgda.TypeChecking.Monad.Builtin
PrimImplAgda.TypeChecking.Primitive
primInfAgda.TypeChecking.Monad.Builtin
primInstanceAgda.TypeChecking.Monad.Builtin
primIntegerAgda.TypeChecking.Monad.Builtin
primIOAgda.TypeChecking.Monad.Builtin
primIrrelevantAgda.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
PrimitiveFunctionAgda.Syntax.Concrete.Definitions
primitiveFunctionsAgda.TypeChecking.Primitive
PrimitiveImplAgda.TypeChecking.Primitive
PrimitiveTypeAgda.Interaction.Highlighting.Precise
primitiviseAgda.Compiler.Epic.Primitive
primLevelAgda.TypeChecking.Monad.Builtin
primLevelMaxAgda.TypeChecking.Monad.Builtin
primLevelSucAgda.TypeChecking.Monad.Builtin
primLevelZeroAgda.TypeChecking.Monad.Builtin
primListAgda.TypeChecking.Monad.Builtin
primNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
primNatAgda.TypeChecking.Monad.Builtin
primNatCaseZDAgda.Compiler.Epic.Primitive
primNatCaseZSAgda.Compiler.Epic.Primitive
primNatDivSucAuxAgda.TypeChecking.Monad.Builtin
primNatEqualityAgda.TypeChecking.Monad.Builtin
primNatLessAgda.TypeChecking.Monad.Builtin
primNatMinusAgda.TypeChecking.Monad.Builtin
primNatModSucAuxAgda.TypeChecking.Monad.Builtin
primNatPlusAgda.TypeChecking.Monad.Builtin
primNatTimesAgda.TypeChecking.Monad.Builtin
primNilAgda.TypeChecking.Monad.Builtin
primQNameAgda.TypeChecking.Monad.Builtin
primQNameDefinitionAgda.TypeChecking.Primitive
primQNameTypeAgda.TypeChecking.Primitive
primReflAgda.TypeChecking.Monad.Builtin
primRelevantAgda.TypeChecking.Monad.Builtin
primRelvanceAgda.TypeChecking.Monad.Builtin
primSharpAgda.TypeChecking.Monad.Builtin
primSizeAgda.TypeChecking.Monad.Builtin
primSizeInfAgda.TypeChecking.Monad.Builtin
primSizeSucAgda.TypeChecking.Monad.Builtin
primStringAgda.TypeChecking.Monad.Builtin
primSucAgda.TypeChecking.Monad.Builtin
PrimTagAgda.Compiler.Epic.Interface
PrimTermAgda.TypeChecking.Primitive
primTermAgda.TypeChecking.Primitive
PrimTFAgda.Compiler.Epic.Primitive
PrimTransformAgda.Compiler.Epic.Primitive
primTrueAgda.TypeChecking.Monad.Builtin
primTrustMeAgda.TypeChecking.Primitive
PrimTypeAgda.TypeChecking.Primitive
primTypeAgda.TypeChecking.Primitive
primVisibleAgda.TypeChecking.Monad.Builtin
primZeroAgda.TypeChecking.Monad.Builtin
printAgda.Utils.IO.Locale
printTestCaseAgda.Utils.QuickCheck
printUsageAgda.Main
printVersionAgda.Main
PrioAgda.Auto.NarrowingSearch
prioAbsurdLambdaAgda.Auto.SearchControl
prioCompareArgListAgda.Auto.SearchControl
prioCompBetaAgda.Auto.SearchControl
prioCompBetaStructuredAgda.Auto.SearchControl
prioCompChoiceAgda.Auto.SearchControl
prioCompCopyAgda.Auto.SearchControl
prioCompIotaAgda.Auto.SearchControl
prioCompUnifAgda.Auto.SearchControl
prioInferredTypeUnknownAgda.Auto.SearchControl
PrioMeta 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
prioNoAgda.Auto.SearchControl
prioNoIotaAgda.Auto.SearchControl
prioProjIndexAgda.Auto.SearchControl
prioTypecheckAgda.Auto.SearchControl
prioTypecheckArgListAgda.Auto.SearchControl
prioTypeUnknownAgda.Auto.SearchControl
PrivateAgda.Syntax.Concrete
PrivateAccessAgda.Syntax.Common
PrivateNSAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
prNatEqualityAgda.Compiler.Epic.Primitive
Problem 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
Problem'Agda.TypeChecking.Rules.LHS.Problem
ProblemConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ProblemId 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
problemInPatAgda.TypeChecking.Rules.LHS.Problem
problemOutPatAgda.TypeChecking.Rules.LHS.Problem
ProblemPartAgda.TypeChecking.Rules.LHS.Problem
problemTelAgda.TypeChecking.Rules.LHS.Problem
ProjAgda.Syntax.Internal
ProjectRootAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
projectRootAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
promoteAgda.Utils.QuickCheck
proofIrrelevanceAgda.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
propAgda.Syntax.Internal
propagatePrioAgda.Auto.NarrowingSearch
PropertyAgda.Utils.QuickCheck
propertyAgda.Utils.QuickCheck
propFreqAgda.TypeChecking.Test.Generators
PropMustBeSingletonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
prop_disjointAgda.Utils.Warshall
prop_distinct_fastDistinctAgda.Utils.List
prop_extractNthElementAgda.Utils.List
prop_flattenTelInvAgda.TypeChecking.Tests
prop_flattenTelScopeAgda.TypeChecking.Tests
prop_genericElemIndexAgda.Utils.List
prop_groupBy'Agda.Utils.List
prop_pathAgda.Utils.Warshall
prop_reorderTelStableAgda.TypeChecking.Tests
prop_smallerAgda.Utils.Warshall
prop_splitTelescopePermScopeAgda.TypeChecking.Tests
prop_splitTelescopeScopeAgda.TypeChecking.Tests
prop_stableAgda.Utils.Warshall
prop_telToListInvAgda.TypeChecking.Tests
prop_uniqByAgda.Utils.List
prop_wellScopedVarsAgda.TypeChecking.Test.Generators
prop_zipWith'Agda.Utils.List
prPredAgda.Compiler.Epic.Primitive
prSucAgda.Compiler.Epic.Primitive
prTrueAgda.Compiler.Epic.Primitive
pruneAgda.TypeChecking.MetaVars.Occurs
PrunedEverythingAgda.TypeChecking.MetaVars.Occurs
PrunedNothingAgda.TypeChecking.MetaVars.Occurs
PrunedSomethingAgda.TypeChecking.MetaVars.Occurs
PruneResultAgda.TypeChecking.MetaVars.Occurs
prZeroAgda.Compiler.Epic.Primitive
PStateAgda.Syntax.Parser.Monad
PStrAgda.Utils.Pretty
ptextAgda.Utils.Pretty
PtrAgda.Utils.Pointer
PublicAccessAgda.Syntax.Common
publicModulesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
PublicNSAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
publicOpenAgda.Syntax.Concrete
punctAgda.Compiler.JS.Parser
punctuate 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
pureTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
pushContextAgda.Syntax.Parser.Monad
pushCurrentContextAgda.Syntax.Parser.Monad
pushLexStateAgda.Syntax.Parser.Monad
putConArityAgda.Compiler.Epic.CompileState
putConstrTagAgda.Compiler.Epic.CompileState
putDelayedAgda.Compiler.Epic.CompileState
putForcedArgsAgda.Compiler.Epic.CompileState
putMainAgda.Compiler.Epic.CompileState
putResponseAgda.Interaction.EmacsCommand
putStrAgda.Utils.IO.Locale
putStrLnAgda.Utils.IO.Locale
pwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty