| P64ToI | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| package | Agda.Version |
| packUnquoteM | Agda.TypeChecking.Unquote |
| PAdd | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PAdd64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PageMode | Agda.Utils.Pretty |
| Pair | |
| 1 (Type/Class) | Agda.Utils.Tuple |
| 2 (Data Constructor) | Agda.Utils.Tuple |
| PairInt | |
| 1 (Type/Class) | Agda.Utils.RangeMap |
| 2 (Data Constructor) | Agda.Utils.RangeMap |
| pairs | Agda.Interaction.JSON |
| PApp | Agda.Utils.Haskell.Syntax |
| parallelS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| Paren | Agda.Syntax.Concrete |
| ParenP | Agda.Syntax.Concrete |
| ParenPreference | Agda.Syntax.Fixity |
| parens | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| 3 (Function) | Agda.TypeChecking.Pretty |
| parens' | Agda.Interaction.Base |
| parensNonEmpty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| ParenV | Agda.Syntax.Concrete.Operators.Parser |
| Parse | Agda.Interaction.Base |
| parse | |
| 1 (Function) | Agda.Utils.Parser.MemoisedCPS |
| 2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad |
| 3 (Function) | Agda.Syntax.Parser.Monad |
| 4 (Function) | Agda.Syntax.Concrete.Operators.Parser |
| 5 (Function) | Agda.Syntax.Parser |
| parseAndDoAtToplevel | Agda.Interaction.InteractionTop |
| parseApplication | Agda.Syntax.Concrete.Operators |
| parseArgs | Agda.Auto.Options |
| parseBackendOptions | Agda.Compiler.Backend |
| 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 |
| parseErrorRange | Agda.Syntax.Parser.Monad |
| parseExpr | Agda.Interaction.BasicOps |
| parseExprIn | Agda.Interaction.BasicOps |
| ParseFailed | 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 |
| parseFromSrc | Agda.Syntax.Parser.Monad |
| parseHaskellPragma | Agda.Compiler.MAlonzo.Pragmas |
| parseIdiomBracketsSeq | Agda.Syntax.IdiomBrackets |
| parseIndexedJSON | Agda.Interaction.JSON |
| parseInp | Agda.Syntax.Parser.Monad |
| parseJSON | Agda.Interaction.JSON |
| parseJSON1 | Agda.Interaction.JSON |
| parseJSON2 | Agda.Interaction.JSON |
| parseJSONList | Agda.Interaction.JSON |
| parseKeepComments | Agda.Syntax.Parser.Monad |
| parseLastPos | Agda.Syntax.Parser.Monad |
| parseLayKw | Agda.Syntax.Parser.Monad |
| parseLayout | Agda.Syntax.Parser.Monad |
| parseLayStatus | Agda.Syntax.Parser.Monad |
| parseLexState | Agda.Syntax.Parser.Monad |
| parseLHS | Agda.Syntax.Concrete.Operators |
| parseLibFile | Agda.Interaction.Library.Parse |
| parseModuleApplication | Agda.Syntax.Concrete.Operators |
| parseName | Agda.Interaction.BasicOps |
| ParseOk | Agda.Syntax.Parser.Monad |
| 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 |
| parsePragma | Agda.Compiler.MAlonzo.Pragmas |
| parsePragmaOptions | Agda.Interaction.Options |
| parsePrevChar | Agda.Syntax.Parser.Monad |
| parsePrevToken | Agda.Syntax.Parser.Monad |
| Parser | |
| 1 (Type/Class) | Agda.Utils.Parser.MemoisedCPS |
| 2 (Type/Class) | Agda.Syntax.Concrete.Operators.Parser.Monad |
| 3 (Type/Class) | Agda.Syntax.Parser.Monad |
| 4 (Type/Class) | Agda.Syntax.Parser |
| parserBased | Agda.Interaction.Highlighting.Precise |
| ParserClass | Agda.Utils.Parser.MemoisedCPS |
| ParseResult | Agda.Syntax.Parser.Monad |
| ParserWithGrammar | Agda.Utils.Parser.MemoisedCPS |
| ParseSections | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Operators.Parser |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Operators.Parser |
| parseSource | Agda.Interaction.Imports |
| parseSrcFile | Agda.Syntax.Parser.Monad |
| ParseState | Agda.Syntax.Parser.Monad |
| parseTime | Agda.Auto.Options |
| parseToReadsPrec | Agda.Interaction.Base |
| parseVariables | Agda.Interaction.MakeCase |
| parseVerboseKey | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ParseWarning | |
| 1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| parseWarning | Agda.Syntax.Parser.Monad |
| parseWarningName | Agda.Syntax.Parser.Monad |
| parseWarnings | Agda.Syntax.Parser.Monad |
| Parsing | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| Partial | Agda.Interaction.Highlighting.Generate |
| PartialOrd | Agda.Utils.PartialOrd |
| PartialOrdering | Agda.Utils.PartialOrd |
| partition | Agda.Utils.List1 |
| partition3 | Agda.Utils.Three |
| partitionByKindOfForeignCode | Agda.Compiler.MAlonzo.Pragmas |
| partitionEithers | Agda.Utils.List1 |
| partitionEithers3 | Agda.Utils.Three |
| partitionImportedNames | Agda.Syntax.Common |
| partitionM | Agda.Utils.Monad |
| partitionMaybe | Agda.Utils.List |
| partP | Agda.Syntax.Concrete.Operators.Parser |
| PAsPat | Agda.Utils.Haskell.Syntax |
| Pat | |
| 1 (Type/Class) | Agda.Utils.Haskell.Syntax |
| 2 (Type/Class) | Agda.Auto.Syntax |
| patAsNames | Agda.Syntax.Internal |
| PatConApp | Agda.Auto.Syntax |
| PatExp | Agda.Auto.Syntax |
| path | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| PathCons | Agda.TypeChecking.Rules.Data |
| pathLevel | Agda.Syntax.Internal |
| pathLhs | Agda.Syntax.Internal |
| pathName | Agda.Syntax.Internal |
| pathRhs | Agda.Syntax.Internal |
| pathSort | Agda.Syntax.Internal |
| PathType | Agda.Syntax.Internal |
| pathType | Agda.Syntax.Internal |
| pathUnview | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| PathView | Agda.Syntax.Internal |
| pathView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| pathView' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| pathViewAsPi | Agda.TypeChecking.Telescope |
| pathViewAsPi' | Agda.TypeChecking.Telescope |
| pathViewAsPi'whnf | Agda.TypeChecking.Telescope |
| PatInfo | Agda.Syntax.Info |
| patmMetas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| patmRemainder | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PatName | Agda.Syntax.Translation.ConcreteToAbstract |
| patNoRange | Agda.Syntax.Info |
| PatOAbsurd | Agda.Syntax.Internal |
| PatOCon | Agda.Syntax.Internal |
| PatODot | Agda.Syntax.Internal |
| PatOLit | Agda.Syntax.Internal |
| PatORec | Agda.Syntax.Internal |
| PatOrigin | Agda.Syntax.Internal |
| patOrigin | Agda.Syntax.Internal |
| PatOSplit | Agda.Syntax.Internal |
| PatOSystem | Agda.Syntax.Internal |
| PatOVar | Agda.Syntax.Internal |
| PatOWild | Agda.Syntax.Internal |
| PatRange | Agda.Syntax.Info |
| patsToElims | Agda.TypeChecking.With |
| PatSyn | Agda.Utils.Haskell.Syntax |
| Pattern | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Internal |
| 3 (Type/Class) | Agda.Syntax.Reflected |
| 4 (Type/Class) | Agda.Syntax.Abstract |
| Pattern' | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| patternAppView | Agda.Syntax.Concrete.Pattern |
| patternBinder | Agda.Syntax.Concrete.Operators.Parser |
| PatternBound | Agda.Syntax.Scope.Base |
| patternDepth | Agda.Termination.Monad |
| PatternErr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PatternFrom | Agda.TypeChecking.Rewriting.NonLinPattern |
| patternFrom | Agda.TypeChecking.Rewriting.NonLinPattern |
| PatternInfo | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| patternInfo | Agda.Syntax.Internal |
| patternInTeleName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PatternLike | Agda.Syntax.Internal.Pattern |
| PatternMatching | Agda.Syntax.Common |
| PatternMatchingAllowed | Agda.Syntax.Common |
| patternMatchingAllowed | Agda.Syntax.Common |
| patternNames | Agda.Syntax.Concrete.Pattern |
| PatternOrCopattern | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| patternOrigin | Agda.Syntax.Internal |
| patternQNames | Agda.Syntax.Concrete.Pattern |
| Patterns | Agda.Syntax.Abstract |
| PatternShadowsConstructor | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| patternsToElims | Agda.Syntax.Internal.Pattern |
| PatternSubstitution | Agda.Syntax.Internal |
| 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 |
| PatternSynP | Agda.Syntax.Abstract |
| PatternSynResName | Agda.Syntax.Scope.Base |
| patternToElim | Agda.Syntax.Internal.Pattern |
| patternToExpr | Agda.Syntax.Abstract |
| patternToModuleBound | Agda.Syntax.Scope.Base |
| patternToTerm | Agda.Syntax.Internal.Pattern |
| patternVariables | Agda.TypeChecking.Rules.LHS.Problem |
| PatternVarModalities | Agda.Syntax.Internal.Pattern |
| patternVarModalities | Agda.Syntax.Internal.Pattern |
| PatternVarOut | Agda.Syntax.Internal, Agda.Syntax.Internal |
| PatternVars | Agda.Syntax.Internal |
| patternVars | |
| 1 (Function) | Agda.Syntax.Internal |
| 2 (Function) | Agda.Syntax.Abstract.Pattern |
| patternView | Agda.Syntax.Concrete.Operators.Parser |
| patternViolation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| patternViolation' | Agda.TypeChecking.MetaVars.Occurs |
| PatTypeSig | Agda.Utils.Haskell.Syntax |
| PatVar | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.Syntax.Internal.Pattern |
| PatVarLabel | Agda.Syntax.Internal.Pattern |
| PatVarName | Agda.Syntax.Internal |
| patVarNameToString | Agda.Syntax.Internal |
| PB | Agda.Auto.NarrowingSearch |
| PBangPat | Agda.Utils.Haskell.Syntax |
| PBlocked | Agda.Auto.NarrowingSearch |
| PBoundVar | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PConstr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| pDom | Agda.Syntax.Internal |
| PDoubleBlocked | Agda.Auto.NarrowingSearch |
| PEConApp | Agda.Auto.Typecheck |
| PElims | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PENo | Agda.Auto.Typecheck |
| PEq64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PEqC | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PEqF | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PEqI | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PEqQ | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PEqS | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| performedSimplification | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| performedSimplification' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| 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 |
| permuteTel | Agda.TypeChecking.Telescope |
| PersistentTCSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PersistentTCState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PersistentVerbosity | Agda.Interaction.Options.Lenses |
| PEval | Agda.Auto.Typecheck |
| PGeq | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Phase | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| pHasEta0 | 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.Reflected |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| piAbstract | Agda.TypeChecking.Abstract |
| piAbstractTerm | Agda.TypeChecking.Abstract |
| piApply | Agda.TypeChecking.Substitute |
| PiApplyM | Agda.TypeChecking.Telescope |
| piApplyM | Agda.TypeChecking.Telescope |
| piApplyM' | Agda.TypeChecking.Telescope |
| piBrackets | Agda.Syntax.Fixity |
| pickid | Agda.Auto.Typecheck |
| pickName | Agda.TypeChecking.Unquote |
| pickUid | Agda.Auto.SearchControl |
| PIf | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PiHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PInf | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PiNotLam | Agda.TypeChecking.Rules.Term |
| piOrPath | Agda.TypeChecking.Telescope |
| PIrrPat | Agda.Utils.Haskell.Syntax |
| PiSort | Agda.Syntax.Internal |
| piSort | Agda.TypeChecking.Substitute |
| piSort' | Agda.TypeChecking.Substitute |
| PITo64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Placeholder | Agda.Syntax.Common |
| placeholder | Agda.Syntax.Concrete.Operators.Parser |
| PlainJS | Agda.Compiler.JS.Syntax |
| PLam | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PLit | Agda.Utils.Haskell.Syntax |
| PLockUniv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PLt | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PLt64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| plugHole | Agda.Utils.Zipper |
| Plus | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Utils |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| plus | Agda.TypeChecking.SizedTypes.Utils |
| plusKView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PlusLevel | Agda.Syntax.Internal |
| PlusLevel' | Agda.Syntax.Internal |
| PM | |
| 1 (Type/Class) | Agda.Syntax.Parser |
| 2 (Data Constructor) | Agda.Syntax.Parser |
| PMul | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PMul64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Pn | Agda.Syntax.Position |
| POAny | Agda.Utils.PartialOrd |
| POEQ | Agda.Utils.PartialOrd |
| POGE | Agda.Utils.PartialOrd |
| POGT | Agda.Utils.PartialOrd |
| PointCons | Agda.TypeChecking.Rules.Data |
| Pointwise | |
| 1 (Type/Class) | Agda.Utils.PartialOrd |
| 2 (Data Constructor) | Agda.Utils.PartialOrd |
| pointwise | Agda.Utils.PartialOrd |
| Polarities | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.Syntax.Concrete.Fixity |
| polaritiesFromAssignments | Agda.TypeChecking.SizedTypes.Syntax |
| Polarity | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PolarityAssignment | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| PolarityPragma | Agda.Syntax.Concrete |
| PolarityPragmasButNotPostulates | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| PolarityPragmasButNotPostulates_ | Agda.Interaction.Options.Warnings |
| POLE | Agda.Utils.PartialOrd |
| polFromCmp | Agda.TypeChecking.Conversion |
| polFromOcc | Agda.TypeChecking.Polarity |
| POLT | Agda.Utils.PartialOrd |
| POMonoid | Agda.Utils.POMonoid |
| popBlock | Agda.Syntax.Parser.Monad |
| popCatchallPragma | Agda.Syntax.Concrete.Definitions.Monad |
| popLexState | Agda.Syntax.Parser.Monad |
| popMapS | Agda.Auto.Convert |
| popnCallStack | Agda.Utils.CallStack |
| posCol | Agda.Syntax.Position |
| POSemigroup | Agda.Utils.POMonoid |
| Position | Agda.Syntax.Position |
| Position' | Agda.Syntax.Position |
| PositionInName | Agda.Syntax.Common |
| positionInvariant | Agda.Syntax.Position |
| PositionMap | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| positionMap | Agda.Interaction.Highlighting.Precise |
| PositionWithoutFile | Agda.Syntax.Position |
| Positivity | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| PositivityCheck | Agda.Syntax.Common |
| positivityCheck | Agda.Syntax.Concrete.Definitions.Types |
| positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| positivityCheckPragma | Agda.Syntax.Concrete.Definitions.Monad |
| PositivityProblem | Agda.Interaction.Highlighting.Precise |
| posLine | Agda.Syntax.Position |
| posPos | Agda.Syntax.Position |
| PossiblyUnused | Agda.Compiler.MAlonzo.Misc |
| Post | Agda.Syntax.Concrete.Operators.Parser |
| postAction | Agda.TypeChecking.CheckInternal |
| postCompile | Agda.Compiler.Backend |
| PostfixNotation | Agda.Syntax.Notation |
| PostLeftsK | Agda.Syntax.Concrete.Operators.Parser.Monad |
| postModule | Agda.Compiler.Backend |
| posToInterval | Agda.Syntax.Position |
| posToRange | Agda.Syntax.Position |
| posToRange' | Agda.Syntax.Position |
| PostponedCheckArgs | Agda.Interaction.Base |
| PostponedCheckFunDef | Agda.Interaction.Base |
| PostponedEquation | |
| 1 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch |
| 2 (Data Constructor) | Agda.TypeChecking.Rewriting.NonLinMatch |
| PostponedEquations | Agda.TypeChecking.Rewriting.NonLinMatch |
| PostponedTypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| postponeInstanceConstraints | Agda.TypeChecking.InstanceArguments |
| postponeTypeCheckingProblem | Agda.TypeChecking.MetaVars |
| postponeTypeCheckingProblem_ | Agda.TypeChecking.MetaVars |
| PostScopeState | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| postTraverseAPatternM | Agda.Syntax.Abstract.Pattern |
| postTraverseCPatternM | Agda.Syntax.Concrete.Pattern |
| postTraversePatternM | Agda.Syntax.Internal.Pattern |
| Postulate | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| PostulateBlock | Agda.Syntax.Concrete.Definitions.Types |
| PPi | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| pPi' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| PProp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PQuot | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PQuot64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Pragma | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 4 (Type/Class) | Agda.Syntax.Abstract |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| PragmaCompiled | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| PragmaCompiled_ | Agda.Interaction.Options.Warnings |
| PragmaCompileErased | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PragmaCompileErased_ | Agda.Interaction.Options.Warnings |
| PragmaNoTerminationCheck | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| PragmaNoTerminationCheck_ | Agda.Interaction.Options.Warnings |
| PragmaOptions | |
| 1 (Type/Class) | Agda.Interaction.Options |
| 2 (Data Constructor) | Agda.Interaction.Options |
| pragmaOptions | Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Pragmas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Pre | Agda.Syntax.Concrete.Operators.Parser |
| preAction | Agda.TypeChecking.CheckInternal |
| Precedence | Agda.Syntax.Fixity |
| PrecedenceKey | Agda.Syntax.Concrete.Operators.Parser.Monad |
| PrecedenceLevel | Agda.Syntax.Common |
| PrecedenceStack | Agda.Syntax.Fixity |
| preCompile | Agda.Compiler.Backend |
| precomputedFreeVars | Agda.TypeChecking.Free.Precompute |
| PrecomputeFreeVars | Agda.TypeChecking.Free.Precompute |
| precomputeFreeVars | Agda.TypeChecking.Free.Precompute |
| precomputeFreeVars_ | Agda.TypeChecking.Free.Precompute |
| pRecord | Agda.Syntax.Concrete.Pretty |
| pRecordDirective | Agda.Syntax.Concrete.Pretty |
| Pred | Agda.TypeChecking.Primitive |
| PreferParen | Agda.Syntax.Fixity |
| preferParen | Agda.Syntax.Fixity |
| PreferParenless | Agda.Syntax.Fixity |
| preferParenless | Agda.Syntax.Fixity |
| Prefix | Agda.Utils.List |
| prefix | Agda.Compiler.JS.Compiler |
| PrefixDef | Agda.Syntax.Common |
| prefixedThings | Agda.Utils.Pretty |
| PrefixNotation | Agda.Syntax.Notation |
| PRem | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PRem64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| preModule | Agda.Compiler.Backend |
| PreOp | Agda.Compiler.JS.Syntax |
| prependList | Agda.Utils.List1 |
| prependS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| preprocess | Agda.TypeChecking.Positivity |
| PreRightsK | Agda.Syntax.Concrete.Operators.Parser.Monad |
| PreScopeState | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| preserveInteractionIds | Agda.Syntax.Translation.AbstractToConcrete |
| preTraverseAPatternM | Agda.Syntax.Abstract.Pattern |
| preTraverseCPatternM | Agda.Syntax.Concrete.Pattern |
| preTraversePatternM | Agda.Syntax.Internal.Pattern |
| 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 |
| prettyAssign | Agda.Utils.Pretty |
| prettyATop | Agda.Syntax.Abstract.Pretty |
| prettyCallSite | Agda.Utils.CallStack |
| prettyCallStack | Agda.Utils.CallStack |
| prettyCohesion | Agda.Syntax.Concrete.Pretty |
| prettyConstraint | Agda.TypeChecking.Pretty.Constraint |
| prettyConstraints | Agda.Interaction.BasicOps |
| PrettyContext | |
| 1 (Type/Class) | Agda.TypeChecking.Pretty |
| 2 (Data Constructor) | Agda.TypeChecking.Pretty |
| prettyDuplicateFields | Agda.TypeChecking.Pretty.Warning |
| prettyErased | Agda.Syntax.Concrete.Pretty |
| prettyError | Agda.TypeChecking.Errors |
| prettyErrorParts | Agda.TypeChecking.Unquote |
| prettyGuardedRhs | Agda.Compiler.MAlonzo.Pretty |
| prettyHiding | Agda.Syntax.Concrete.Pretty |
| prettyInterestingConstraints | Agda.TypeChecking.Pretty.Constraint |
| prettyList | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyList_ | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyMap | Agda.Utils.Pretty |
| prettyMap_ | Agda.TypeChecking.CompiledClause |
| prettyNameSpace | Agda.Syntax.Scope.Base |
| prettyNotInScopeNames | Agda.TypeChecking.Pretty.Warning |
| prettyOpApp | Agda.Syntax.Concrete.Pretty |
| prettyPrec | Agda.Utils.Pretty |
| prettyPrecLevelSucs | Agda.Syntax.Internal |
| prettyPrint | Agda.Compiler.MAlonzo.Pretty |
| prettyQName | Agda.Compiler.MAlonzo.Pretty |
| prettyQuantity | Agda.Syntax.Concrete.Pretty |
| prettyR | Agda.TypeChecking.Pretty |
| prettyRecordFieldWarning | Agda.TypeChecking.Pretty.Warning |
| prettyRelevance | Agda.Syntax.Concrete.Pretty |
| prettyRhs | Agda.Compiler.MAlonzo.Pretty |
| prettySet | Agda.Utils.Pretty |
| prettyShow | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| prettySrcLoc | Agda.Utils.CallStack |
| prettyTactic | Agda.Syntax.Concrete.Pretty |
| prettyTactic' | Agda.Syntax.Concrete.Pretty |
| PrettyTCM | Agda.TypeChecking.Pretty |
| prettyTCM | Agda.TypeChecking.Pretty |
| prettyTCMCtx | Agda.TypeChecking.Pretty |
| prettyTCMPatternList | Agda.TypeChecking.Pretty |
| prettyTCMPatterns | Agda.TypeChecking.Pretty |
| PrettyTCMWithNode | Agda.TypeChecking.Pretty |
| prettyTCMWithNode | Agda.TypeChecking.Pretty |
| prettyTCWarnings | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| prettyTCWarnings' | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| prettyTooManyFields | Agda.TypeChecking.Pretty.Warning |
| prettyTypeOfMeta | Agda.Interaction.EmacsTop |
| prettyWarning | Agda.TypeChecking.Pretty.Warning |
| prettyWarningModeError | Agda.Interaction.Options.Warnings |
| prettyWhere | Agda.Compiler.MAlonzo.Pretty |
| PreviousInput | Agda.Syntax.Parser.Alex |
| Prim | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primAbs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAbsAbs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAbstr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primAgdaClause | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaClauseAbsurd | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaClauseClause | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinition | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionDataConstructor | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionDataDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionFunDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionPostulate | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionPrimitive | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaDefinitionRecordDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaErrorPart | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaErrorPartName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaErrorPartString | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaErrorPartTerm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaLitChar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaLiteral | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaLitFloat | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaLitMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaLitNat | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaLitQName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaLitString | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaLitWord64 | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaPatAbsurd | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaPatCon | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaPatDot | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaPatLit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaPatProj | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaPattern | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaPatVar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaSort | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaSortInf | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaSortLit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaSortProp | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaSortPropLit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaSortSet | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaSortUnsupported | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCM | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMBind | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMBlockOnMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMCatchError | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMCheckType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMCommit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMDebugPrint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMDeclareDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMDeclarePostulate | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMDefineFun | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMDontReduceDefs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMExec | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMExtendContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMFreshName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMGetContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMGetDefinition | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMGetType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMInContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMInferType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMIsMacro | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMNoConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMNormalise | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMOnlyReduceDefs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMQuoteOmegaTerm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMQuoteTerm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMReduce | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMReturn | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMRunSpeculative | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMTypeError | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMUnify | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMUnquoteTerm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMWithNormalisation | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMWithReconsParams | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTerm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermCon | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermExtLam | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermLam | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermLit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermPi | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermSort | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermUnsupported | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAgdaTermVar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primArg | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primArgArg | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primArgArgInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primArgInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAssoc | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAssocLeft | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAssocNon | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primAssocRight | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primBody | Agda.Compiler.MAlonzo.Primitives |
| primBool | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primChar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primCharToNatInjective | Agda.TypeChecking.Primitive |
| primClauses | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primComp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primCompiled | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primConId | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primCons | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primDepIMin' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| Prime | Agda.Utils.Suffix |
| primEquality | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primEqualityName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primEquiv | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primEquivFun | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primEquivProof | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primEraseEquality | Agda.TypeChecking.Primitive |
| primFaceForall | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primFaceForall' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primFalse | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primFixity | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primFixityFixity | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primFlat | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primFloat | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primFloatToWord64Injective | Agda.TypeChecking.Primitive |
| primForce | Agda.TypeChecking.Primitive |
| primForceLemma | Agda.TypeChecking.Primitive |
| primFromNat | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primFromNeg | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primFromString | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| PrimFun | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primFun | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primFunArity | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primFunImplementation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primFunName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primGlue | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primGlue' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primHComp | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primHComp' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primHidden | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primHiding | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIBin | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primId | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIdElim | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIdElim' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primIdFace' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primIdJ | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primIdPath' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primIMax | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIMax' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primIMin | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIMin' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| PrimImpl | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primINeg | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primINeg' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primInf | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primInstance | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primInteger | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIntegerNegSuc | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIntegerPos | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primInterval | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIntervalType | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primInv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primIO | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIOne | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIrrelevant | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIsOne | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIsOne1 | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIsOne2 | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primIsOneEmpty | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primItIsOne | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| Primitive | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 3 (Data Constructor) | Agda.Syntax.Reflected |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| 5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PrimitiveBlock | Agda.Syntax.Concrete.Definitions.Types |
| PrimitiveFunction | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
| primitiveFunctions | Agda.TypeChecking.Primitive |
| PrimitiveImpl | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primitiveModules | Agda.Interaction.Options.Lenses |
| primitives | Agda.Compiler.JS.Compiler |
| PrimitiveSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PrimitiveType | Agda.Interaction.Highlighting.Precise |
| primIZero | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primJust | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primLevel | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primLevelMax | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primLevelSuc | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primLevelZero | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primList | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primLockUniv | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primLockUniv' | Agda.TypeChecking.Primitive |
| primMaybe | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primMetaToNatInjective | Agda.TypeChecking.Primitive |
| primModality | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primModalityConstructor | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| PrimName | Agda.Syntax.Scope.Base |
| primName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primNat | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNatDivSucAux | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNatEquality | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNatLess | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNatMinus | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNatModSucAux | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNatPlus | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNatTimes | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNil | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primNothing | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primPartial | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primPartial' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primPartialP | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primPartialP' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primPath | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primPathP | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primPOr | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primPrecedence | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primPrecRelated | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primPrecUnrelated | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primProp | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primQName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primQNameToWord64sInjective | Agda.TypeChecking.Primitive |
| primQuantity | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primQuantity0 | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primQuantityω | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primRefl | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primRelevance | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primRelevant | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primRewrite | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSet | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSetOmega | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSharp | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSigma | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSize | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSizeInf | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSizeLt | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSizeMax | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSizeSuc | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSizeUniv | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| primSSetOmega | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primStrictSet | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primString | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primStringFromListInjective | Agda.TypeChecking.Primitive |
| primStringToListInjective | Agda.TypeChecking.Primitive |
| primSub | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSubIn | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSubOut | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primSubOut' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primSuc | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| PrimTerm | Agda.TypeChecking.Primitive |
| primTerm | Agda.TypeChecking.Primitive |
| primTrans | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primTrans' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primTransHComp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| primTranspProof | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primTrue | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| PrimType | Agda.TypeChecking.Primitive |
| primType | Agda.TypeChecking.Primitive |
| primUnit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primUnitUnit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primVisible | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primWord64 | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| primWord64ToNatInjective | Agda.TypeChecking.Primitive |
| primZero | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| prim_glue | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| prim_glue' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| prim_glueU | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| prim_glueU' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| prim_unglue | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| prim_unglue' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| prim_unglueU | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| prim_unglueU' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| PrincipalArgTypeMetas | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| print | Agda.TypeChecking.Monad.Benchmark |
| printAgdaDir | Agda.Main |
| printErrorInfo | Agda.Interaction.Highlighting.Generate |
| printHighlightingInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace, Agda.Interaction.Highlighting.Generate |
| printLocals | Agda.Syntax.Scope.Monad |
| PrintRange | |
| 1 (Type/Class) | Agda.Syntax.Position |
| 2 (Data Constructor) | Agda.Syntax.Position |
| printScope | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| printStatistics | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics |
| printSyntaxInfo | Agda.Interaction.Highlighting.Generate |
| printUnsolvedInfo | Agda.Interaction.Highlighting.Generate |
| printUsage | Agda.Main |
| printVersion | Agda.Main |
| Prio | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | 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 |
| Problem | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemConstraint | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| problemCont | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemEq | |
| 1 (Type/Class) | Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Data Constructor) | Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem |
| problemEqs | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemId | |
| 1 (Type/Class) | Agda.Syntax.Common, Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Common, Agda.Syntax.Internal |
| problemInPat | Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem |
| problemInPats | Agda.TypeChecking.Rules.LHS.Problem |
| problemInst | Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem |
| problemRestPats | Agda.TypeChecking.Rules.LHS.Problem |
| problemType | |
| 1 (Function) | Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Function) | Agda.TypeChecking.MetaVars |
| Processor | Agda.Syntax.Parser.Literate |
| productOfEdgesInBoundedWalk | Agda.TypeChecking.Positivity.Occurrence |
| Products | Agda.Utils.TypeLevel |
| Proj | |
| 1 (Data Constructor) | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| projArgInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| projCase | Agda.TypeChecking.CompiledClause |
| projDropPars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| projDropParsApply | Agda.TypeChecking.Substitute |
| ProjectConfig | |
| 1 (Type/Class) | Agda.Interaction.Library.Base, Agda.Interaction.Library |
| 2 (Data Constructor) | Agda.Interaction.Library.Base, Agda.Interaction.Library |
| ProjectedVar | |
| 1 (Type/Class) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| 2 (Data Constructor) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| Projection | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| projectionArgs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| ProjectionLikeness | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| ProjectionReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ProjectionView | |
| 1 (Type/Class) | Agda.TypeChecking.ProjectionLike |
| 2 (Data Constructor) | Agda.TypeChecking.ProjectionLike |
| projectRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| projectTyped | Agda.TypeChecking.Records |
| ProjEliminator | Agda.TypeChecking.ProjectionLike |
| projFromType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| projIndex | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ProjLams | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| projLams | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| projOrig | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ProjOrigin | Agda.Syntax.Common |
| ProjP | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| projPatterns | Agda.TypeChecking.CompiledClause |
| ProjPostfix | Agda.Syntax.Common |
| ProjPrefix | Agda.Syntax.Common |
| projProper | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ProjSystem | Agda.Syntax.Common |
| ProjT | Agda.TypeChecking.Records |
| projTField | Agda.TypeChecking.Records |
| projTRec | Agda.TypeChecking.Records |
| projUseSizeLt | Agda.Termination.Monad |
| ProjVar | Agda.TypeChecking.MetaVars |
| projView | Agda.TypeChecking.ProjectionLike |
| projViewProj | Agda.TypeChecking.ProjectionLike |
| projViewSelf | Agda.TypeChecking.ProjectionLike |
| projViewSpine | Agda.TypeChecking.ProjectionLike |
| Prop | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| propagatePrio | Agda.Auto.NarrowingSearch |
| properlyMatching | Agda.Syntax.Internal |
| properlyMatching' | Agda.Syntax.Internal |
| properSplit | Agda.TypeChecking.CompiledClause.Compile |
| PropLitS | Agda.Syntax.Reflected |
| PropMustBeSingleton | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PropS | Agda.Syntax.Reflected |
| prProjs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| 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 |
| PSeq | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| pshow | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| PSizeUniv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PState | Agda.Syntax.Parser.Monad |
| PStr | Agda.Utils.Pretty |
| PSub | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PSub64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| PSyn | |
| 1 (Type/Class) | Agda.Syntax.Internal.Names |
| 2 (Data Constructor) | Agda.Syntax.Internal.Names |
| PTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ptext | Agda.Utils.Pretty |
| Ptr | Agda.Utils.Pointer |
| PTSInstance | Agda.Interaction.Base |
| ptsRule | Agda.TypeChecking.Sort |
| ptsRule' | Agda.TypeChecking.Sort |
| PType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| PublicAccess | Agda.Syntax.Common |
| publicModules | Agda.Syntax.Scope.Base |
| publicNames | Agda.Syntax.Scope.Base |
| PublicNS | Agda.Syntax.Scope.Base |
| publicOpen | Agda.Syntax.Common |
| punctuate | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| 3 (Function) | Agda.TypeChecking.Pretty |
| pureCompareAs | Agda.TypeChecking.Conversion.Pure |
| PureConversionT | |
| 1 (Type/Class) | Agda.TypeChecking.Conversion.Pure |
| 2 (Data Constructor) | Agda.TypeChecking.Conversion.Pure |
| pureEqualTerm | Agda.TypeChecking.Conversion.Pure |
| pureEqualType | Agda.TypeChecking.Conversion.Pure |
| PureTCM | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Pure |
| pureTCM | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| purgeNonvariant | Agda.TypeChecking.Polarity |
| pushBlock | Agda.Syntax.Parser.Monad |
| pushLexState | Agda.Syntax.Parser.Monad |
| pushPrecedence | Agda.Syntax.Fixity |
| putAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
| putAllConstraintsToSleep | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| putAllowedReductions | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| putBenchmark | Agda.Utils.Benchmark |
| putConstraintsToSleep | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| putIncludePaths | Agda.Interaction.Options.Lenses |
| putPersistentVerbosity | Agda.Interaction.Options.Lenses |
| putResponse | |
| 1 (Function) | Agda.Interaction.EmacsCommand |
| 2 (Function) | Agda.Interaction.InteractionTop |
| putSafeMode | Agda.Interaction.Options.Lenses |
| putTC | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| putVerbosity | Agda.Interaction.Options.Lenses |
| PVar | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| pvIndex | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| PWildCard | Agda.Utils.Haskell.Syntax |
| pwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |