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

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

Index - P

P64ToI | Agda.Syntax.Treeless, Agda.Compiler.Backend
packUnquoteM | Agda.TypeChecking.Unquote
PAdd | Agda.Syntax.Treeless, Agda.Compiler.Backend
PAdd64 | 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
ParenPreference | Agda.Syntax.Fixity
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.Concrete.Operators.Parser.Monad
4 (Function) | Agda.Syntax.Parser.Monad
5 (Function) | Agda.Syntax.Concrete.Operators.Parser
6 (Function) | Agda.Syntax.Parser
parse' | Agda.Utils.Parser.ReadP
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 |
1 (Function) | Agda.Interaction.BasicOps
2 (Function) | Agda.Interaction.CommandLine
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
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.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
parseSrcFile | Agda.Syntax.Parser.Monad
ParseState | Agda.Syntax.Parser.Monad
parseTime | Agda.Auto.Options
parseToReadsPrec | Agda.Interaction.InteractionTop
parseVariables | Agda.Interaction.MakeCase
parseVerboseKey | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ParseWarning |
1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
parseWarningName | Agda.Syntax.Parser.Monad
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
partitionEithers3 | Agda.Utils.Three
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
path | Agda.TypeChecking.Primitive
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.TypeChecking.Monad.Builtin
PathView | Agda.Syntax.Internal
pathView | Agda.TypeChecking.Monad.Builtin
pathView' | Agda.TypeChecking.Monad.Builtin
pathViewAsPi | Agda.TypeChecking.Telescope
pathViewAsPi' | Agda.TypeChecking.Telescope
pathViewAsPi'whnf | Agda.TypeChecking.Telescope
PatInfo | Agda.Syntax.Info
patInfo | Agda.Syntax.Info
patLazy | Agda.Syntax.Info
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.Info
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.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
PatternBound | Agda.Syntax.Scope.Base
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.Pattern
patternOrigin | Agda.Syntax.Internal
patternQNames | Agda.Syntax.Concrete.Pattern
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.Base
patternToElim | Agda.Syntax.Internal.Pattern
patternToExpr | Agda.Syntax.Abstract
patternToModuleBound | Agda.Syntax.Scope.Base
patternToTerm | Agda.Syntax.Internal.Pattern
PatternVarModalities | Agda.Syntax.Internal.Pattern
patternVarModalities | 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
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.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
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
PLit | Agda.Utils.Haskell.Syntax
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
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
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
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
popContext | Agda.Syntax.Parser.Monad
popLexState | Agda.Syntax.Parser.Monad
popMapS | Agda.Auto.Convert
posCol | Agda.Syntax.Position
POSemigroup | Agda.Utils.POMonoid
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
PostponedCheckFunDef | 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
postponeInstanceConstraints | Agda.TypeChecking.InstanceArguments
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
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
PPi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pPi' | Agda.TypeChecking.Primitive
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
PragmaCompiled_ | Agda.Interaction.Options.Warnings
PragmaNoTerminationCheck | Agda.Syntax.Concrete.Definitions
PragmaNoTerminationCheck_ | Agda.Interaction.Options.Warnings
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
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
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
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
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
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
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
prettyTCMCtx | 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
primAgdaLitWord64 | 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
primAgdaTCMDeclarePostulate | 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
primAgdaTCMNoConstraints | Agda.TypeChecking.Monad.Builtin
primAgdaTCMNormalise | Agda.TypeChecking.Monad.Builtin
primAgdaTCMQuoteTerm | Agda.TypeChecking.Monad.Builtin
primAgdaTCMReduce | Agda.TypeChecking.Monad.Builtin
primAgdaTCMReturn | Agda.TypeChecking.Monad.Builtin
primAgdaTCMRunSpeculative | 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
primCharToNatInjective | Agda.TypeChecking.Primitive
primClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primComp | Agda.TypeChecking.Primitive
primCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primConId | Agda.TypeChecking.Monad.Builtin
primCons | Agda.TypeChecking.Monad.Builtin
primDepIMin' | Agda.TypeChecking.Primitive
Prime | Agda.Utils.Suffix
primEquality | Agda.TypeChecking.Monad.Builtin
primEqualityName | Agda.TypeChecking.Monad.Builtin
primEquiv | Agda.TypeChecking.Monad.Builtin
primEquivFun | Agda.TypeChecking.Monad.Builtin
primEquivProof | Agda.TypeChecking.Monad.Builtin
primEraseEquality | Agda.TypeChecking.Primitive
primFaceForall | Agda.TypeChecking.Monad.Builtin
primFaceForall' | Agda.TypeChecking.Primitive
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
primFun | 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
primGlue | Agda.TypeChecking.Monad.Builtin
primGlue' | Agda.TypeChecking.Primitive
primHComp | Agda.TypeChecking.Monad.Builtin
primHComp' | Agda.TypeChecking.Primitive
primHidden | Agda.TypeChecking.Monad.Builtin
primHiding | Agda.TypeChecking.Monad.Builtin
primIBin | Agda.TypeChecking.Primitive
primId | Agda.TypeChecking.Monad.Builtin
primIdElim | Agda.TypeChecking.Monad.Builtin
primIdElim' | Agda.TypeChecking.Primitive
primIdFace' | Agda.TypeChecking.Primitive
primIdJ | Agda.TypeChecking.Primitive
primIdPath' | Agda.TypeChecking.Primitive
primIMax | Agda.TypeChecking.Monad.Builtin
primIMax' | Agda.TypeChecking.Primitive
primIMin | Agda.TypeChecking.Monad.Builtin
primIMin' | Agda.TypeChecking.Primitive
PrimImpl | Agda.TypeChecking.Primitive
primINeg | Agda.TypeChecking.Monad.Builtin
primINeg' | 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
primInterval | Agda.TypeChecking.Monad.Builtin
primInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIO | Agda.TypeChecking.Monad.Builtin
primIOne | Agda.TypeChecking.Monad.Builtin
primIrrelevant | Agda.TypeChecking.Monad.Builtin
primIsOne | Agda.TypeChecking.Monad.Builtin
primIsOne1 | Agda.TypeChecking.Monad.Builtin
primIsOne2 | Agda.TypeChecking.Monad.Builtin
primIsOneEmpty | Agda.TypeChecking.Monad.Builtin
primItIsOne | 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
primitiveModules | Agda.Interaction.Options.Lenses
primitives | Agda.Compiler.JS.Compiler
PrimitiveType | Agda.Interaction.Highlighting.Precise
primIZero | Agda.TypeChecking.Monad.Builtin
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
primPartial | Agda.TypeChecking.Monad.Builtin
primPartial' | Agda.TypeChecking.Primitive
primPartialP | Agda.TypeChecking.Monad.Builtin
primPartialP' | Agda.TypeChecking.Primitive
primPath | Agda.TypeChecking.Monad.Builtin
primPathP | Agda.TypeChecking.Monad.Builtin
primPathToEquiv | Agda.TypeChecking.Monad.Builtin
primPOr | Agda.TypeChecking.Primitive
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
primSetOmega | Agda.TypeChecking.Monad.Builtin
primSharp | Agda.TypeChecking.Monad.Builtin
primSigma | 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
primStringToListInjective | Agda.TypeChecking.Primitive
primSub | Agda.TypeChecking.Monad.Builtin
primSubIn | Agda.TypeChecking.Monad.Builtin
primSubOut | Agda.TypeChecking.Monad.Builtin
primSubOut' | Agda.TypeChecking.Primitive
primSuc | Agda.TypeChecking.Monad.Builtin
PrimTerm | Agda.TypeChecking.Primitive
primTerm | Agda.TypeChecking.Primitive
primTrans | Agda.TypeChecking.Monad.Builtin
primTrans' | Agda.TypeChecking.Primitive
primTransHComp | Agda.TypeChecking.Primitive
primTrue | Agda.TypeChecking.Monad.Builtin
PrimType | Agda.TypeChecking.Primitive
primType | Agda.TypeChecking.Primitive
primUnit | Agda.TypeChecking.Monad.Builtin
primUnitUnit | Agda.TypeChecking.Monad.Builtin
primVisible | Agda.TypeChecking.Monad.Builtin
primWord64 | Agda.TypeChecking.Monad.Builtin
primWord64ToNatInjective | Agda.TypeChecking.Primitive
primZero | Agda.TypeChecking.Monad.Builtin
prim_glue | Agda.TypeChecking.Monad.Builtin
prim_glue' | Agda.TypeChecking.Primitive
prim_unglue | Agda.TypeChecking.Monad.Builtin
prim_unglue' | Agda.TypeChecking.Primitive
print | Agda.TypeChecking.Monad.Benchmark
printErrorInfo | Agda.Interaction.Highlighting.Generate
printHighlightingInfo | 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.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
ProblemConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
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
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
PropN | Agda.Syntax.Concrete
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
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.TypeChecking.Monad, Agda.Compiler.Backend
ptext | Agda.Utils.Pretty
Ptr | Agda.Utils.Pointer
PTSInstance | Agda.Interaction.BasicOps
ptsRule | Agda.TypeChecking.Sort
ptsRule' | Agda.TypeChecking.Sort
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
putTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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