| PageMode | Agda.Utils.Pretty |
| Pair | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| pairwiseFilter | Agda.Compiler.Epic.Interface |
| parallelS | Agda.TypeChecking.Substitute |
| Paren | Agda.Syntax.Concrete |
| paren | Agda.Syntax.Concrete.Operators |
| parened | Agda.Compiler.JS.Parser |
| ParenP | Agda.Syntax.Concrete |
| parens | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| parens' | Agda.Interaction.InteractionTop |
| ParenV | Agda.Syntax.Concrete.Operators.Parser |
| Parse | Agda.Interaction.InteractionTop |
| parse | |
| 1 (Function) | Agda.Utils.ReadP |
| 2 (Function) | Agda.Compiler.JS.Parser |
| 3 (Function) | Agda.Syntax.Parser.Monad |
| 4 (Function) | Agda.Syntax.Parser |
| parse' | Agda.Utils.ReadP |
| parseAndDoAtToplevel | Agda.Interaction.InteractionTop |
| parseApplication | Agda.Syntax.Concrete.Operators |
| ParseError | |
| 1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| 2 (Data Constructor) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| parseError | Agda.Syntax.Parser.Monad |
| 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 |
| 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 |
| parseName | Agda.Interaction.BasicOps |
| ParseOk | Agda.Syntax.Parser.Monad |
| parsePat | Agda.Syntax.Concrete.Operators |
| parsePattern | Agda.Syntax.Concrete.Operators |
| parsePatternSyn | Agda.Syntax.Concrete.Operators |
| parsePluginOptions | Agda.Interaction.Options |
| parsePos | Agda.Syntax.Parser.Monad |
| parsePosString | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.Syntax.Parser |
| parsePragmaOptions | Agda.Interaction.Options |
| parsePrevChar | Agda.Syntax.Parser.Monad |
| parsePrevToken | Agda.Syntax.Parser.Monad |
| Parser | |
| 1 (Type/Class) | Agda.Compiler.JS.Parser |
| 2 (Type/Class) | Agda.Syntax.Parser.Monad |
| 3 (Type/Class) | Agda.Syntax.Parser |
| ParseResult | Agda.Syntax.Parser.Monad |
| parseStandardOptions | Agda.Interaction.Options |
| ParseState | Agda.Syntax.Parser.Monad |
| parseToReadsPrec | Agda.Interaction.InteractionTop |
| parseVariables | Agda.Interaction.MakeCase |
| Parsing | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| Partial | Agda.Interaction.Highlighting.Generate |
| PartialOrd | Agda.Utils.PartialOrd |
| PartialOrdering | Agda.Utils.PartialOrd |
| partitionMaybe | Agda.Utils.List |
| partP | Agda.Syntax.Concrete.Operators.Parser |
| Pat | Agda.Auto.Syntax |
| PatConApp | Agda.Auto.Syntax |
| PatExp | Agda.Auto.Syntax |
| patImplicit | Agda.Syntax.Info |
| PatInfo | Agda.Syntax.Info |
| patInfo | Agda.Syntax.Info |
| PatName | Agda.Syntax.Translation.ConcreteToAbstract |
| patNoRange | Agda.Syntax.Info |
| PatRange | Agda.Syntax.Info |
| pats | Agda.Compiler.JS.Case |
| PatSource | Agda.Syntax.Info |
| patsToTerms | Agda.TypeChecking.With |
| Patt | Agda.Compiler.JS.Case |
| Pattern | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| 3 (Type/Class) | Agda.Syntax.Internal |
| pattern | Agda.Compiler.JS.Compiler |
| Pattern' | Agda.Syntax.Abstract |
| patternAppView | Agda.Syntax.Concrete.Operators |
| PatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| patternHead | Agda.Syntax.Concrete |
| patternNames | Agda.Syntax.Concrete |
| patternQNames | Agda.Syntax.Concrete.Operators |
| Patterns | Agda.Syntax.Abstract |
| PatternShadowsConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| patternsToElims | Agda.Syntax.Internal.Pattern |
| PatternSyn | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| PatternSynDef | Agda.Syntax.Abstract |
| PatternSynDefn | Agda.Syntax.Abstract |
| PatternSynDefns | Agda.Syntax.Abstract |
| PatternSynName | Agda.Syntax.Scope.Base |
| PatternSynonymArityMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PatternSynP | Agda.Syntax.Abstract |
| PatternSynResName | Agda.Syntax.Scope.Monad |
| patternToExpr | Agda.Syntax.Abstract |
| patternToTerm | Agda.Compiler.Epic.Injection |
| patternVars | Agda.Syntax.Internal |
| patternViolation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| patternViolation' | Agda.TypeChecking.MetaVars.Occurs |
| PatVar | Agda.Auto.Syntax |
| PB | Agda.Auto.NarrowingSearch |
| PBlocked | Agda.Auto.NarrowingSearch |
| pColors | Agda.Syntax.Concrete.Pretty |
| pconName | Agda.Compiler.MAlonzo.Primitives |
| PConstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PDoubleBlocked | Agda.Auto.NarrowingSearch |
| PEConApp | Agda.Auto.Typecheck |
| PENo | Agda.Auto.Typecheck |
| performedSimplification | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| performedSimplification' | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| performKill | Agda.TypeChecking.MetaVars.Occurs |
| Perm | Agda.Utils.Permutation |
| permPicks | Agda.Utils.Permutation |
| permRange | Agda.Utils.Permutation |
| Permutation | Agda.Utils.Permutation |
| permute | Agda.Utils.Permutation |
| PersistentTCSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PersistentTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PersistentVerbosity | Agda.Interaction.Options.Lenses |
| PEval | Agda.Auto.Typecheck |
| pfail | Agda.Utils.ReadP |
| Phase | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| pHidden | Agda.Syntax.Concrete.Pretty |
| Pi | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| piAbstractTerm | Agda.TypeChecking.Abstract |
| piApply | Agda.TypeChecking.Substitute |
| piApplyM | Agda.TypeChecking.Telescope |
| piApplyM' | Agda.Compiler.Epic.Forcing |
| piBrackets | Agda.Syntax.Fixity |
| pickid | Agda.Auto.Typecheck |
| piFreq | Agda.TypeChecking.Test.Generators |
| PiHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PiNotLam | Agda.TypeChecking.Rules.Term |
| PiSh | Agda.TypeChecking.Rules.LHS.Unify |
| plugHole | Agda.Syntax.Internal.Pattern |
| Plus | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Utils |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| plus | Agda.TypeChecking.SizedTypes.Utils |
| PlusLevel | Agda.Syntax.Internal |
| Pn | Agda.Syntax.Position |
| POAny | Agda.Utils.PartialOrd |
| POEQ | Agda.Utils.PartialOrd |
| POGE | Agda.Utils.PartialOrd |
| POGT | Agda.Utils.PartialOrd |
| point | Agda.Utils.Pointed |
| Pointed | Agda.Utils.Pointed |
| pointerChain | Agda.Syntax.Internal |
| Pointwise | |
| 1 (Type/Class) | Agda.Utils.PartialOrd |
| 2 (Data Constructor) | Agda.Utils.PartialOrd |
| pointwise | Agda.Utils.PartialOrd |
| Polarities | Agda.TypeChecking.SizedTypes.Syntax |
| polarities | Agda.TypeChecking.Polarity |
| polaritiesFromAssignments | Agda.TypeChecking.SizedTypes.Syntax |
| Polarity | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| polarity | Agda.TypeChecking.Polarity |
| PolarityAssignment | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| POLE | Agda.Utils.PartialOrd |
| polFromOcc | Agda.TypeChecking.Polarity |
| POLT | Agda.Utils.PartialOrd |
| polyQuickCheck | Agda.Utils.QuickCheck |
| polyVerboseCheck | Agda.Utils.QuickCheck |
| pop | Agda.Compiler.JS.Case |
| popContext | Agda.Syntax.Parser.Monad |
| popLexState | Agda.Syntax.Parser.Monad |
| popMapS | Agda.Auto.Convert |
| posCol | Agda.Syntax.Position |
| Position | Agda.Syntax.Position |
| Position' | Agda.Syntax.Position |
| positionInvariant | Agda.Syntax.Position |
| Positive | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| positive | Agda.Utils.TestHelpers |
| Positivity | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| posLine | Agda.Syntax.Position |
| posPos | Agda.Syntax.Position |
| Possibly | Agda.TypeChecking.Rules.LHS.Unify |
| postfixP | Agda.Syntax.Concrete.Operators.Parser |
| postop | Agda.Syntax.Concrete.Operators.Parser |
| posToRange | Agda.Syntax.Position |
| PostponedCheckArgs | Agda.Interaction.BasicOps |
| PostponedTypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| postponeTypeCheckingProblem | Agda.TypeChecking.MetaVars |
| postponeTypeCheckingProblem_ | Agda.TypeChecking.MetaVars |
| 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 |
| predecessor | Agda.Utils.List |
| Prefix | Agda.Utils.List |
| prefix | Agda.Compiler.JS.Compiler |
| PrefixDef | Agda.Syntax.Common |
| prefixP | Agda.Syntax.Concrete.Operators.Parser |
| pRelevance | Agda.Syntax.Concrete.Pretty |
| PreOp | Agda.Compiler.JS.Syntax |
| preop | |
| 1 (Function) | Agda.Compiler.JS.Parser |
| 2 (Function) | Agda.Syntax.Concrete.Operators.Parser |
| PreOrSuffix | Agda.Utils.List |
| preOrSuffix | Agda.Utils.List |
| Pretties | Agda.Compiler.JS.Pretty |
| pretties | Agda.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 |
| prettyAs | |
| 1 (Function) | Agda.Syntax.Abstract.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyATop | Agda.Syntax.Abstract.Pretty |
| PrettyContext | |
| 1 (Type/Class) | Agda.TypeChecking.Pretty |
| 2 (Data Constructor) | Agda.TypeChecking.Pretty |
| prettyContext | Agda.Interaction.InteractionTop |
| prettyEpic | Agda.Compiler.Epic.Epic |
| prettyEpicFun | Agda.Compiler.Epic.Epic |
| prettyError | Agda.TypeChecking.Errors |
| prettyList | Agda.TypeChecking.Pretty |
| prettyMap | Agda.TypeChecking.CompiledClause |
| prettyOpApp | Agda.Syntax.Concrete.Pretty |
| prettyPrec | Agda.Utils.Pretty |
| prettyPrint | Agda.Compiler.MAlonzo.Pretty |
| PrettyTCM | Agda.TypeChecking.Pretty, Agda.TypeChecking.Errors |
| prettyTCM | Agda.TypeChecking.Pretty, Agda.TypeChecking.Errors |
| prettyTypeOfMeta | Agda.Interaction.InteractionTop |
| PreviousInput | Agda.Syntax.Parser.Alex |
| prFalse | Agda.Compiler.Epic.Primitive |
| Prim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primAgdaDataDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinition | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionDataConstructor | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionDataDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionFunDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionPostulate | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionPrimitive | Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionRecordDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaFunDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaRecordDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaSort | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortLit | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortSet | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortUnsupported | Agda.TypeChecking.Monad.Builtin |
| 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 |
| primAgdaType | Agda.TypeChecking.Monad.Builtin |
| primAgdaTypeEl | Agda.TypeChecking.Monad.Builtin |
| primArg | Agda.TypeChecking.Monad.Builtin |
| primArgArg | Agda.TypeChecking.Monad.Builtin |
| primArgArgInfo | Agda.TypeChecking.Monad.Builtin |
| primArgInfo | 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 |
| primDataConstructors | Agda.TypeChecking.Primitive |
| Prime | Agda.Utils.Suffix |
| primEquality | Agda.TypeChecking.Monad.Builtin |
| primEqualityName | 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 |
| primHidden | Agda.TypeChecking.Monad.Builtin |
| primHiding | Agda.TypeChecking.Monad.Builtin |
| PrimImpl | Agda.TypeChecking.Primitive |
| primInf | Agda.TypeChecking.Monad.Builtin |
| primInstance | Agda.TypeChecking.Monad.Builtin |
| primInteger | Agda.TypeChecking.Monad.Builtin |
| primIO | Agda.TypeChecking.Monad.Builtin |
| primIrrAxiom | Agda.TypeChecking.Monad.Builtin |
| primIrrelevant | 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 |
| 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 |
| primQNameDefinition | Agda.TypeChecking.Primitive |
| primQNameType | Agda.TypeChecking.Primitive |
| primRefl | Agda.TypeChecking.Monad.Builtin |
| primRelevance | Agda.TypeChecking.Monad.Builtin |
| primRelevant | Agda.TypeChecking.Monad.Builtin |
| primSharp | Agda.TypeChecking.Monad.Builtin |
| primSize | Agda.TypeChecking.Monad.Builtin |
| primSizeInf | Agda.TypeChecking.Monad.Builtin |
| primSizeLt | Agda.TypeChecking.Monad.Builtin |
| primSizeMax | Agda.TypeChecking.Monad.Builtin |
| primSizeSuc | Agda.TypeChecking.Monad.Builtin |
| primString | Agda.TypeChecking.Monad.Builtin |
| primSuc | Agda.TypeChecking.Monad.Builtin |
| PrimTag | Agda.Compiler.Epic.Interface |
| 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 |
| primVisible | Agda.TypeChecking.Monad.Builtin |
| primZero | Agda.TypeChecking.Monad.Builtin |
| printErrorInfo | Agda.Interaction.Highlighting.Generate |
| printHighlightingInfo | Agda.Interaction.Highlighting.Generate |
| printScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| printTestCase | Agda.Utils.QuickCheck |
| printUnsolvedInfo | Agda.Interaction.Highlighting.Generate |
| 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 |
| prNatEquality | Agda.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 |
| ProblemConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| problemFromPats | Agda.TypeChecking.Rules.LHS.ProblemRest |
| ProblemId | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| problemInPat | Agda.TypeChecking.Rules.LHS.Problem |
| problemOutPat | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemPart | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemRest | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| problemRest | Agda.TypeChecking.Rules.LHS.Problem |
| problemTel | Agda.TypeChecking.Rules.LHS.Problem |
| problemType | Agda.TypeChecking.MetaVars |
| Proj | Agda.Syntax.Internal |
| ProjDBP | Agda.Termination.Monad |
| projDropPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ProjectedVar | Agda.TypeChecking.MetaVars |
| Projection | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| projectionArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| ProjectionLikeness | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| projectionMismatch | Agda.TypeChecking.Rules.LHS.Unify |
| ProjectionReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ProjectionView | |
| 1 (Type/Class) | Agda.TypeChecking.ProjectionLike |
| 2 (Data Constructor) | Agda.TypeChecking.ProjectionLike |
| ProjectRoot | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| projectRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| projectType | Agda.TypeChecking.Records |
| projFreq | Agda.TypeChecking.Test.Generators |
| projFromType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| projIndex | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ProjMP | Agda.TypeChecking.Coverage.Match |
| ProjName | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| ProjP | Agda.Syntax.Internal |
| projProper | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| projUseSizeLt | Agda.Termination.Monad |
| ProjVarExc | |
| 1 (Type/Class) | Agda.TypeChecking.MetaVars |
| 2 (Data Constructor) | Agda.TypeChecking.MetaVars |
| projView | Agda.TypeChecking.ProjectionLike |
| projViewProj | Agda.TypeChecking.ProjectionLike |
| projViewSelf | Agda.TypeChecking.ProjectionLike |
| projViewSpine | Agda.TypeChecking.ProjectionLike |
| proofIrrelevance | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Prop | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| prop | Agda.Syntax.Internal |
| propagatePrio | Agda.Auto.NarrowingSearch |
| propAssociative | Agda.TypeChecking.SizedTypes.Tests |
| propBoundedSemiLattice | Agda.TypeChecking.SizedTypes.Tests |
| propCommutative | Agda.TypeChecking.SizedTypes.Tests |
| propDioid | Agda.TypeChecking.SizedTypes.Tests |
| propDioid_Gen | Agda.TypeChecking.SizedTypes.Tests |
| propDistL | Agda.TypeChecking.SizedTypes.Tests |
| propDistR | Agda.TypeChecking.SizedTypes.Tests |
| propDistributive | Agda.TypeChecking.SizedTypes.Tests |
| properlyMatching | Agda.Syntax.Internal |
| Property | Agda.Utils.QuickCheck |
| property | Agda.Utils.QuickCheck |
| property_not_null_singleton | Agda.Utils.Favorites |
| property_null_empty | Agda.Utils.Favorites |
| property_seqPO | Agda.Utils.PartialOrd |
| propFreq | Agda.TypeChecking.Test.Generators |
| propIdempotent | Agda.TypeChecking.SizedTypes.Tests |
| propMonoid | Agda.TypeChecking.SizedTypes.Tests |
| PropMustBeSingleton | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| propSemiLattice | Agda.TypeChecking.SizedTypes.Tests |
| propUnit | Agda.TypeChecking.SizedTypes.Tests |
| propZero | Agda.TypeChecking.SizedTypes.Tests |
| prop_associative_orPO | Agda.Utils.PartialOrd |
| prop_associative_seqPO | Agda.Utils.PartialOrd |
| prop_BiMap_invariant | Agda.Utils.BiMap |
| prop_BoundedSemiLattice_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_commutative_orPO | Agda.Utils.PartialOrd |
| prop_commutative_seqPO | Agda.Utils.PartialOrd |
| prop_comparable_PartialOrdering | Agda.Utils.PartialOrd |
| prop_comparable_related | Agda.Utils.PartialOrd |
| prop_compareWithFavorites | Agda.Utils.Favorites |
| prop_ComposeComplete | Agda.TypeChecking.SizedTypes.Tests |
| prop_ComposeSound | Agda.TypeChecking.SizedTypes.Tests |
| prop_Dioid_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_Dioid_Weight | Agda.TypeChecking.SizedTypes.Tests |
| prop_disjoint | Agda.Utils.Warshall |
| prop_distinct_fastDistinct | Agda.Utils.List |
| prop_DistL_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_distributive_seqPO_orPO | Agda.Utils.PartialOrd |
| prop_DistR_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_Dist_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_extractNthElement | Agda.Utils.List |
| prop_flattenTelInv | Agda.TypeChecking.Tests |
| prop_flattenTelScope | Agda.TypeChecking.Tests |
| prop_fromList_after_toList | Agda.Utils.Favorites |
| prop_fromOrderings_after_toOrderings | Agda.Utils.PartialOrd |
| prop_galois | Agda.TypeChecking.Irrelevance |
| prop_genericElemIndex | Agda.Utils.List |
| prop_groupBy' | Agda.Utils.List |
| prop_identity_seqPO | Agda.Utils.PartialOrd |
| prop_MeetComplete | Agda.TypeChecking.SizedTypes.Tests |
| prop_MeetSound | Agda.TypeChecking.SizedTypes.Tests |
| prop_Monoid_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_oppPO | Agda.Utils.PartialOrd |
| prop_orPO_sound | Agda.Utils.PartialOrd |
| prop_path | Agda.Utils.Warshall |
| prop_related_pair | Agda.Utils.PartialOrd |
| prop_reorderTelStable | Agda.TypeChecking.Tests |
| prop_SemiLattice_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_seqPO | Agda.Utils.PartialOrd |
| prop_smaller | Agda.Utils.Warshall |
| prop_sorted_toOrderings | Agda.Utils.PartialOrd |
| prop_splitTelescopePermScope | Agda.TypeChecking.Tests |
| prop_splitTelescopeScope | Agda.TypeChecking.Tests |
| prop_stable | Agda.Utils.Warshall |
| prop_telToListInv | Agda.TypeChecking.Tests |
| prop_toOrderings_after_fromOrdering | Agda.Utils.PartialOrd |
| prop_toOrderings_after_fromOrderings | Agda.Utils.PartialOrd |
| prop_union_union2 | Agda.Utils.Favorites |
| prop_uniqBy | Agda.Utils.List |
| prop_Unit_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_wellScopedVars | Agda.TypeChecking.Test.Generators |
| prop_Zero_Label | Agda.TypeChecking.SizedTypes.Tests |
| prop_zero_orPO | Agda.Utils.PartialOrd |
| prop_zero_seqPO | Agda.Utils.PartialOrd |
| prop_zipWith' | Agda.Utils.List |
| prPred | Agda.Compiler.Epic.Primitive |
| prSuc | Agda.Compiler.Epic.Primitive |
| prTrue | Agda.Compiler.Epic.Primitive |
| prune | Agda.TypeChecking.MetaVars.Occurs |
| PrunedEverything | Agda.TypeChecking.MetaVars.Occurs |
| PrunedNothing | Agda.TypeChecking.MetaVars.Occurs |
| PrunedSomething | Agda.TypeChecking.MetaVars.Occurs |
| PruneResult | Agda.TypeChecking.MetaVars.Occurs |
| prZero | Agda.Compiler.Epic.Primitive |
| PState | Agda.Syntax.Parser.Monad |
| PStr | Agda.Utils.Pretty |
| ptext | Agda.Utils.Pretty |
| Ptr | Agda.Utils.Pointer, Agda.Syntax.Internal |
| PublicAccess | Agda.Syntax.Common |
| publicModules | Agda.Syntax.Scope.Base |
| PublicNS | Agda.Syntax.Scope.Base |
| publicOpen | Agda.Syntax.Concrete |
| punct | Agda.Compiler.JS.Parser |
| punctuate | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| pureTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| purgeNonvariant | Agda.TypeChecking.Polarity |
| pushContext | Agda.Syntax.Parser.Monad |
| pushCurrentContext | Agda.Syntax.Parser.Monad |
| pushLexState | Agda.Syntax.Parser.Monad |
| putAllConstraintsToSleep | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| putConArity | Agda.Compiler.Epic.CompileState |
| putConstrTag | Agda.Compiler.Epic.CompileState |
| putDelayed | Agda.Compiler.Epic.CompileState |
| putForcedArgs | Agda.Compiler.Epic.CompileState |
| putIncludeDirs | Agda.Interaction.Options.Lenses |
| putMain | Agda.Compiler.Epic.CompileState |
| putPersistentVerbosity | Agda.Interaction.Options.Lenses |
| putResponse | |
| 1 (Function) | Agda.Interaction.EmacsCommand |
| 2 (Function) | Agda.Interaction.InteractionTop |
| putSafeMode | Agda.Interaction.Options.Lenses |
| putVerbosity | Agda.Interaction.Options.Lenses |
| pwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |