Agda-2.8.0: 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
package | Agda.Version
packUnquoteM | Agda.TypeChecking.Unquote
PAdd | Agda.Syntax.Treeless, Agda.Compiler.Backend
PAdd64 | Agda.Syntax.Treeless, Agda.Compiler.Backend
PageMode | Agda.Syntax.Common.Pretty
Pair |
1 (Type/Class) | Agda.Utils.Tuple
2 (Data Constructor) | Agda.Utils.Tuple
3 (Data Constructor) | Agda.Utils.TypeLevel
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.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
3 (Function) | Agda.TypeChecking.Pretty
parens' | Agda.Interaction.Base
parensNonEmpty |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
parentPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
parentProjectionOrigin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Concrete.Operators.Parser
4 (Function) | Agda.Syntax.Parser.Monad
5 (Function) | Agda.Syntax.Parser
parseAndDoAtToplevel | Agda.Interaction.InteractionTop
parseApplication | Agda.Syntax.Concrete.Operators
parseArguments | Agda.Syntax.Concrete.Operators
parseAttributes | Agda.Syntax.Parser.Monad
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
parseIOTCM | Agda.Interaction.Base
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
parseLibName | Agda.Interaction.Library.Base, Agda.Interaction.Library
parseName | Agda.Interaction.BasicOps
ParseOk | Agda.Syntax.Parser.Monad
parseOptions | Agda.Mimer.Options
parsePattern | Agda.Syntax.Concrete.Operators
parsePatternSyn | Agda.Syntax.Concrete.Operators
parsePluginOptions | Agda.Interaction.Options
parsePolarity | Agda.Syntax.Parser.Helpers
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
ParserError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Mimer.Options
parseToReadsPrec | Agda.Interaction.Base
parseVariables | Agda.Interaction.MakeCase
parseVerboseKey | Agda.Interaction.Options
ParseWarning |
1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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 |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Map1
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
partitionWithKey | Agda.Utils.Map1
partP | Agda.Syntax.Concrete.Operators.Parser
PAsPat | Agda.Utils.Haskell.Syntax
passCode | Agda.Compiler.ToTreeless
passName | Agda.Compiler.ToTreeless
passTag | Agda.Compiler.ToTreeless
passVerbosity | Agda.Compiler.ToTreeless
Pat | Agda.Utils.Haskell.Syntax
patAsNames | Agda.Syntax.Internal
path | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
PathAbstractionFailed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PathAbstractionFailed_ | Agda.Interaction.Options.Errors
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
pathTelescope | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
pathTelescope' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PathType | Agda.Syntax.Internal
pathType | Agda.Syntax.Internal
pathUnview | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PathView | Agda.Syntax.Internal
pathView | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pathView' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pathViewAsPi | Agda.TypeChecking.Telescope
pathViewAsPi' | Agda.TypeChecking.Telescope
pathViewAsPi'whnf | Agda.TypeChecking.Telescope
PatInfo | Agda.Syntax.Info
PatLamWithoutClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatLamWithoutClauses_ | Agda.Interaction.Options.Errors
patmMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
patmRemainder | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
PatOSplitArg | 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.Internal
2 (Type/Class) | Agda.Syntax.Reflected
3 (Type/Class) | Agda.Syntax.Concrete
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.TypeChecking.Monad, Agda.Compiler.Backend
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
PatternInPathLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternInPathLambda_ | Agda.Interaction.Options.Errors
PatternInSystem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternInSystem_ | Agda.Interaction.Options.Errors
patternInTeleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternLambdas | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
PatternShadowsConstructor_ | Agda.Interaction.Options.Warnings
patternsToElims | Agda.Syntax.Internal.Pattern
PatternSubstitution | Agda.Syntax.Internal
PatternSyn |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
patternSynArgs | Agda.Syntax.Parser.Helpers
PatternSynDef | Agda.Syntax.Abstract
PatternSynDefn | Agda.Syntax.Abstract
PatternSynDefns | Agda.Syntax.Abstract
PatternSynDefS | Agda.Syntax.Abstract
PatternSynName | Agda.Syntax.Scope.Base
PatternSynonymArgumentShadows | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternSynonymArgumentShadows_ | Agda.Interaction.Options.Errors
PatternSynP | Agda.Syntax.Abstract
PatternSynResName | Agda.Syntax.Scope.Base
patternToElim | Agda.Syntax.Internal.Pattern
PatternToExpr | Agda.Syntax.Abstract.Pattern
patternToExpr | Agda.Syntax.Abstract.Pattern
patternToModuleBound | Agda.Syntax.Scope.Base
patternToNames | Agda.Syntax.Parser.Helpers
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.TypeChecking.Monad, Agda.Compiler.Backend
patternViolation' | Agda.TypeChecking.MetaVars.Occurs
patToExpr | Agda.Syntax.Abstract.Pattern
PattPart | Agda.TypeChecking.Unquote
PatTypeSig | Agda.Utils.Haskell.Syntax
PatVar | Agda.Syntax.Internal.Pattern
PatVarLabel | Agda.Syntax.Internal.Pattern
PatVarName | Agda.Syntax.Internal
patVarNameToString | Agda.Syntax.Internal
PBangPat | Agda.Utils.Haskell.Syntax
PBoundVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
Peano | Agda.Utils.Size
PElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
permutations | Agda.Utils.List1
permutations1 | Agda.Utils.List1
Permute | Agda.Utils.GetOpt
permute | Agda.Utils.Permutation
permuteContext | Agda.TypeChecking.Telescope
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
PGeq | Agda.Syntax.Treeless, Agda.Compiler.Backend
Phase | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
pHasEta0 | Agda.Syntax.Concrete.Pretty
Pi |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Concrete
4 (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
pickName | Agda.TypeChecking.Unquote
PIf | Agda.Syntax.Treeless, Agda.Compiler.Backend
PiHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PiK | Agda.TypeChecking.DiscrimTree.Types
PInf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PiNotLam | Agda.TypeChecking.Rules.Term
PIntervalUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
piOrPath | Agda.TypeChecking.Telescope
Pipeline | Agda.Compiler.ToTreeless
PIrrPat | Agda.Utils.Haskell.Syntax
PiSort | Agda.Syntax.Internal
piSort | Agda.TypeChecking.Substitute
piSort' | Agda.TypeChecking.Substitute
PITo64 | Agda.Syntax.Treeless, Agda.Compiler.Backend
PiView |
1 (Type/Class) | Agda.Syntax.Abstract.Views
2 (Data Constructor) | Agda.Syntax.Abstract.Views
piView | Agda.Syntax.Abstract.Views
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
PlentyInHardCompileTimeMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PlentyInHardCompileTimeMode_ | Agda.Interaction.Options.Warnings
PLevelUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PLit | Agda.Utils.Haskell.Syntax
PLockUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PLt | Agda.Syntax.Treeless, Agda.Compiler.Backend
PLt64 | Agda.Syntax.Treeless, Agda.Compiler.Backend
plugHole | Agda.Utils.Zipper
pluralS |
1 (Function) | Agda.Utils.String
2 (Function) | Agda.Syntax.Common.Pretty
3 (Function) | Agda.TypeChecking.Pretty
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.Syntax.Concrete.Fixity
2 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
polaritiesFromAssignments | Agda.TypeChecking.SizedTypes.Syntax
Polarity |
1 (Type/Class) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
PolarityAssignment |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
PolarityAttribute | Agda.Syntax.Concrete.Attribute
polarityAttributeTable | Agda.Syntax.Concrete.Attribute
PolarityModality |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
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
popnCallStack | Agda.Utils.CallStack
posCol | Agda.Syntax.Position
POSemigroup | Agda.Utils.POMonoid
Position | Agda.Syntax.Position
Position' | Agda.Syntax.Position
positionalModalityComponent | Agda.Syntax.Common
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
Positive | Agda.Syntax.Common
Positivity | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
PositivityCheck | Agda.Syntax.Common
positivityCheck | Agda.Syntax.Concrete.Definitions.Types
positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
positivityCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
PositivityProblem | Agda.Syntax.Common.Aspect, 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.Base, Agda.Compiler.Backend
PostfixNotation | Agda.Syntax.Notation
PostLeftsK | Agda.Syntax.Concrete.Operators.Parser.Monad
postModule | Agda.Compiler.Backend.Base, 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.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
postTraverseAPatternM | Agda.Syntax.Abstract.Pattern
postTraverseCPatternM | Agda.Syntax.Concrete.Pattern
postTraversePatternM | Agda.Syntax.Internal.Pattern
Postulate |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Concrete
PostulateBlock | Agda.Syntax.Concrete.Definitions.Types
PostulatedSizeInModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PostulatedSizeInModule_ | Agda.Interaction.Options.Errors
powerSet | Agda.Utils.Set1
PPi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pPi' | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
PProp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PQuot | Agda.Syntax.Treeless, Agda.Compiler.Backend
PQuot64 | Agda.Syntax.Treeless, Agda.Compiler.Backend
Pragma |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Type/Class) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Concrete
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.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileErased_ | Agda.Interaction.Options.Warnings
PragmaCompileList | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileList_ | Agda.Interaction.Options.Warnings
PragmaCompileMaybe | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileMaybe_ | Agda.Interaction.Options.Warnings
PragmaCompileUnparsable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileUnparsable_ | Agda.Interaction.Options.Warnings
PragmaCompileWrong | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileWrongName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileWrongName_ | Agda.Interaction.Options.Warnings
PragmaCompileWrong_ | Agda.Interaction.Options.Warnings
PragmaExpectsDefinedSymbol | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaExpectsDefinedSymbol_ | Agda.Interaction.Options.Warnings
PragmaExpectsUnambiguousConstructorOrFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaExpectsUnambiguousConstructorOrFunction_ | Agda.Interaction.Options.Warnings
PragmaExpectsUnambiguousProjectionOrFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaExpectsUnambiguousProjectionOrFunction_ | 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.TypeChecking.Monad, Agda.Compiler.Backend
PragmaPolarities | Agda.TypeChecking.Positivity.Occurrence
pragmaQName | Agda.Syntax.Parser.Helpers
pragmaRange | Agda.Interaction.Library.Base, Agda.Interaction.Library
PragmaS | Agda.Syntax.Abstract
Pragmas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pragmaStrings | Agda.Interaction.Library.Base, Agda.Interaction.Library
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.Base, 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.Syntax.Common.Pretty
PrefixNotation | Agda.Syntax.Notation
PRem | Agda.Syntax.Treeless, Agda.Compiler.Backend
PRem64 | Agda.Syntax.Treeless, Agda.Compiler.Backend
preModule | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
PreOp | Agda.Compiler.JS.Syntax
prepareCommonAssets | Agda.Interaction.Highlighting.LaTeX.Base
prepareCommonDestinationAssets | Agda.Interaction.Highlighting.HTML.Base
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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
preTraverseAPatternM | Agda.Syntax.Abstract.Pattern
preTraverseCPatternM | Agda.Syntax.Concrete.Pattern
preTraverseDecl | Agda.Syntax.Concrete.Generic
preTraversePatternM | Agda.Syntax.Internal.Pattern
Pretties | Agda.Compiler.JS.Pretty
pretties | Agda.Compiler.JS.Pretty
Pretty |
1 (Type/Class) | Agda.Syntax.Common.Pretty
2 (Type/Class) | Agda.Compiler.JS.Pretty
pretty |
1 (Function) | Agda.Syntax.Common.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.Syntax.Common.Pretty
prettyATop | Agda.Syntax.Abstract.Pretty
prettyAttr | Agda.Syntax.Parser.Helpers
prettyAUnqualify | Agda.Syntax.Abstract.Pretty
prettyCallSite | Agda.Utils.CallStack
prettyCallStack | Agda.Utils.CallStack
prettyCohesion | Agda.Syntax.Common
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.Common
prettyError | Agda.TypeChecking.Errors
prettyFiniteness | Agda.Syntax.Concrete.Pretty
prettyGuardedRhs | Agda.Compiler.MAlonzo.Pretty
prettyHiding | Agda.Syntax.Common
prettyInstalledLibraries | Agda.Interaction.Library.Base
prettyInterestingConstraints | Agda.TypeChecking.Pretty.Constraint
prettyLineColumn | Agda.Syntax.Common.Pretty
prettyList |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
prettyList_ |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
prettyLock | Agda.Syntax.Common
prettyMap | Agda.Syntax.Common.Pretty
prettyMap_ | Agda.TypeChecking.CompiledClause
prettyNameSpace | Agda.Syntax.Scope.Base
prettyOpApp | Agda.Syntax.Concrete.Pretty
prettyPolarity | Agda.Syntax.Common
prettyPrec |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
prettyPrecLevelSucs | Agda.Syntax.Internal
prettyPrint | Agda.Compiler.MAlonzo.Pretty
prettyQName | Agda.Compiler.MAlonzo.Pretty
prettyQuantity | Agda.Syntax.Common
prettyR | Agda.TypeChecking.Pretty
prettyRangeConstraint | Agda.TypeChecking.Pretty.Constraint
prettyRelevance | Agda.Syntax.Common
prettyResponseContext | Agda.Interaction.EmacsTop
prettyRhs | Agda.Compiler.MAlonzo.Pretty
prettySet | Agda.Syntax.Common.Pretty
prettyShow |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
prettySigCubicalNotErasure | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
primAbs | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbsAbs | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaBlocker | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaBlockerAll | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaBlockerAny | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaBlockerMeta | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClause | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseAbsurd | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseClause | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinition | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionDataConstructor | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionDataDef | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionFunDef | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionPostulate | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionPrimitive | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionRecordDef | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPart | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartName | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartPatt | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartString | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartTerm | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitChar | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLiteral | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitFloat | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitMeta | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitNat | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitQName | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitString | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitWord64 | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaMeta | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatAbsurd | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatCon | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatDot | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatLit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatProj | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPattern | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatVar | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSort | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortInf | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortLit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortProp | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortPropLit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortSet | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortUnsupported | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCM | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAskExpandLast | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAskNormalisation | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAskReconstructed | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAskReduceDefs | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMBind | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMBlock | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCatchError | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCheckFromString | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCheckType | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCommit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDebugPrint | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclareData | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclareDef | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclarePostulate | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDefineData | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDefineFun | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMExec | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMExtendContext | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMFormatErrorParts | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMFreshName | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetContext | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetDefinition | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetInstances | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetType | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMInContext | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMInferType | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMIsMacro | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMNoConstraints | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMNormalise | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMPragmaCompile | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMPragmaForeign | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMQuoteOmegaTerm | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMQuoteTerm | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMReduce | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMReturn | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMRunSpeculative | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMSolveInstances | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMTypeError | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMUnify | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMUnquoteTerm | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithExpandLast | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithNormalisation | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithReconstructed | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithReduceDefs | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWorkOnTypes | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTerm | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermCon | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermDef | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermExtLam | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermLam | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermLit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermMeta | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermPi | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermSort | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermUnsupported | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermVar | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArg | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgArg | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgArgInfo | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgInfo | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssoc | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocLeft | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocNon | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocRight | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primBody | Agda.Compiler.MAlonzo.Primitives
primBool | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primChar | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimCharEquality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimCharToNat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimCharToNatInjective | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCharToNatInjective | Agda.TypeChecking.Primitive
primClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimComp | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primComp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCons | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Prime | Agda.Utils.Suffix
primEquality | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEqualityName | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquiv | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivFun | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivProof | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimErase | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimEraseEquality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEraseEquality | Agda.TypeChecking.Primitive
PrimFaceForall | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFaceForall | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFaceForall' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primFalse | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFixity | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFixityFixity | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFlat | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFloat | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatACos | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatACosh | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatASin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatASinh | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatATan | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatATan2 | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatATanh | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatCeiling | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatCos | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatCosh | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatDecode | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatDiv | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatEncode | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatEquality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatExp | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatFloor | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatInequality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatIsInfinite | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatIsNaN | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatIsNegativeZero | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatIsSafeInteger | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatLess | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatLog | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatMinus | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatNegate | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatPlus | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatPow | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatRound | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatSin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatSinh | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatSqrt | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatTan | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatTanh | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatTimes | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatToRatio | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatToWord64 | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimFloatToWord64Injective | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFloatToWord64Injective | Agda.TypeChecking.Primitive
PrimForce | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primForce | Agda.TypeChecking.Primitive
PrimForceLemma | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primForceLemma | Agda.TypeChecking.Primitive
primFromNat | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFromNeg | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFromString | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
primFunArgOccurrences | 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.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlue | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlue' | Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimHComp | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHComp | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHComp' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primHidden | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHiding | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIMax | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMax | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMax' | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimIMin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMin | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMin' | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimImpl | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimINeg | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primINeg | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primINeg' | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primInf | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInstance | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInteger | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerNegSuc | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerPos | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInterval | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntervalType | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIntervalUniv | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIntToFloat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIO | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIOne | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIrrelevant | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsAlpha | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsAscii | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsDigit | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsHexDigit | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsLatin1 | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsLower | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne1 | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne2 | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOneEmpty | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsPrint | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimIsSpace | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primItIsOne | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Primitive |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Concrete
4 (Data Constructor) | Agda.Syntax.Abstract
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveBlock | Agda.Syntax.Concrete.Definitions.Types
primitiveById | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveData |
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
PrimitiveDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveFunction | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
primitiveFunctions | Agda.TypeChecking.Primitive
PrimitiveId | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveImpl | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveLibDir | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primitiveLibDir | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primitiveModules | Agda.Interaction.Library
PrimitiveName | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveS | Agda.Syntax.Abstract
primitives | Agda.Compiler.JS.Compiler
PrimitiveSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveSortData |
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
PrimitiveSortDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveType | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
primIZero | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primJust | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevel | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimLevelMax | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelMax | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimLevelSuc | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelSuc | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelUniv | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimLevelZero | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelZero | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primList | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimLockUniv | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLockUniv | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLockUniv' | Agda.TypeChecking.Primitive
primMaybe | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimMetaEquality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimMetaLess | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimMetaToNat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimMetaToNatInjective | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primMetaToNatInjective | Agda.TypeChecking.Primitive
primModality | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primModalityConstructor | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimName | Agda.Syntax.Scope.Base
primName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNat | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatDivSucAux | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatDivSucAux | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatEquality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatEquality | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatLess | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatLess | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatMinus | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatMinus | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatModSucAux | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatModSucAux | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatPlus | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatPlus | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatTimes | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatTimes | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatToChar | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimNatToFloat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNil | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNothing | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimPartial | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartial | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartial' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimPartialP | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartialP | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartialP' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPath | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPathP | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimPOr | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPOr | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPrecedence | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPrecRelated | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPrecUnrelated | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primProp | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPropOmega | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQName | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameEquality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameFixity | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameLess | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameToWord64s | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimQNameToWord64sInjective | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQNameToWord64sInjective | Agda.TypeChecking.Primitive
primQuantity | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQuantity0 | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQuantityω | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimRatioToFloat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRefl | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRelevance | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRelevant | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSet | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSetOmega | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSharp | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowChar | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowFloat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowInteger | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowMeta | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowNat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowQName | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimShowString | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSigma | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSize | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeInf | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeLt | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeMax | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeSuc | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeUniv | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSortName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSortSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSSetOmega | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStrictSet | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primString | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringAppend | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringEquality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringFromList | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringFromListInjective | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStringFromListInjective | Agda.TypeChecking.Primitive
PrimStringToList | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimStringToListInjective | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStringToListInjective | Agda.TypeChecking.Primitive
PrimStringUncons | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSub | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubIn | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimSubOut | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubOut | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubOut' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primSuc | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimTerm | Agda.TypeChecking.Primitive
primTerm | Agda.TypeChecking.Primitive
PrimToLower | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimToUpper | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimTrans | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrans | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrans' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primTransHComp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primTranspProof | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrue | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimType | Agda.TypeChecking.Primitive
primType | Agda.TypeChecking.Primitive
primUnit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primUnitUnit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primVisible | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primWord64 | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimWord64FromNat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimWord64ToNat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimWord64ToNatInjective | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primWord64ToNatInjective | Agda.TypeChecking.Primitive
primZero | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Prim_glue | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glue | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glue' | Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Prim_glueU | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glueU | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glueU' | Agda.TypeChecking.Primitive.Cubical.HCompU, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Prim_unglue | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglue | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglue' | Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Prim_unglueU | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglueU | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglueU' | Agda.TypeChecking.Primitive.Cubical.HCompU, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrincipalArgTypeMetas |
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
print | Agda.TypeChecking.Monad.Benchmark
printAgdaAppDir | Agda.Main
printAgdaDataDir | Agda.Main
PrintAgdaNumericVersion | Agda.Interaction.Options
PrintAgdaVersion |
1 (Type/Class) | Agda.Interaction.Options
2 (Data Constructor) | Agda.Interaction.Options
printEmacsModeFile | Agda.Setup.EmacsMode
printErrorInfo | Agda.Interaction.Highlighting.Generate
printHighlightingInfo | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend
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
Private | Agda.Syntax.Concrete
PrivateAccess | Agda.Syntax.Common
privateAccessInserted | Agda.Syntax.Common
PrivateNS | Agda.Syntax.Scope.Base
PrivateRecordField | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrivateRecordField_ | Agda.Interaction.Options.Errors
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.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
ProfileOption | Agda.Utils.ProfileOptions
ProfileOptions | Agda.Utils.ProfileOptions
profileOptionsFromList | Agda.Utils.ProfileOptions
profileOptionsToList | Agda.Utils.ProfileOptions
Proj |
1 (Data Constructor) | Agda.Syntax.Internal.Elim, 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
ProjectConfig |
1 (Type/Class) | Agda.Interaction.Library.Base, Agda.Interaction.Library
2 (Data Constructor) | Agda.Interaction.Library.Base, Agda.Interaction.Library
projectConfigs | Agda.Interaction.Library.Base
ProjectedVar |
1 (Type/Class) | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ProjectionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionIsIrrelevant_ | Agda.Interaction.Options.Errors
ProjectionLikeness | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
ProjectionLikenessMissing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TopLevelModuleName
projectTyped | Agda.TypeChecking.Records
ProjEliminator | Agda.TypeChecking.ProjectionLike
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.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.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
ProjVar | Agda.TypeChecking.MetaVars
projView | Agda.TypeChecking.ProjectionLike
projViewProj | Agda.TypeChecking.ProjectionLike
projViewSelf | Agda.TypeChecking.ProjectionLike
projViewSpine | Agda.TypeChecking.ProjectionLike
Prop | Agda.Syntax.Internal
properlyMatching | Agda.TypeChecking.Patterns.Match
properlyMatching' | Agda.TypeChecking.Patterns.Match
properSplit | Agda.TypeChecking.CompiledClause.Compile
PropLitS | Agda.Syntax.Reflected
PropS | Agda.Syntax.Reflected
propToType | Agda.Syntax.Internal
prProjs | Agda.TypeChecking.Monad.SizedTypes, 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
pruneTemporaryInstances | Agda.TypeChecking.InstanceArguments
PSeq | Agda.Syntax.Treeless, Agda.Compiler.Backend
pshow |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
PSizeUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PSSet | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PState | Agda.Syntax.Parser.Monad
PStr | Agda.Syntax.Common.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.Syntax.Common.Pretty
PTSInstance | Agda.Interaction.Base
PType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PublicAccess | Agda.Syntax.Common
publicModules | Agda.Syntax.Scope.Base
publicNames | Agda.Syntax.Scope.Base
publicNamesOfModules | Agda.Syntax.Scope.Base
PublicNS | Agda.Syntax.Scope.Base
publicOpen | Agda.Syntax.Common
punctuate |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
3 (Function) | Agda.TypeChecking.Pretty
PUniv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
pureEqualTermB | Agda.TypeChecking.Conversion.Pure
pureEqualType | Agda.TypeChecking.Conversion.Pure
pureEqualTypeB | Agda.TypeChecking.Conversion.Pure
PureTCM | Agda.TypeChecking.Monad.Pure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pureTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.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
putDoc | Agda.Syntax.Common.Pretty.ANSI
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
putTCPreservingSession | Agda.TypeChecking.Monad.State, 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
pvIndex | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PWildCard | Agda.Utils.Haskell.Syntax
pwords |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty