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 |
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 |
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 |
parseModuleApplication | Agda.Syntax.Concrete.Operators |
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 |
parsePos | Agda.Syntax.Parser.Monad |
parsePosString | |
1 (Function) | Agda.Syntax.Parser.Monad |
2 (Function) | Agda.Syntax.Parser |
parsePragma | Agda.Compiler.MAlonzo.Pragmas |
parsePragmaOptions | Agda.Interaction.Options |
parsePrevChar | Agda.Syntax.Parser.Monad |
parsePrevToken | Agda.Syntax.Parser.Monad |
Parser | |
1 (Type/Class) | Agda.Utils.Parser.MemoisedCPS |
2 (Type/Class) | Agda.Syntax.Concrete.Operators.Parser.Monad |
3 (Type/Class) | Agda.Syntax.Parser.Monad |
4 (Type/Class) | Agda.Syntax.Parser |
parserBased | Agda.Interaction.Highlighting.Precise |
ParserClass | Agda.Utils.Parser.MemoisedCPS |
ParseResult | Agda.Syntax.Parser.Monad |
ParserWithGrammar | Agda.Utils.Parser.MemoisedCPS |
ParseSections | |
1 (Type/Class) | Agda.Syntax.Concrete.Operators.Parser |
2 (Data Constructor) | Agda.Syntax.Concrete.Operators.Parser |
parseSource | Agda.Interaction.Imports |
parseSrcFile | Agda.Syntax.Parser.Monad |
ParseState | Agda.Syntax.Parser.Monad |
parseTime | Agda.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 | Agda.Utils.List1 |
partition3 | Agda.Utils.Three |
partitionByKindOfForeignCode | Agda.Compiler.MAlonzo.Pragmas |
partitionEithers | Agda.Utils.List1 |
partitionEithers3 | Agda.Utils.Three |
partitionImportedNames | Agda.Syntax.Common |
partitionM | Agda.Utils.Monad |
partitionMaybe | Agda.Utils.List |
partP | Agda.Syntax.Concrete.Operators.Parser |
PAsPat | Agda.Utils.Haskell.Syntax |
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 |
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 |
patmMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
patmRemainder | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
PatName | Agda.Syntax.Translation.ConcreteToAbstract |
patNoRange | Agda.Syntax.Info |
PatOAbsurd | Agda.Syntax.Internal |
PatOCon | Agda.Syntax.Internal |
PatODot | Agda.Syntax.Internal |
PatOLit | Agda.Syntax.Internal |
PatORec | Agda.Syntax.Internal |
PatOrigin | Agda.Syntax.Internal |
patOrigin | Agda.Syntax.Internal |
PatOSplit | Agda.Syntax.Internal |
PatOSystem | Agda.Syntax.Internal |
PatOVar | Agda.Syntax.Internal |
PatOWild | Agda.Syntax.Internal |
PatRange | Agda.Syntax.Info |
patsToElims | Agda.TypeChecking.With |
PatSyn | Agda.Utils.Haskell.Syntax |
Pattern | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Internal |
3 (Type/Class) | Agda.Syntax.Reflected |
4 (Type/Class) | Agda.Syntax.Abstract |
Pattern' | |
1 (Type/Class) | Agda.Syntax.Internal |
2 (Type/Class) | Agda.Syntax.Abstract |
patternAppView | Agda.Syntax.Concrete.Pattern |
patternBinder | Agda.Syntax.Concrete.Operators.Parser |
PatternBound | Agda.Syntax.Scope.Base |
patternDepth | Agda.Termination.Monad |
PatternErr | Agda.TypeChecking.Monad.Base, Agda.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 |
patternInTeleName | 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 |
PatternSynonymArgumentShadowsConstructorOrPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.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.Concrete |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Reflected |
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 |
Plus | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Utils |
2 (Data Constructor) | Agda.Syntax.Internal |
plus | Agda.TypeChecking.SizedTypes.Utils |
plusKView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
PlusLevel | Agda.Syntax.Internal |
PlusLevel' | Agda.Syntax.Internal |
PM | |
1 (Type/Class) | Agda.Syntax.Parser |
2 (Data Constructor) | Agda.Syntax.Parser |
PMul | Agda.Syntax.Treeless, Agda.Compiler.Backend |
PMul64 | Agda.Syntax.Treeless, Agda.Compiler.Backend |
Pn | Agda.Syntax.Position |
POAny | Agda.Utils.PartialOrd |
POEQ | Agda.Utils.PartialOrd |
POGE | Agda.Utils.PartialOrd |
POGT | Agda.Utils.PartialOrd |
PointCons | Agda.TypeChecking.Rules.Data |
Pointwise | |
1 (Type/Class) | Agda.Utils.PartialOrd |
2 (Data Constructor) | Agda.Utils.PartialOrd |
pointwise | Agda.Utils.PartialOrd |
Polarities | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Type/Class) | Agda.Syntax.Concrete.Fixity |
polaritiesFromAssignments | Agda.TypeChecking.SizedTypes.Syntax |
Polarity | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
polarity | Agda.Syntax.Parser.Helpers |
PolarityAssignment | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
PolarityPragma | Agda.Syntax.Concrete |
PolarityPragmasButNotPostulates | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
PolarityPragmasButNotPostulates_ | Agda.Interaction.Options.Warnings |
POLE | Agda.Utils.PartialOrd |
polFromCmp | Agda.TypeChecking.Conversion |
polFromOcc | Agda.TypeChecking.Polarity |
POLT | Agda.Utils.PartialOrd |
POMonoid | Agda.Utils.POMonoid |
popBlock | Agda.Syntax.Parser.Monad |
popCatchallPragma | Agda.Syntax.Concrete.Definitions.Monad |
popLexState | Agda.Syntax.Parser.Monad |
popnCallStack | Agda.Utils.CallStack |
posCol | Agda.Syntax.Position |
POSemigroup | Agda.Utils.POMonoid |
Position | Agda.Syntax.Position |
Position' | Agda.Syntax.Position |
PositionInName | Agda.Syntax.Common |
positionInvariant | Agda.Syntax.Position |
PositionMap | |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
positionMap | Agda.Interaction.Highlighting.Precise |
PositionWithoutFile | Agda.Syntax.Position |
Positivity | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
PositivityCheck | Agda.Syntax.Common |
positivityCheck | Agda.Syntax.Concrete.Definitions.Types |
positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.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 |
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 |
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 |
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 |
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 |
preserveInteractionIds | Agda.Syntax.Translation.AbstractToConcrete |
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 |
prettyCallSite | Agda.Utils.CallStack |
prettyCallStack | Agda.Utils.CallStack |
prettyCohesion | Agda.Syntax.Concrete.Pretty |
prettyConstraint | Agda.TypeChecking.Pretty.Constraint |
prettyConstraints | Agda.Interaction.BasicOps |
PrettyContext | |
1 (Type/Class) | Agda.TypeChecking.Pretty |
2 (Data Constructor) | Agda.TypeChecking.Pretty |
prettyDuplicateFields | Agda.TypeChecking.Pretty.Warning |
prettyErased | Agda.Syntax.Concrete.Pretty |
prettyError | Agda.TypeChecking.Errors |
prettyFiniteness | Agda.Syntax.Concrete.Pretty |
prettyGuardedRhs | Agda.Compiler.MAlonzo.Pretty |
prettyHiding | Agda.Syntax.Concrete.Pretty |
prettyInstalledLibraries | Agda.Interaction.Library.Base |
prettyInterestingConstraints | Agda.TypeChecking.Pretty.Constraint |
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.Concrete.Pretty |
prettyMap | Agda.Syntax.Common.Pretty |
prettyMap_ | Agda.TypeChecking.CompiledClause |
prettyNameSpace | Agda.Syntax.Scope.Base |
prettyNotInScopeNames | Agda.TypeChecking.Pretty.Warning |
prettyOpApp | Agda.Syntax.Concrete.Pretty |
prettyPrec | Agda.Syntax.Common.Pretty |
prettyPrecLevelSucs | Agda.Syntax.Internal |
prettyPrint | Agda.Compiler.MAlonzo.Pretty |
prettyQName | Agda.Compiler.MAlonzo.Pretty |
prettyQuantity | Agda.Syntax.Concrete.Pretty |
prettyR | Agda.TypeChecking.Pretty |
prettyRangeConstraint | Agda.TypeChecking.Pretty.Constraint |
prettyRecordFieldWarning | Agda.TypeChecking.Pretty.Warning |
prettyRelevance | Agda.Syntax.Concrete.Pretty |
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 |
prettyWarningName | Agda.TypeChecking.Pretty.Warning |
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 |
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 |
PrimConId | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
primConId | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
primConId' | Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
primCons | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
PrimDepIMin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
primDepIMin' | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
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 |
primId | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
PrimIdElim | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
primIdElim | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
primIdElim' | Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
PrimIdFace | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
primIdFace' | Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
PrimIdPath | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
primIdPath' | Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
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.Concrete |
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 |
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 |
primitiveModules | Agda.Interaction.Options.Lenses |
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 |
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 |
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 |
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 |
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.Syntax.Internal |
properlyMatching' | Agda.Syntax.Internal |
properSplit | Agda.TypeChecking.CompiledClause.Compile |
PropLitS | Agda.Syntax.Reflected |
PropMustBeSingleton | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
PropS | Agda.Syntax.Reflected |
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 |
Ptr | Agda.Utils.Pointer |
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 |
pureEqualType | 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 |
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 |