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

Index - P

P64ToIAgda.Syntax.Treeless, Agda.Compiler.Backend
packUnquoteMAgda.TypeChecking.Unquote
PAddAgda.Syntax.Treeless, Agda.Compiler.Backend
PAdd64Agda.Syntax.Treeless, Agda.Compiler.Backend
pageAgda.Interaction.Highlighting.HTML
PageModeAgda.Utils.Pretty
PAppAgda.Utils.Haskell.Syntax
parallelSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
ParenAgda.Syntax.Concrete
ParenPAgda.Syntax.Concrete
ParenPreferenceAgda.Syntax.Fixity
parens 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
parens'Agda.Interaction.Base
ParenVAgda.Syntax.Concrete.Operators.Parser
ParseAgda.Interaction.Base
parse 
1 (Function)Agda.Utils.Parser.MemoisedCPS
2 (Function)Agda.Syntax.Concrete.Operators.Parser.Monad
3 (Function)Agda.Syntax.Parser.Monad
4 (Function)Agda.Syntax.Concrete.Operators.Parser
5 (Function)Agda.Syntax.Parser
parseAndDoAtToplevelAgda.Interaction.InteractionTop
parseApplicationAgda.Syntax.Concrete.Operators
parseArgsAgda.Auto.Options
parseBackendOptionsAgda.Compiler.Backend
ParseError 
1 (Type/Class)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
2 (Data Constructor)Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
parseErrorAgda.Syntax.Parser.Monad
parseError'Agda.Syntax.Parser.Monad
parseErrorAtAgda.Syntax.Parser.Monad
parseErrorRangeAgda.Syntax.Parser.Monad
parseExpr 
1 (Function)Agda.Interaction.BasicOps
2 (Function)Agda.Interaction.CommandLine
parseExprInAgda.Interaction.BasicOps
ParseFailedAgda.Syntax.Parser.Monad
parseFileAgda.Syntax.Parser
ParseFlags 
1 (Type/Class)Agda.Syntax.Parser.Monad
2 (Data Constructor)Agda.Syntax.Parser.Monad
parseFlagsAgda.Syntax.Parser.Monad
parseFromSrcAgda.Syntax.Parser.Monad
parseHaskellPragmaAgda.Compiler.MAlonzo.Pragmas
parseIdiomBracketsSeqAgda.Syntax.IdiomBrackets
parseInpAgda.Syntax.Parser.Monad
parseKeepCommentsAgda.Syntax.Parser.Monad
parseLastPosAgda.Syntax.Parser.Monad
parseLayoutAgda.Syntax.Parser.Monad
parseLexStateAgda.Syntax.Parser.Monad
parseLHSAgda.Syntax.Concrete.Operators
parseLibFileAgda.Interaction.Library.Parse
parseModuleApplicationAgda.Syntax.Concrete.Operators
parseNameAgda.Interaction.BasicOps
ParseOkAgda.Syntax.Parser.Monad
parsePatternAgda.Syntax.Concrete.Operators
parsePatternSynAgda.Syntax.Concrete.Operators
parsePluginOptionsAgda.Interaction.Options
parsePosAgda.Syntax.Parser.Monad
parsePosString 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.Syntax.Parser
parsePragmaAgda.Compiler.MAlonzo.Pragmas
parsePragmaOptionsAgda.Interaction.Options
parsePrevCharAgda.Syntax.Parser.Monad
parsePrevTokenAgda.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
parserBasedAgda.Interaction.Highlighting.Precise
ParserClassAgda.Utils.Parser.MemoisedCPS
ParseResultAgda.Syntax.Parser.Monad
ParserWithGrammarAgda.Utils.Parser.MemoisedCPS
ParseSections 
1 (Type/Class)Agda.Syntax.Concrete.Operators.Parser
2 (Data Constructor)Agda.Syntax.Concrete.Operators.Parser
parseSrcFileAgda.Syntax.Parser.Monad
ParseStateAgda.Syntax.Parser.Monad
parseTimeAgda.Auto.Options
parseToReadsPrecAgda.Interaction.Base
parseVariablesAgda.Interaction.MakeCase
parseVerboseKeyAgda.TypeChecking.Monad.Debug, 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
parseWarningNameAgda.Syntax.Parser.Monad
ParsingAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
PartialAgda.Interaction.Highlighting.Generate
PartialOrdAgda.Utils.PartialOrd
PartialOrderingAgda.Utils.PartialOrd
partition3Agda.Utils.Three
partitionByKindOfForeignCodeAgda.Compiler.MAlonzo.Pragmas
partitionEithers3Agda.Utils.Three
partitionMAgda.Utils.Monad
partitionMaybeAgda.Utils.List
partPAgda.Syntax.Concrete.Operators.Parser
PAsPatAgda.Utils.Haskell.Syntax
Pat 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Type/Class)Agda.Auto.Syntax
patAsNamesAgda.Syntax.Internal
PatConAppAgda.Auto.Syntax
PatExpAgda.Auto.Syntax
pathAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
PathConsAgda.TypeChecking.Rules.Data
pathLevelAgda.Syntax.Internal
pathLhsAgda.Syntax.Internal
pathNameAgda.Syntax.Internal
pathRhsAgda.Syntax.Internal
pathSortAgda.Syntax.Internal
PathTypeAgda.Syntax.Internal
pathTypeAgda.Syntax.Internal
pathUnviewAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PathViewAgda.Syntax.Internal
pathViewAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pathView'Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pathViewAsPiAgda.TypeChecking.Telescope
pathViewAsPi'Agda.TypeChecking.Telescope
pathViewAsPi'whnfAgda.TypeChecking.Telescope
PatInfoAgda.Syntax.Info
PatNameAgda.Syntax.Translation.ConcreteToAbstract
patNoRangeAgda.Syntax.Info
PatOAbsurdAgda.Syntax.Internal
PatOConAgda.Syntax.Internal
PatODotAgda.Syntax.Internal
PatOLitAgda.Syntax.Internal
PatORecAgda.Syntax.Internal
PatOriginAgda.Syntax.Internal
patOriginAgda.Syntax.Internal
PatOSplitAgda.Syntax.Internal
PatOSystemAgda.Syntax.Internal
PatOVarAgda.Syntax.Internal
PatOWildAgda.Syntax.Internal
PatRangeAgda.Syntax.Info
patsToElimsAgda.TypeChecking.With
PatSynAgda.Utils.Haskell.Syntax
Pattern 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Reflected
4 (Type/Class)Agda.Syntax.Abstract
Pattern' 
1 (Type/Class)Agda.Syntax.Internal
2 (Type/Class)Agda.Syntax.Abstract
patternAppViewAgda.Syntax.Concrete.Pattern
patternBinderAgda.Syntax.Concrete.Operators.Parser
PatternBoundAgda.Syntax.Scope.Base
patternDepthAgda.Termination.Monad
PatternErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternFromAgda.TypeChecking.Rewriting.NonLinPattern
patternFromAgda.TypeChecking.Rewriting.NonLinPattern
PatternInfo 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
patternInfoAgda.Syntax.Internal
patternInTeleNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PatternLikeAgda.Syntax.Internal.Pattern
patternNamesAgda.Syntax.Concrete.Pattern
patternOriginAgda.Syntax.Internal
patternQNamesAgda.Syntax.Concrete.Pattern
PatternsAgda.Syntax.Abstract
PatternShadowsConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
patternsToElimsAgda.Syntax.Internal.Pattern
PatternSubstitutionAgda.Syntax.Internal
PatternSyn 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
PatternSynDefAgda.Syntax.Abstract
PatternSynDefnAgda.Syntax.Abstract
PatternSynDefnsAgda.Syntax.Abstract
PatternSynNameAgda.Syntax.Scope.Base
PatternSynPAgda.Syntax.Abstract
PatternSynResNameAgda.Syntax.Scope.Base
patternToElimAgda.Syntax.Internal.Pattern
patternToExprAgda.Syntax.Abstract
patternToModuleBoundAgda.Syntax.Scope.Base
patternToTermAgda.Syntax.Internal.Pattern
patternVariablesAgda.TypeChecking.Rules.LHS.Problem
PatternVarModalitiesAgda.Syntax.Internal.Pattern
patternVarModalitiesAgda.Syntax.Internal.Pattern
PatternVarsAgda.Syntax.Internal
patternVars 
1 (Function)Agda.Syntax.Internal
2 (Function)Agda.Syntax.Abstract.Pattern
patternViewAgda.Syntax.Concrete.Operators.Parser
patternViolationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
patternViolation'Agda.TypeChecking.MetaVars.Occurs
PatTypeSigAgda.Utils.Haskell.Syntax
PatVarAgda.Auto.Syntax
PatVarNameAgda.Syntax.Internal
patVarNameToStringAgda.Syntax.Internal
PBAgda.Auto.NarrowingSearch
PBangPatAgda.Utils.Haskell.Syntax
PBlockedAgda.Auto.NarrowingSearch
PBoundVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pconNameAgda.Compiler.MAlonzo.Primitives
PConstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pDomAgda.Syntax.Internal
PDoubleBlockedAgda.Auto.NarrowingSearch
PEConAppAgda.Auto.Typecheck
PElimsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PENoAgda.Auto.Typecheck
PEq64Agda.Syntax.Treeless, Agda.Compiler.Backend
PEqCAgda.Syntax.Treeless, Agda.Compiler.Backend
PEqFAgda.Syntax.Treeless, Agda.Compiler.Backend
PEqIAgda.Syntax.Treeless, Agda.Compiler.Backend
PEqQAgda.Syntax.Treeless, Agda.Compiler.Backend
PEqSAgda.Syntax.Treeless, Agda.Compiler.Backend
performedSimplificationAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
performedSimplification'Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
performKillAgda.TypeChecking.MetaVars.Occurs
PermAgda.Utils.Permutation
permPicksAgda.Utils.Permutation
permRangeAgda.Utils.Permutation
PermutationAgda.Utils.Permutation
permuteAgda.Utils.Permutation
permuteTelAgda.TypeChecking.Telescope
PersistentTCStAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PersistentTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PersistentVerbosityAgda.Interaction.Options.Lenses
PEvalAgda.Auto.Typecheck
PGeqAgda.Syntax.Treeless, Agda.Compiler.Backend
PhaseAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Pi 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Reflected
5 (Data Constructor)Agda.Syntax.Abstract
piAbstractAgda.TypeChecking.Abstract
piAbstractTermAgda.TypeChecking.Abstract
piApplyAgda.TypeChecking.Substitute
PiApplyMAgda.TypeChecking.Telescope
piApplyMAgda.TypeChecking.Telescope
piBracketsAgda.Syntax.Fixity
pickidAgda.Auto.Typecheck
pickNameAgda.TypeChecking.Unquote
pickUidAgda.Auto.SearchControl
PIfAgda.Syntax.Treeless, Agda.Compiler.Backend
PiHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PInfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PiNotLamAgda.TypeChecking.Rules.Term
piOrPathAgda.TypeChecking.Telescope
PIrrPatAgda.Utils.Haskell.Syntax
PiSortAgda.Syntax.Internal
piSortAgda.TypeChecking.Substitute
piSort'Agda.TypeChecking.Substitute
PITo64Agda.Syntax.Treeless, Agda.Compiler.Backend
PlaceholderAgda.Syntax.Common
placeholderAgda.Syntax.Concrete.Operators.Parser
PlainJSAgda.Compiler.JS.Syntax
PLamAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PLitAgda.Utils.Haskell.Syntax
PLtAgda.Syntax.Treeless, Agda.Compiler.Backend
PLt64Agda.Syntax.Treeless, Agda.Compiler.Backend
plugHoleAgda.Utils.Zipper
Plus 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Utils
2 (Data Constructor)Agda.Syntax.Internal
plusAgda.TypeChecking.SizedTypes.Utils
plusKViewAgda.Syntax.Treeless, Agda.Compiler.Backend
PlusLevelAgda.Syntax.Internal
PlusLevel'Agda.Syntax.Internal
PM 
1 (Type/Class)Agda.Syntax.Parser
2 (Data Constructor)Agda.Syntax.Parser
PMulAgda.Syntax.Treeless, Agda.Compiler.Backend
PMul64Agda.Syntax.Treeless, Agda.Compiler.Backend
PnAgda.Syntax.Position
POAnyAgda.Utils.PartialOrd
POEQAgda.Utils.PartialOrd
POGEAgda.Utils.PartialOrd
POGTAgda.Utils.PartialOrd
PointConsAgda.TypeChecking.Rules.Data
Pointwise 
1 (Type/Class)Agda.Utils.PartialOrd
2 (Data Constructor)Agda.Utils.PartialOrd
pointwiseAgda.Utils.PartialOrd
Polarities 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.Syntax.Concrete.Fixity
polaritiesAgda.TypeChecking.Polarity
polaritiesFromAssignmentsAgda.TypeChecking.SizedTypes.Syntax
Polarity 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
polarityAgda.TypeChecking.Polarity
PolarityAssignment 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
polarityFromPositivityAgda.TypeChecking.Polarity
PolarityPragmaAgda.Syntax.Concrete
PolarityPragmasButNotPostulatesAgda.Syntax.Concrete.Definitions
PolarityPragmasButNotPostulates_Agda.Interaction.Options.Warnings
POLEAgda.Utils.PartialOrd
polFromCmpAgda.TypeChecking.Conversion
polFromOccAgda.TypeChecking.Polarity
POLTAgda.Utils.PartialOrd
POMonoidAgda.Utils.POMonoid
popContextAgda.Syntax.Parser.Monad
popLexStateAgda.Syntax.Parser.Monad
popMapSAgda.Auto.Convert
posColAgda.Syntax.Position
POSemigroupAgda.Utils.POMonoid
PositionAgda.Syntax.Position
Position'Agda.Syntax.Position
PositionInNameAgda.Syntax.Common
positionInvariantAgda.Syntax.Position
PositionWithoutFileAgda.Syntax.Position
PositivityAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
PositivityCheckAgda.Syntax.Common
positivityCheckEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PositivityProblemAgda.Interaction.Highlighting.Precise
posLineAgda.Syntax.Position
posPosAgda.Syntax.Position
PostAgda.Syntax.Concrete.Operators.Parser
postActionAgda.TypeChecking.CheckInternal
postCompileAgda.Compiler.Backend
PostfixNotationAgda.Syntax.Notation
PostLeftsKAgda.Syntax.Concrete.Operators.Parser.Monad
postModuleAgda.Compiler.Backend
posToIntervalAgda.Syntax.Position
posToRangeAgda.Syntax.Position
posToRange'Agda.Syntax.Position
PostponedCheckArgsAgda.Interaction.Base
PostponedCheckFunDefAgda.Interaction.Base
PostponedEquation 
1 (Type/Class)Agda.TypeChecking.Rewriting.NonLinMatch
2 (Data Constructor)Agda.TypeChecking.Rewriting.NonLinMatch
PostponedEquationsAgda.TypeChecking.Rewriting.NonLinMatch
PostponedTypeCheckingProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
postponeInstanceConstraintsAgda.TypeChecking.InstanceArguments
postponeTypeCheckingProblemAgda.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
postscriptAgda.Compiler.JS.Syntax
postTraverseAPatternMAgda.Syntax.Abstract.Pattern
postTraverseCPatternMAgda.Syntax.Concrete.Pattern
postTraversePatternMAgda.Syntax.Internal.Pattern
Postulate 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Interaction.Highlighting.Precise
PPiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
pPi'Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
PPropAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PQuotAgda.Syntax.Treeless, Agda.Compiler.Backend
PQuot64Agda.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
PragmaCompiledAgda.Syntax.Concrete.Definitions
PragmaCompiled_Agda.Interaction.Options.Warnings
PragmaCompileErasedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmaCompileErased_Agda.Interaction.Options.Warnings
PragmaNoTerminationCheckAgda.Syntax.Concrete.Definitions
PragmaNoTerminationCheck_Agda.Interaction.Options.Warnings
PragmaOptions 
1 (Type/Class)Agda.Interaction.Options
2 (Data Constructor)Agda.Interaction.Options
pragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PragmasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PreAgda.Syntax.Concrete.Operators.Parser
preActionAgda.TypeChecking.CheckInternal
PrecedenceAgda.Syntax.Fixity
PrecedenceKeyAgda.Syntax.Concrete.Operators.Parser.Monad
PrecedenceLevelAgda.Syntax.Common
PrecedenceStackAgda.Syntax.Fixity
preCompileAgda.Compiler.Backend
precomputedFreeVarsAgda.TypeChecking.Free.Precompute
PrecomputeFreeVarsAgda.TypeChecking.Free.Precompute
precomputeFreeVarsAgda.TypeChecking.Free.Precompute
precomputeFreeVars_Agda.TypeChecking.Free.Precompute
pRecordAgda.Syntax.Concrete.Pretty
PredAgda.TypeChecking.Primitive
PreferParenAgda.Syntax.Fixity
preferParenAgda.Syntax.Fixity
PreferParenlessAgda.Syntax.Fixity
preferParenlessAgda.Syntax.Fixity
PrefixAgda.Utils.List
prefixAgda.Compiler.JS.Compiler
PrefixDefAgda.Syntax.Common
prefixedThingsAgda.Utils.Pretty
PrefixNotationAgda.Syntax.Notation
PRemAgda.Syntax.Treeless, Agda.Compiler.Backend
PRem64Agda.Syntax.Treeless, Agda.Compiler.Backend
preModuleAgda.Compiler.Backend
PreOpAgda.Compiler.JS.Syntax
prependSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
preprocessAgda.TypeChecking.Positivity
PreRightsKAgda.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
preserveInteractionIdsAgda.Syntax.Translation.AbstractToConcrete
preTraverseAPatternMAgda.Syntax.Abstract.Pattern
preTraverseCPatternMAgda.Syntax.Concrete.Pattern
preTraversePatternMAgda.Syntax.Internal.Pattern
PrettiesAgda.Compiler.JS.Pretty
prettiesAgda.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
prettyATopAgda.Syntax.Abstract.Pretty
prettyCohesionAgda.Syntax.Concrete.Pretty
prettyConstraintAgda.TypeChecking.Pretty.Warning
prettyConstraintsAgda.Interaction.BasicOps
PrettyContext 
1 (Type/Class)Agda.TypeChecking.Pretty
2 (Data Constructor)Agda.TypeChecking.Pretty
prettyErrorAgda.TypeChecking.Errors
prettyGuardedRhsAgda.Compiler.MAlonzo.Pretty
prettyHidingAgda.Syntax.Concrete.Pretty
prettyInterestingConstraintsAgda.TypeChecking.Pretty.Warning
prettyList 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyList_ 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
prettyMapAgda.TypeChecking.CompiledClause
prettyNameSpaceAgda.Syntax.Scope.Base
prettyOpAppAgda.Syntax.Concrete.Pretty
prettyPrecAgda.Utils.Pretty
prettyPrecLevelSucsAgda.Syntax.Internal
prettyPrintAgda.Compiler.MAlonzo.Pretty
prettyQNameAgda.Compiler.MAlonzo.Pretty
prettyQuantityAgda.Syntax.Concrete.Pretty
prettyRAgda.TypeChecking.Pretty
prettyRelevanceAgda.Syntax.Concrete.Pretty
prettyRhsAgda.Compiler.MAlonzo.Pretty
prettyShowAgda.Utils.Pretty
prettyTacticAgda.Syntax.Concrete.Pretty
prettyTactic'Agda.Syntax.Concrete.Pretty
PrettyTCMAgda.TypeChecking.Pretty
prettyTCMAgda.TypeChecking.Pretty
prettyTCMCtxAgda.TypeChecking.Pretty
prettyTCMPatternListAgda.TypeChecking.Pretty
prettyTCMPatternsAgda.TypeChecking.Pretty
prettyTCWarningsAgda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
prettyTCWarnings'Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
prettyTypeOfMetaAgda.Interaction.EmacsTop
prettyWarningAgda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
prettyWhereAgda.Compiler.MAlonzo.Pretty
PreviousInputAgda.Syntax.Parser.Alex
PrimAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbsAbsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseAbsurdAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaClauseClauseAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionDataConstructorAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionDataDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionFunDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionPostulateAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionPrimitiveAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaDefinitionRecordDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartStringAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaErrorPartTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitCharAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLiteralAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitFloatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitMetaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitNatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitQNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitStringAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaLitWord64Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaMetaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatAbsurdAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatConAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatDotAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatLitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatProjAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatternAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaPatVarAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortLitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortSetAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaSortUnsupportedAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMBindAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMBlockOnMetaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCatchErrorAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCheckTypeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMCommitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDebugPrintAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclareDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDeclarePostulateAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMDefineFunAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMExtendContextAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMFreshNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetContextAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetDefinitionAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMGetTypeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMInContextAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMInferTypeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMIsMacroAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMNoConstraintsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMNormaliseAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMQuoteTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMReduceAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMReturnAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMRunSpeculativeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMTypeErrorAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMUnifyAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMUnquoteTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTCMWithNormalisationAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermConAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermDefAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermExtLamAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermLamAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermLitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermMetaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermPiAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermSortAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermUnsupportedAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAgdaTermVarAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgArgAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgArgInfoAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primArgInfoAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocLeftAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocNonAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primAssocRightAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primBodyAgda.Compiler.MAlonzo.Primitives
primBoolAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCharAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCharToNatInjectiveAgda.TypeChecking.Primitive
primClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primCompAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primConIdAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primConsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primDepIMin'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimeAgda.Utils.Suffix
primEqualityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEqualityNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivFunAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEquivProofAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primEraseEqualityAgda.TypeChecking.Primitive
primFaceForallAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFaceForall'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primFalseAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFixityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFixityFixityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFlatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFloatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFloatToWord64InjectiveAgda.TypeChecking.Primitive
primForceAgda.TypeChecking.Primitive
primForceLemmaAgda.TypeChecking.Primitive
primFromNatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFromNegAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFromStringAgda.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
primFunAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunArityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunImplementationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primFunNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlueAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primGlue'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primHCompAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHComp'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primHiddenAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primHidingAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIBinAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIdAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIdElimAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIdElim'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIdFace'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIdJAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIdPath'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIMaxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMax'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primIMinAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIMin'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
PrimImplAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primINegAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primINeg'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primInfAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInstanceAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerNegSucAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntegerPosAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIntervalAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primInvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIOAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIOneAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIrrelevantAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOneAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne1Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOne2Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primIsOneEmptyAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primItIsOneAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Primitive 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.Syntax.Reflected
4 (Data Constructor)Agda.Syntax.Abstract
5 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimitiveFunctionAgda.Syntax.Concrete.Definitions
primitiveFunctionsAgda.TypeChecking.Primitive
PrimitiveImplAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primitiveModulesAgda.Interaction.Options.Lenses
primitivesAgda.Compiler.JS.Compiler
PrimitiveTypeAgda.Interaction.Highlighting.Precise
primIZeroAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelMaxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelSucAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primLevelZeroAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primListAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primMetaToNatInjectiveAgda.TypeChecking.Primitive
PrimNameAgda.Syntax.Scope.Base
primNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatDivSucAuxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatEqualityAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatLessAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatMinusAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatModSucAuxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatPlusAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNatTimesAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primNilAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartialAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartial'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPartialPAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPartialP'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPathAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPathPAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPOrAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primPrecedenceAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPrecRelatedAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primPrecUnrelatedAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQNameAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primQNameToWord64sInjectiveAgda.TypeChecking.Primitive
primReflAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRelevanceAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRelevantAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primRewriteAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSetOmegaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSharpAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSigmaAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeInfAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeLtAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeMaxAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeSucAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSizeUnivAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStringAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primStringToListInjectiveAgda.TypeChecking.Primitive
primSubAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubInAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubOutAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primSubOut'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primSucAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimTermAgda.TypeChecking.Primitive
primTermAgda.TypeChecking.Primitive
primTransAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrans'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primTransHCompAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
primTranspProofAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primTrueAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PrimTypeAgda.TypeChecking.Primitive
primTypeAgda.TypeChecking.Primitive
primUnitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primUnitUnitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primVisibleAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primWord64Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
primWord64ToNatInjectiveAgda.TypeChecking.Primitive
primZeroAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glueAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glue'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
prim_glueUAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_glueU'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
prim_unglueAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglue'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
prim_unglueUAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
prim_unglueU'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
printAgda.TypeChecking.Monad.Benchmark
printErrorInfoAgda.Interaction.Highlighting.Generate
printHighlightingInfoAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend
printLocalsAgda.Syntax.Scope.Monad
PrintRange 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
printScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
printStatisticsAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
printSyntaxInfoAgda.Interaction.Highlighting.Generate
printUnsolvedInfoAgda.Interaction.Highlighting.Generate
printUsageAgda.Main
printVersionAgda.Main
Prio 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
prioAbsurdLambdaAgda.Auto.SearchControl
prioCompareArgListAgda.Auto.SearchControl
prioCompBetaAgda.Auto.SearchControl
prioCompBetaStructuredAgda.Auto.SearchControl
prioCompChoiceAgda.Auto.SearchControl
prioCompCopyAgda.Auto.SearchControl
prioCompIotaAgda.Auto.SearchControl
prioCompUnifAgda.Auto.SearchControl
prioInferredTypeUnknownAgda.Auto.SearchControl
PrioMeta 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
prioNoAgda.Auto.SearchControl
prioNoIotaAgda.Auto.SearchControl
prioProjIndexAgda.Auto.SearchControl
prioTypecheckAgda.Auto.SearchControl
prioTypecheckArgListAgda.Auto.SearchControl
prioTypeUnknownAgda.Auto.SearchControl
PrivateAgda.Syntax.Concrete
PrivateAccessAgda.Syntax.Common
PrivateNSAgda.Syntax.Scope.Base
Problem 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
ProblemConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
problemContAgda.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
problemEqsAgda.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
problemInPatAgda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
problemInPatsAgda.TypeChecking.Rules.LHS.Problem
problemInstAgda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
problemRestPatsAgda.TypeChecking.Rules.LHS.Problem
problemType 
1 (Function)Agda.Syntax.Abstract, Agda.TypeChecking.Rules.LHS.Problem
2 (Function)Agda.TypeChecking.MetaVars
ProcessorAgda.Syntax.Parser.Literate
productOfEdgesInBoundedWalkAgda.TypeChecking.Positivity.Occurrence
ProductsAgda.Utils.TypeLevel
Proj 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract
projArgInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projCaseAgda.TypeChecking.CompiledClause
projDropParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projDropParsApplyAgda.TypeChecking.Substitute
ProjectedVarAgda.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
projectionArgsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionLikenessAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
ProjectionReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjectionView 
1 (Type/Class)Agda.TypeChecking.ProjectionLike
2 (Data Constructor)Agda.TypeChecking.ProjectionLike
projectRootAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
projectTypedAgda.TypeChecking.Records
projFromTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projIndexAgda.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
projLamsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
projOrigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjOriginAgda.Syntax.Common
ProjP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Reflected
3 (Data Constructor)Agda.Syntax.Abstract
projPatternsAgda.TypeChecking.CompiledClause
ProjPostfixAgda.Syntax.Common
ProjPrefixAgda.Syntax.Common
projProperAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ProjSystemAgda.Syntax.Common
ProjTAgda.TypeChecking.Records
projTFieldAgda.TypeChecking.Records
projTRecAgda.TypeChecking.Records
projUseSizeLtAgda.Termination.Monad
ProjVarExc 
1 (Type/Class)Agda.TypeChecking.MetaVars
2 (Data Constructor)Agda.TypeChecking.MetaVars
projViewAgda.TypeChecking.ProjectionLike
projViewProjAgda.TypeChecking.ProjectionLike
projViewSelfAgda.TypeChecking.ProjectionLike
projViewSpineAgda.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
propagatePrioAgda.Auto.NarrowingSearch
properlyMatchingAgda.Syntax.Internal
properlyMatching'Agda.Syntax.Internal
properSplitAgda.TypeChecking.CompiledClause.Compile
PropMustBeSingletonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PropNAgda.Syntax.Concrete
pruneAgda.TypeChecking.MetaVars.Occurs
PrunedEverythingAgda.TypeChecking.MetaVars.Occurs
PrunedNothingAgda.TypeChecking.MetaVars.Occurs
PrunedSomethingAgda.TypeChecking.MetaVars.Occurs
PruneResultAgda.TypeChecking.MetaVars.Occurs
PSeqAgda.Syntax.Treeless, Agda.Compiler.Backend
pshow 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
PSizeUnivAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PStateAgda.Syntax.Parser.Monad
PStrAgda.Utils.Pretty
PSubAgda.Syntax.Treeless, Agda.Compiler.Backend
PSub64Agda.Syntax.Treeless, Agda.Compiler.Backend
PSyn 
1 (Type/Class)Agda.Syntax.Internal.Names
2 (Data Constructor)Agda.Syntax.Internal.Names
PTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ptextAgda.Utils.Pretty
PtrAgda.Utils.Pointer
PTSInstanceAgda.Interaction.Base
ptsRuleAgda.TypeChecking.Sort
ptsRule'Agda.TypeChecking.Sort
PTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PublicAccessAgda.Syntax.Common
publicModulesAgda.Syntax.Scope.Base
publicNamesAgda.Syntax.Scope.Base
PublicNSAgda.Syntax.Scope.Base
publicOpenAgda.Syntax.Common
punctuate 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
pureCompareAsAgda.TypeChecking.Conversion.Pure
PureConversionT 
1 (Type/Class)Agda.TypeChecking.Conversion.Pure
2 (Data Constructor)Agda.TypeChecking.Conversion.Pure
pureEqualTermAgda.TypeChecking.Conversion.Pure
pureTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
purgeNonvariantAgda.TypeChecking.Polarity
pushContextAgda.Syntax.Parser.Monad
pushCurrentContextAgda.Syntax.Parser.Monad
pushLexStateAgda.Syntax.Parser.Monad
pushPrecedenceAgda.Syntax.Fixity
putAbsoluteIncludePathsAgda.Interaction.Options.Lenses
putAllConstraintsToSleepAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putAllowedReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putBenchmarkAgda.Utils.Benchmark
putConstraintsToSleepAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putIncludePathsAgda.Interaction.Options.Lenses
putPersistentVerbosityAgda.Interaction.Options.Lenses
putResponse 
1 (Function)Agda.Interaction.EmacsCommand
2 (Function)Agda.Interaction.InteractionTop
putSafeModeAgda.Interaction.Options.Lenses
putTCAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
putVerbosityAgda.Interaction.Options.Lenses
PVar 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
PWildCardAgda.Utils.Haskell.Syntax
pwords 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty