| packUnquoteM | Agda.TypeChecking.Unquote |
| PAdd | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| page | Agda.Interaction.Highlighting.HTML |
| PageMode | Agda.Utils.Pretty |
| PApp | Agda.Utils.Haskell.Syntax |
| parallelS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| Paren | Agda.Syntax.Concrete |
| 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.Parser.ReadP |
| 2 (Function) | Agda.Utils.Parser.MemoisedCPS |
| 3 (Function) | Agda.Syntax.Parser.Monad |
| 4 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad |
| 5 (Function) | Agda.Syntax.Concrete.Operators.Parser |
| 6 (Function) | Agda.Syntax.Parser |
| parse' | Agda.Utils.Parser.ReadP |
| parseAndDoAtToplevel | Agda.Interaction.InteractionTop |
| 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 |
| parseExpr | |
| 1 (Function) | Agda.Interaction.BasicOps |
| 2 (Function) | Agda.Interaction.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 |
| parseFromSrc | Agda.Syntax.Parser.Monad |
| parseHaskellPragma | Agda.Compiler.MAlonzo.Pragmas |
| parseIdiomBrackets | Agda.Syntax.IdiomBrackets |
| 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 |
| 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.Parser.Monad |
| 3 (Type/Class) | Agda.Syntax.Concrete.Operators.Parser.Monad |
| 4 (Type/Class) | Agda.Syntax.Parser |
| 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 |
| parseSrcFile | Agda.Syntax.Parser.Monad |
| parseStandardOptions | Agda.Interaction.Options |
| parseStandardOptions' | Agda.Interaction.Options |
| ParseState | Agda.Syntax.Parser.Monad |
| parseToReadsPrec | Agda.Interaction.InteractionTop |
| parseVariables | Agda.Interaction.MakeCase |
| ParseWarning | |
| 1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Parsing | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| Partial | Agda.Interaction.Highlighting.Generate |
| PartialOrd | Agda.Utils.PartialOrd |
| PartialOrdering | Agda.Utils.PartialOrd |
| partition3 | Agda.Utils.Three |
| partitionByKindOfForeignCode | Agda.Compiler.MAlonzo.Pragmas |
| 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 |
| PatConApp | Agda.Auto.Syntax |
| PatExp | Agda.Auto.Syntax |
| PatInfo | Agda.Syntax.Info |
| patInfo | Agda.Syntax.Info |
| PatName | Agda.Syntax.Translation.ConcreteToAbstract |
| patNoRange | Agda.Syntax.Info |
| patOrigin | Agda.Syntax.Info |
| PatRange | Agda.Syntax.Info |
| patsToElims | Agda.TypeChecking.With |
| PatSyn | Agda.Utils.Haskell.Syntax |
| Pattern | |
| 1 (Type/Class) | Agda.Syntax.Reflected |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Internal |
| 4 (Type/Class) | Agda.Syntax.Abstract |
| Pattern' | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| patternDepth | Agda.Termination.Monad |
| PatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PatternFrom | Agda.TypeChecking.Rewriting.NonLinMatch |
| patternFrom | Agda.TypeChecking.Rewriting.NonLinMatch |
| PatternLike | Agda.Syntax.Internal.Pattern |
| patternNames | Agda.Syntax.Concrete |
| patternQNames | Agda.Syntax.Concrete |
| Patterns | Agda.Syntax.Abstract |
| PatternShadowsConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.Monad |
| patternToElim | Agda.Syntax.Internal.Pattern |
| patternToExpr | Agda.Syntax.Abstract |
| patternToTerm | Agda.Syntax.Internal.Pattern |
| PatternVars | Agda.Syntax.Internal |
| patternVars | |
| 1 (Function) | Agda.Syntax.Internal |
| 2 (Function) | Agda.Syntax.Abstract.Pattern |
| patternViolation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| patternViolation' | Agda.TypeChecking.MetaVars.Occurs |
| PatTypeSig | Agda.Utils.Haskell.Syntax |
| PatVar | Agda.Auto.Syntax |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| pconName | Agda.Compiler.MAlonzo.Primitives |
| PConstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| pDom | Agda.Syntax.Internal |
| PDoubleBlocked | Agda.Auto.NarrowingSearch |
| PEConApp | Agda.Auto.Typecheck |
| PElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PENo | Agda.Auto.Typecheck |
| 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.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| performedSimplification' | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| PersistentTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PersistentVerbosity | Agda.Interaction.Options.Lenses |
| PEval | Agda.Auto.Typecheck |
| pfail | Agda.Utils.Parser.ReadP |
| PGeq | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Phase | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| Pi | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| piAbstract | Agda.TypeChecking.Abstract |
| piAbstractTerm | Agda.TypeChecking.Abstract |
| piApply | Agda.TypeChecking.Substitute |
| piApply1 | 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.TypeChecking.Monad, Agda.Compiler.Backend |
| PiNotLam | Agda.TypeChecking.Rules.Term |
| PIrrPat | Agda.Utils.Haskell.Syntax |
| Placeholder | Agda.Syntax.Common |
| placeholder | Agda.Syntax.Concrete.Operators.Parser |
| PlainJS | Agda.Compiler.JS.Syntax |
| PLam | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PLit | Agda.Utils.Haskell.Syntax |
| PLt | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| 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 |
| PM | |
| 1 (Type/Class) | Agda.Syntax.Parser |
| 2 (Data Constructor) | Agda.Syntax.Parser |
| PMul | 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 |
| 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, Agda.Compiler.Backend |
| polarity | Agda.TypeChecking.Polarity |
| PolarityAssignment | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| polarityFromPositivity | Agda.TypeChecking.Polarity |
| PolarityPragma | Agda.Syntax.Concrete |
| PolarityPragmasButNotPostulates | Agda.Syntax.Concrete.Definitions |
| POLE | Agda.Utils.PartialOrd |
| polFromCmp | Agda.TypeChecking.Conversion |
| polFromOcc | Agda.TypeChecking.Polarity |
| POLT | Agda.Utils.PartialOrd |
| popContext | Agda.Syntax.Parser.Monad |
| popContextPrecedence | Agda.Syntax.Scope.Monad |
| popLexState | Agda.Syntax.Parser.Monad |
| popMapS | Agda.Auto.Convert |
| posCol | Agda.Syntax.Position |
| Position | Agda.Syntax.Position |
| Position' | Agda.Syntax.Position |
| PositionInName | Agda.Syntax.Common |
| positionInvariant | Agda.Syntax.Position |
| PositionWithoutFile | Agda.Syntax.Position |
| Positivity | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| PositivityCheck | Agda.Syntax.Common |
| positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PositivityProblem | Agda.Interaction.Highlighting.Precise |
| posLine | Agda.Syntax.Position |
| posPos | Agda.Syntax.Position |
| 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.BasicOps |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| postponeTypeCheckingProblem | Agda.TypeChecking.MetaVars |
| postponeTypeCheckingProblem_ | Agda.TypeChecking.MetaVars |
| PostScopeState | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| postscript | Agda.Compiler.JS.Syntax |
| postTraverseAPatternM | Agda.Syntax.Abstract.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 |
| PPi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PQuot | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| 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 |
| PragmaNoTerminationCheck | Agda.Syntax.Concrete.Definitions |
| PragmaOptions | |
| 1 (Type/Class) | Agda.Interaction.Options |
| 2 (Data Constructor) | Agda.Interaction.Options |
| pragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Pragmas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Pre | Agda.Syntax.Concrete.Operators.Parser |
| preAction | Agda.TypeChecking.CheckInternal |
| Precedence | Agda.Syntax.Fixity |
| PrecedenceLevel | Agda.Syntax.Fixity |
| PrecedenceStack | Agda.Syntax.Fixity |
| preCompile | Agda.Compiler.Backend |
| Pred | Agda.TypeChecking.Primitive |
| Prefix | Agda.Utils.List |
| prefix | Agda.Compiler.JS.Compiler |
| PrefixDef | Agda.Syntax.Common |
| PrefixNotation | Agda.Syntax.Notation |
| PRem | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| preModule | Agda.Compiler.Backend |
| PreOp | Agda.Compiler.JS.Syntax |
| PreOrSuffix | Agda.Utils.List |
| preOrSuffix | Agda.Utils.List |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| preTraverseAPatternM | Agda.Syntax.Abstract.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 |
| prettyATop | Agda.Syntax.Abstract.Pretty |
| PrettyContext | |
| 1 (Type/Class) | Agda.TypeChecking.Pretty |
| 2 (Data Constructor) | Agda.TypeChecking.Pretty |
| prettyContext | Agda.Interaction.InteractionTop |
| prettyError | Agda.TypeChecking.Errors |
| prettyGuardedRhs | Agda.Compiler.MAlonzo.Pretty |
| prettyHiding | Agda.Syntax.Concrete.Pretty |
| prettyList | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyList_ | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyMap | Agda.TypeChecking.CompiledClause |
| prettyNameSpace | Agda.Syntax.Scope.Base |
| prettyOpApp | Agda.Syntax.Concrete.Pretty |
| prettyPrec | Agda.Utils.Pretty |
| prettyPrint | Agda.Compiler.MAlonzo.Pretty |
| prettyQName | Agda.Compiler.MAlonzo.Pretty |
| prettyRelevance | Agda.Syntax.Concrete.Pretty |
| prettyRhs | Agda.Compiler.MAlonzo.Pretty |
| prettyShow | Agda.Utils.Pretty |
| PrettyTCM | Agda.TypeChecking.Pretty |
| prettyTCM | Agda.TypeChecking.Pretty |
| prettyTCMPatternList | Agda.TypeChecking.Pretty |
| prettyTCMPatterns | Agda.TypeChecking.Pretty |
| prettyTCWarnings | Agda.TypeChecking.Errors |
| prettyTCWarnings' | Agda.TypeChecking.Errors |
| prettyTypeOfMeta | Agda.Interaction.InteractionTop |
| prettyWarning | Agda.TypeChecking.Errors |
| prettyWhere | Agda.Compiler.MAlonzo.Pretty |
| PreviousInput | Agda.Syntax.Parser.Alex |
| Prim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| primAbs | Agda.TypeChecking.Monad.Builtin |
| primAbsAbs | Agda.TypeChecking.Monad.Builtin |
| primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| primAgdaClause | Agda.TypeChecking.Monad.Builtin |
| primAgdaClauseAbsurd | Agda.TypeChecking.Monad.Builtin |
| primAgdaClauseClause | 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 |
| primAgdaErrorPart | Agda.TypeChecking.Monad.Builtin |
| primAgdaErrorPartName | Agda.TypeChecking.Monad.Builtin |
| primAgdaErrorPartString | Agda.TypeChecking.Monad.Builtin |
| primAgdaErrorPartTerm | Agda.TypeChecking.Monad.Builtin |
| primAgdaLitChar | Agda.TypeChecking.Monad.Builtin |
| primAgdaLiteral | Agda.TypeChecking.Monad.Builtin |
| primAgdaLitFloat | Agda.TypeChecking.Monad.Builtin |
| primAgdaLitMeta | Agda.TypeChecking.Monad.Builtin |
| primAgdaLitNat | Agda.TypeChecking.Monad.Builtin |
| primAgdaLitQName | Agda.TypeChecking.Monad.Builtin |
| primAgdaLitString | Agda.TypeChecking.Monad.Builtin |
| primAgdaMeta | Agda.TypeChecking.Monad.Builtin |
| primAgdaPatAbsurd | Agda.TypeChecking.Monad.Builtin |
| primAgdaPatCon | Agda.TypeChecking.Monad.Builtin |
| primAgdaPatDot | Agda.TypeChecking.Monad.Builtin |
| primAgdaPatLit | Agda.TypeChecking.Monad.Builtin |
| primAgdaPatProj | Agda.TypeChecking.Monad.Builtin |
| primAgdaPattern | Agda.TypeChecking.Monad.Builtin |
| primAgdaPatVar | Agda.TypeChecking.Monad.Builtin |
| primAgdaSort | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortLit | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortSet | Agda.TypeChecking.Monad.Builtin |
| primAgdaSortUnsupported | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCM | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMBind | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMBlockOnMeta | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMCatchError | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMCheckType | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMCommit | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMDebugPrint | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMDeclareDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMDefineFun | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMExtendContext | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMFreshName | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMGetContext | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMGetDefinition | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMGetType | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMInContext | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMInferType | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMIsMacro | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMNormalise | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMQuoteTerm | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMReduce | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMReturn | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMTypeError | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMUnify | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMUnquoteTerm | Agda.TypeChecking.Monad.Builtin |
| primAgdaTCMWithNormalisation | Agda.TypeChecking.Monad.Builtin |
| primAgdaTerm | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermCon | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermExtLam | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermLam | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermLit | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermMeta | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermPi | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermSort | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermUnsupported | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermVar | Agda.TypeChecking.Monad.Builtin |
| primArg | Agda.TypeChecking.Monad.Builtin |
| primArgArg | Agda.TypeChecking.Monad.Builtin |
| primArgArgInfo | Agda.TypeChecking.Monad.Builtin |
| primArgInfo | Agda.TypeChecking.Monad.Builtin |
| primAssoc | Agda.TypeChecking.Monad.Builtin |
| primAssocLeft | Agda.TypeChecking.Monad.Builtin |
| primAssocNon | Agda.TypeChecking.Monad.Builtin |
| primAssocRight | 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, Agda.Compiler.Backend |
| primCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| primCons | Agda.TypeChecking.Monad.Builtin |
| Prime | Agda.Utils.Suffix |
| primEquality | Agda.TypeChecking.Monad.Builtin |
| primEqualityName | Agda.TypeChecking.Monad.Builtin |
| primFalse | Agda.TypeChecking.Monad.Builtin |
| primFixity | Agda.TypeChecking.Monad.Builtin |
| primFixityFixity | Agda.TypeChecking.Monad.Builtin |
| primFlat | Agda.TypeChecking.Monad.Builtin |
| primFloat | Agda.TypeChecking.Monad.Builtin |
| primForce | Agda.TypeChecking.Primitive |
| primForceLemma | Agda.TypeChecking.Primitive |
| primFromNat | Agda.TypeChecking.Monad.Builtin |
| primFromNeg | Agda.TypeChecking.Monad.Builtin |
| primFromString | Agda.TypeChecking.Monad.Builtin |
| PrimFun | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| primFunArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| primFunImplementation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| primFunName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| primIntegerNegSuc | Agda.TypeChecking.Monad.Builtin |
| primIntegerPos | Agda.TypeChecking.Monad.Builtin |
| primIO | Agda.TypeChecking.Monad.Builtin |
| primIrrelevant | Agda.TypeChecking.Monad.Builtin |
| Primitive | |
| 1 (Data Constructor) | Agda.Syntax.Reflected |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| 5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PrimitiveFunction | Agda.Syntax.Concrete.Definitions |
| primitiveFunctions | Agda.TypeChecking.Primitive |
| PrimitiveImpl | Agda.TypeChecking.Primitive |
| primitives | Agda.Compiler.JS.Compiler |
| PrimitiveType | Agda.Interaction.Highlighting.Precise |
| 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, Agda.Compiler.Backend |
| primNat | Agda.TypeChecking.Monad.Builtin |
| 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 |
| primPrecedence | Agda.TypeChecking.Monad.Builtin |
| primPrecRelated | Agda.TypeChecking.Monad.Builtin |
| primPrecUnrelated | Agda.TypeChecking.Monad.Builtin |
| primQName | Agda.TypeChecking.Monad.Builtin |
| primRefl | Agda.TypeChecking.Monad.Builtin |
| primRelevance | Agda.TypeChecking.Monad.Builtin |
| primRelevant | Agda.TypeChecking.Monad.Builtin |
| primRewrite | 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 |
| primSizeUniv | Agda.TypeChecking.Monad.Builtin |
| primString | Agda.TypeChecking.Monad.Builtin |
| primSuc | Agda.TypeChecking.Monad.Builtin |
| PrimTerm | Agda.TypeChecking.Primitive |
| primTerm | Agda.TypeChecking.Primitive |
| primTrue | Agda.TypeChecking.Monad.Builtin |
| primTrustMe | Agda.TypeChecking.Primitive |
| PrimType | Agda.TypeChecking.Primitive |
| primType | Agda.TypeChecking.Primitive |
| primUnit | Agda.TypeChecking.Monad.Builtin |
| primUnitUnit | Agda.TypeChecking.Monad.Builtin |
| primVisible | Agda.TypeChecking.Monad.Builtin |
| primZero | Agda.TypeChecking.Monad.Builtin |
| print | Agda.TypeChecking.Monad.Benchmark |
| printErrorInfo | Agda.Interaction.Highlighting.Generate |
| printHighlightingInfo | Agda.Interaction.Highlighting.Generate |
| PrintRange | |
| 1 (Type/Class) | Agda.Syntax.Position |
| 2 (Data Constructor) | Agda.Syntax.Position |
| printScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| printStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| Problem' | Agda.TypeChecking.Rules.LHS.Problem |
| problemAllVariables | Agda.TypeChecking.Rules.LHS |
| ProblemConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| problemFromPats | Agda.TypeChecking.Rules.LHS.ProblemRest |
| ProblemId | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| Processor | Agda.Syntax.Parser.Literate |
| productOfEdgesInBoundedWalk | Agda.TypeChecking.Positivity.Occurrence |
| Products | Agda.Utils.TypeLevel |
| Proj | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| projArgInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| projCase | Agda.TypeChecking.CompiledClause |
| projDropPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| projDropParsApply | Agda.TypeChecking.Substitute |
| ProjectedVar | Agda.TypeChecking.MetaVars |
| Projection | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| projectionArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ProjectionLikeness | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| ProjectionReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ProjectionView | |
| 1 (Type/Class) | Agda.TypeChecking.ProjectionLike |
| 2 (Data Constructor) | Agda.TypeChecking.ProjectionLike |
| Projectn | Agda.TypeChecking.Rules.LHS |
| Projectns | Agda.TypeChecking.Rules.LHS |
| ProjectRoot | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| projectRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| projectTyped | Agda.TypeChecking.Records |
| projFromType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| projIndex | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ProjLams | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| projLams | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| projOrig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ProjOrigin | Agda.Syntax.Common |
| ProjP | |
| 1 (Data Constructor) | Agda.Syntax.Reflected |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| projPatterns | Agda.TypeChecking.CompiledClause |
| ProjPostfix | Agda.Syntax.Common |
| ProjPrefix | Agda.Syntax.Common |
| projProper | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ProjSystem | Agda.Syntax.Common |
| ProjT | Agda.TypeChecking.Records |
| projTField | Agda.TypeChecking.Records |
| projTRec | Agda.TypeChecking.Records |
| 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, Agda.Compiler.Backend |
| Prop | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| propagatePrio | Agda.Auto.NarrowingSearch |
| properlyMatching | Agda.Syntax.Internal |
| properSplit | Agda.TypeChecking.CompiledClause.Compile |
| PropMustBeSingleton | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| PState | Agda.Syntax.Parser.Monad |
| PStr | Agda.Utils.Pretty |
| PSub | 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.TypeChecking.Monad, Agda.Compiler.Backend |
| ptext | Agda.Utils.Pretty |
| Ptr | Agda.Utils.Pointer, Agda.Syntax.Internal |
| pts | Agda.TypeChecking.Substitute |
| ptsRule | Agda.TypeChecking.Rules.Term |
| 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.TypeChecking.Pretty |
| pureTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| purgeNonvariant | Agda.TypeChecking.Polarity |
| pushContext | Agda.Syntax.Parser.Monad |
| pushContextPrecedence | Agda.Syntax.Scope.Monad |
| pushCurrentContext | Agda.Syntax.Parser.Monad |
| pushLexState | Agda.Syntax.Parser.Monad |
| pushPrecedence | Agda.Syntax.Fixity |
| putAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
| putAllConstraintsToSleep | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| putAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| putBenchmark | Agda.Utils.Benchmark |
| putConstraintsToSleep | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| putVerbosity | Agda.Interaction.Options.Lenses |
| PVar | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PWild | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| PWildCard | Agda.Utils.Haskell.Syntax |
| pwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |