page | Agda.Interaction.Highlighting.HTML |
PageMode | Agda.Utils.Pretty |
Pair | |
1 (Type/Class) | Agda.Auto.NarrowingSearch |
2 (Data Constructor) | Agda.Auto.NarrowingSearch |
pairwiseFilter | Agda.Compiler.Epic.Interface |
parallelS | Agda.TypeChecking.Substitute |
Paren | Agda.Syntax.Concrete |
parened | Agda.Compiler.JS.Parser |
ParenP | Agda.Syntax.Concrete |
parens | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
parens' | Agda.Interaction.InteractionTop |
ParenV | Agda.Syntax.Concrete.Operators.Parser |
Parse | Agda.Interaction.InteractionTop |
parse | |
1 (Function) | Agda.Utils.ReadP |
2 (Function) | Agda.Compiler.JS.Parser |
3 (Function) | Agda.Syntax.Parser.Monad |
4 (Function) | Agda.Syntax.Parser |
parse' | Agda.Utils.ReadP |
parseAndDoAtToplevel | Agda.Interaction.InteractionTop |
parseApplication | Agda.Syntax.Concrete.Operators |
ParseError | |
1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
2 (Data Constructor) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
parseError | Agda.Syntax.Parser.Monad |
parseError' | Agda.Syntax.Parser.Monad |
parseErrorAt | Agda.Syntax.Parser.Monad |
parseExpr | |
1 (Function) | Agda.Interaction.BasicOps |
2 (Function) | Agda.Interaction.CommandLine |
parseExprIn | Agda.Interaction.BasicOps |
ParseFailed | Agda.Syntax.Parser.Monad |
parseFile | Agda.Syntax.Parser.Monad |
parseFile' | Agda.Syntax.Parser |
ParseFlags | |
1 (Type/Class) | Agda.Syntax.Parser.Monad |
2 (Data Constructor) | Agda.Syntax.Parser.Monad |
parseFlags | Agda.Syntax.Parser.Monad |
parseInp | Agda.Syntax.Parser.Monad |
parseKeepComments | Agda.Syntax.Parser.Monad |
parseLastPos | Agda.Syntax.Parser.Monad |
parseLayout | Agda.Syntax.Parser.Monad |
parseLexState | Agda.Syntax.Parser.Monad |
parseLHS | Agda.Syntax.Concrete.Operators |
parseLiterate | Agda.Syntax.Parser |
parseModuleApplication | Agda.Syntax.Concrete.Operators |
parseName | Agda.Interaction.BasicOps |
ParseOk | Agda.Syntax.Parser.Monad |
parsePattern | Agda.Syntax.Concrete.Operators |
parsePatternSyn | Agda.Syntax.Concrete.Operators |
parsePluginOptions | Agda.Interaction.Options |
parsePos | Agda.Syntax.Parser.Monad |
parsePosString | |
1 (Function) | Agda.Syntax.Parser.Monad |
2 (Function) | Agda.Syntax.Parser |
parsePragmaOptions | Agda.Interaction.Options |
parsePrevChar | Agda.Syntax.Parser.Monad |
parsePrevToken | Agda.Syntax.Parser.Monad |
Parser | |
1 (Type/Class) | Agda.Compiler.JS.Parser |
2 (Type/Class) | Agda.Syntax.Parser.Monad |
3 (Type/Class) | Agda.Syntax.Parser |
ParseResult | Agda.Syntax.Parser.Monad |
parseStandardOptions | Agda.Interaction.Options |
ParseState | Agda.Syntax.Parser.Monad |
parseToReadsPrec | Agda.Interaction.InteractionTop |
parseVariables | Agda.Interaction.MakeCase |
Parsing | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
Partial | Agda.Interaction.Highlighting.Generate |
PartialOrd | Agda.Utils.PartialOrd |
PartialOrdering | Agda.Utils.PartialOrd |
partitionMaybe | Agda.Utils.List |
partP | Agda.Syntax.Concrete.Operators.Parser |
Pat | Agda.Auto.Syntax |
PatConApp | Agda.Auto.Syntax |
PatExp | Agda.Auto.Syntax |
PatInfo | Agda.Syntax.Info |
patInfo | Agda.Syntax.Info |
PatName | Agda.Syntax.Translation.ConcreteToAbstract |
patNoRange | Agda.Syntax.Info |
patOrigin | Agda.Syntax.Info |
PatRange | Agda.Syntax.Info |
pats | Agda.Compiler.JS.Case |
patsToElims | Agda.TypeChecking.With |
Patt | Agda.Compiler.JS.Case |
Pattern | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Abstract |
3 (Type/Class) | Agda.Syntax.Internal |
pattern | Agda.Compiler.JS.Compiler |
Pattern' | |
1 (Type/Class) | Agda.Syntax.Abstract |
2 (Type/Class) | Agda.Syntax.Internal |
patternDepth | Agda.Termination.Monad |
PatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PatternFrom | Agda.TypeChecking.Rewriting.NonLinMatch |
patternFrom | Agda.TypeChecking.Rewriting.NonLinMatch |
patternNames | Agda.Syntax.Concrete |
patternQNames | Agda.Syntax.Concrete |
Patterns | Agda.Syntax.Abstract |
PatternShadowsConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
patternsToElims | Agda.Syntax.Internal.Pattern |
PatternSyn | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
PatternSynDef | Agda.Syntax.Abstract |
PatternSynDefn | Agda.Syntax.Abstract |
PatternSynDefns | Agda.Syntax.Abstract |
PatternSynName | Agda.Syntax.Scope.Base |
PatternSynP | Agda.Syntax.Abstract |
PatternSynResName | Agda.Syntax.Scope.Monad |
patternToExpr | Agda.Syntax.Abstract |
patternToTerm | Agda.Compiler.Epic.Injection |
patternVars | Agda.Syntax.Internal |
patternViolation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
patternViolation' | Agda.TypeChecking.MetaVars.Occurs |
PatVar | Agda.Auto.Syntax |
PatVarName | Agda.Syntax.Internal |
patVarNameToString | Agda.Syntax.Internal |
PB | Agda.Auto.NarrowingSearch |
PBlocked | Agda.Auto.NarrowingSearch |
PBoundVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
pColors | Agda.Syntax.Concrete.Pretty |
pconName | Agda.Compiler.MAlonzo.Primitives |
PConstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PDoubleBlocked | Agda.Auto.NarrowingSearch |
PEConApp | Agda.Auto.Typecheck |
PElims | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PENo | Agda.Auto.Typecheck |
performedSimplification | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
performedSimplification' | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
performKill | Agda.TypeChecking.MetaVars.Occurs |
Perm | Agda.Utils.Permutation |
permPicks | Agda.Utils.Permutation |
permRange | Agda.Utils.Permutation |
Permutation | Agda.Utils.Permutation |
permute | Agda.Utils.Permutation |
PersistentTCSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PersistentTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PersistentVerbosity | Agda.Interaction.Options.Lenses |
PEval | Agda.Auto.Typecheck |
pfail | Agda.Utils.ReadP |
Phase | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
Pi | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Syntax.Internal |
piAbstractTerm | Agda.TypeChecking.Abstract |
piApply | Agda.TypeChecking.Substitute |
piApply1 | Agda.TypeChecking.Telescope |
piApplyM | Agda.TypeChecking.Telescope |
piApplyM' | Agda.Compiler.Epic.Forcing |
piBrackets | Agda.Syntax.Fixity |
pickid | Agda.Auto.Typecheck |
pickName | Agda.TypeChecking.Unquote |
piFreq | Agda.TypeChecking.Test.Generators |
PiHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PiNotLam | Agda.TypeChecking.Rules.Term |
PiSh | Agda.TypeChecking.Rules.LHS.Unify |
PLam | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
plugHole | Agda.Syntax.Internal.Pattern |
Plus | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Utils |
2 (Data Constructor) | Agda.Syntax.Internal |
plus | Agda.TypeChecking.SizedTypes.Utils |
PlusLevel | Agda.Syntax.Internal |
Pn | Agda.Syntax.Position |
POAny | Agda.Utils.PartialOrd |
POEQ | Agda.Utils.PartialOrd |
POGE | Agda.Utils.PartialOrd |
POGT | Agda.Utils.PartialOrd |
pointerChain | Agda.Syntax.Internal |
Pointwise | |
1 (Type/Class) | Agda.Utils.PartialOrd |
2 (Data Constructor) | Agda.Utils.PartialOrd |
pointwise | Agda.Utils.PartialOrd |
Polarities | Agda.TypeChecking.SizedTypes.Syntax |
polarities | Agda.TypeChecking.Polarity |
polaritiesFromAssignments | Agda.TypeChecking.SizedTypes.Syntax |
Polarity | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
polarity | Agda.TypeChecking.Polarity |
PolarityAssignment | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
POLE | Agda.Utils.PartialOrd |
polFromCmp | Agda.TypeChecking.Conversion |
polFromOcc | Agda.TypeChecking.Polarity |
POLT | Agda.Utils.PartialOrd |
polyQuickCheck | Agda.Utils.QuickCheck |
polyVerboseCheck | Agda.Utils.QuickCheck |
pop | Agda.Compiler.JS.Case |
popContext | Agda.Syntax.Parser.Monad |
popLexState | Agda.Syntax.Parser.Monad |
popMapS | Agda.Auto.Convert |
posCol | Agda.Syntax.Position |
Position | Agda.Syntax.Position |
Position' | Agda.Syntax.Position |
positionInvariant | Agda.Syntax.Position |
Positive | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
positive | Agda.Utils.TestHelpers |
Positivity | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
posLine | Agda.Syntax.Position |
posPos | Agda.Syntax.Position |
Possibly | Agda.TypeChecking.Rules.LHS.Unify |
PostfixNotation | Agda.Syntax.Notation |
postfixP | Agda.Syntax.Concrete.Operators.Parser |
postop | Agda.Syntax.Concrete.Operators.Parser |
posToRange | Agda.Syntax.Position |
PostponedCheckArgs | Agda.Interaction.BasicOps |
PostponedEquation | |
1 (Type/Class) | Agda.TypeChecking.Rewriting.NonLinMatch |
2 (Data Constructor) | Agda.TypeChecking.Rewriting.NonLinMatch |
PostponedEquations | Agda.TypeChecking.Rewriting.NonLinMatch |
PostponedTypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
postponeTypeCheckingProblem | Agda.TypeChecking.MetaVars |
postponeTypeCheckingProblem_ | Agda.TypeChecking.MetaVars |
PostScopeState | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Postulate | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
PPi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Pragma | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Syntax.Abstract |
PragmaNoTerminationCheck | Agda.Syntax.Concrete.Definitions |
PragmaOptions | |
1 (Type/Class) | Agda.Interaction.Options |
2 (Data Constructor) | Agda.Interaction.Options |
pragmaOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
Precedence | Agda.Syntax.Fixity |
Pred | Agda.TypeChecking.Primitive |
Prefix | Agda.Utils.List |
prefix | Agda.Compiler.JS.Compiler |
PrefixDef | Agda.Syntax.Common |
PrefixNotation | Agda.Syntax.Notation |
prefixP | Agda.Syntax.Concrete.Operators.Parser |
PreOp | Agda.Compiler.JS.Syntax |
preop | |
1 (Function) | Agda.Compiler.JS.Parser |
2 (Function) | Agda.Syntax.Concrete.Operators.Parser |
PreOrSuffix | Agda.Utils.List |
preOrSuffix | Agda.Utils.List |
prependS | Agda.TypeChecking.Substitute |
PreScopeState | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Pretties | Agda.Compiler.JS.Pretty |
pretties | Agda.Compiler.JS.Pretty |
Pretty | |
1 (Type/Class) | Agda.Utils.Pretty |
2 (Type/Class) | Agda.Compiler.JS.Pretty |
pretty | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.Compiler.JS.Pretty |
3 (Function) | Agda.TypeChecking.Pretty |
prettyA | |
1 (Function) | Agda.Syntax.Abstract.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
prettyAs | |
1 (Function) | Agda.Syntax.Abstract.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
prettyATop | Agda.Syntax.Abstract.Pretty |
PrettyContext | |
1 (Type/Class) | Agda.TypeChecking.Pretty |
2 (Data Constructor) | Agda.TypeChecking.Pretty |
prettyContext | Agda.Interaction.InteractionTop |
prettyEpic | Agda.Compiler.Epic.Epic |
prettyEpicFun | Agda.Compiler.Epic.Epic |
prettyError | Agda.TypeChecking.Errors |
prettyHiding | Agda.Syntax.Concrete.Pretty |
prettyList | Agda.TypeChecking.Pretty |
prettyList_ | Agda.TypeChecking.Pretty |
prettyMap | Agda.TypeChecking.CompiledClause |
prettyOpApp | Agda.Syntax.Concrete.Pretty |
prettyPrec | Agda.Utils.Pretty |
prettyPrint | Agda.Compiler.MAlonzo.Pretty |
prettyRelevance | Agda.Syntax.Concrete.Pretty |
prettyShow | Agda.Utils.Pretty |
PrettyTCM | Agda.TypeChecking.Pretty |
prettyTCM | Agda.TypeChecking.Pretty |
prettyTypeOfMeta | Agda.Interaction.InteractionTop |
PreviousInput | Agda.Syntax.Parser.Alex |
prFalse | Agda.Compiler.Epic.Primitive |
Prim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primAgdaClause | Agda.TypeChecking.Monad.Builtin |
primAgdaClauseAbsurd | Agda.TypeChecking.Monad.Builtin |
primAgdaClauseClause | Agda.TypeChecking.Monad.Builtin |
primAgdaDataDef | Agda.TypeChecking.Monad.Builtin |
primAgdaDefinition | Agda.TypeChecking.Monad.Builtin |
primAgdaDefinitionDataConstructor | Agda.TypeChecking.Monad.Builtin |
primAgdaDefinitionDataDef | Agda.TypeChecking.Monad.Builtin |
primAgdaDefinitionFunDef | Agda.TypeChecking.Monad.Builtin |
primAgdaDefinitionPostulate | Agda.TypeChecking.Monad.Builtin |
primAgdaDefinitionPrimitive | Agda.TypeChecking.Monad.Builtin |
primAgdaDefinitionRecordDef | Agda.TypeChecking.Monad.Builtin |
primAgdaFunDef | Agda.TypeChecking.Monad.Builtin |
primAgdaFunDefCon | Agda.TypeChecking.Monad.Builtin |
primAgdaLitChar | Agda.TypeChecking.Monad.Builtin |
primAgdaLiteral | Agda.TypeChecking.Monad.Builtin |
primAgdaLitFloat | Agda.TypeChecking.Monad.Builtin |
primAgdaLitNat | Agda.TypeChecking.Monad.Builtin |
primAgdaLitQName | Agda.TypeChecking.Monad.Builtin |
primAgdaLitString | Agda.TypeChecking.Monad.Builtin |
primAgdaPatAbsurd | Agda.TypeChecking.Monad.Builtin |
primAgdaPatCon | Agda.TypeChecking.Monad.Builtin |
primAgdaPatDot | Agda.TypeChecking.Monad.Builtin |
primAgdaPatLit | Agda.TypeChecking.Monad.Builtin |
primAgdaPatProj | Agda.TypeChecking.Monad.Builtin |
primAgdaPattern | Agda.TypeChecking.Monad.Builtin |
primAgdaPatVar | Agda.TypeChecking.Monad.Builtin |
primAgdaRecordDef | Agda.TypeChecking.Monad.Builtin |
primAgdaSort | Agda.TypeChecking.Monad.Builtin |
primAgdaSortLit | Agda.TypeChecking.Monad.Builtin |
primAgdaSortSet | Agda.TypeChecking.Monad.Builtin |
primAgdaSortUnsupported | Agda.TypeChecking.Monad.Builtin |
primAgdaTerm | Agda.TypeChecking.Monad.Builtin |
primAgdaTermCon | Agda.TypeChecking.Monad.Builtin |
primAgdaTermDef | Agda.TypeChecking.Monad.Builtin |
primAgdaTermExtLam | Agda.TypeChecking.Monad.Builtin |
primAgdaTermLam | Agda.TypeChecking.Monad.Builtin |
primAgdaTermLit | Agda.TypeChecking.Monad.Builtin |
primAgdaTermPi | Agda.TypeChecking.Monad.Builtin |
primAgdaTermSort | Agda.TypeChecking.Monad.Builtin |
primAgdaTermUnsupported | Agda.TypeChecking.Monad.Builtin |
primAgdaTermVar | Agda.TypeChecking.Monad.Builtin |
primAgdaType | Agda.TypeChecking.Monad.Builtin |
primAgdaTypeEl | Agda.TypeChecking.Monad.Builtin |
primArg | Agda.TypeChecking.Monad.Builtin |
primArgArg | Agda.TypeChecking.Monad.Builtin |
primArgArgInfo | Agda.TypeChecking.Monad.Builtin |
primArgInfo | Agda.TypeChecking.Monad.Builtin |
primBody | Agda.Compiler.MAlonzo.Primitives |
primBool | Agda.TypeChecking.Monad.Builtin |
primChar | Agda.TypeChecking.Monad.Builtin |
primClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primCons | Agda.TypeChecking.Monad.Builtin |
primDataConstructors | Agda.TypeChecking.Primitive |
Prime | Agda.Utils.Suffix |
primEquality | Agda.TypeChecking.Monad.Builtin |
primEqualityName | Agda.TypeChecking.Monad.Builtin |
primExpr | Agda.Compiler.Epic.Primitive |
primFalse | Agda.TypeChecking.Monad.Builtin |
primFlat | Agda.TypeChecking.Monad.Builtin |
primFloat | Agda.TypeChecking.Monad.Builtin |
PrimFun | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primFun | Agda.Compiler.Epic.Primitive |
primFunArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primFunImplementation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primFunName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primHidden | Agda.TypeChecking.Monad.Builtin |
primHiding | Agda.TypeChecking.Monad.Builtin |
PrimImpl | Agda.TypeChecking.Primitive |
primInf | Agda.TypeChecking.Monad.Builtin |
primInstance | Agda.TypeChecking.Monad.Builtin |
primInteger | Agda.TypeChecking.Monad.Builtin |
primIO | Agda.TypeChecking.Monad.Builtin |
primIrrAxiom | Agda.TypeChecking.Monad.Builtin |
primIrrelevant | Agda.TypeChecking.Monad.Builtin |
Primitive | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PrimitiveFunction | Agda.Syntax.Concrete.Definitions |
primitiveFunctions | Agda.TypeChecking.Primitive |
PrimitiveImpl | Agda.TypeChecking.Primitive |
PrimitiveType | Agda.Interaction.Highlighting.Precise |
primitivise | Agda.Compiler.Epic.Primitive |
primLevel | Agda.TypeChecking.Monad.Builtin |
primLevelMax | Agda.TypeChecking.Monad.Builtin |
primLevelSuc | Agda.TypeChecking.Monad.Builtin |
primLevelZero | Agda.TypeChecking.Monad.Builtin |
primList | Agda.TypeChecking.Monad.Builtin |
primName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
primNat | Agda.TypeChecking.Monad.Builtin |
primNatCaseZD | Agda.Compiler.Epic.Primitive |
primNatCaseZS | Agda.Compiler.Epic.Primitive |
primNatDivSucAux | Agda.TypeChecking.Monad.Builtin |
primNatEquality | Agda.TypeChecking.Monad.Builtin |
primNatLess | Agda.TypeChecking.Monad.Builtin |
primNatMinus | Agda.TypeChecking.Monad.Builtin |
primNatModSucAux | Agda.TypeChecking.Monad.Builtin |
primNatPlus | Agda.TypeChecking.Monad.Builtin |
primNatTimes | Agda.TypeChecking.Monad.Builtin |
primNil | Agda.TypeChecking.Monad.Builtin |
primQName | Agda.TypeChecking.Monad.Builtin |
primQNameDefinition | Agda.TypeChecking.Primitive |
primQNameType | Agda.TypeChecking.Primitive |
primRefl | Agda.TypeChecking.Monad.Builtin |
primRelevance | Agda.TypeChecking.Monad.Builtin |
primRelevant | Agda.TypeChecking.Monad.Builtin |
primRewrite | Agda.TypeChecking.Monad.Builtin |
primSharp | Agda.TypeChecking.Monad.Builtin |
primSize | Agda.TypeChecking.Monad.Builtin |
primSizeInf | Agda.TypeChecking.Monad.Builtin |
primSizeLt | Agda.TypeChecking.Monad.Builtin |
primSizeMax | Agda.TypeChecking.Monad.Builtin |
primSizeSuc | Agda.TypeChecking.Monad.Builtin |
primSizeUniv | Agda.TypeChecking.Monad.Builtin |
primString | Agda.TypeChecking.Monad.Builtin |
primSuc | Agda.TypeChecking.Monad.Builtin |
PrimTag | Agda.Compiler.Epic.Interface |
PrimTerm | Agda.TypeChecking.Primitive |
primTerm | Agda.TypeChecking.Primitive |
PrimTF | Agda.Compiler.Epic.Primitive |
PrimTransform | Agda.Compiler.Epic.Primitive |
primTrue | Agda.TypeChecking.Monad.Builtin |
primTrustMe | Agda.TypeChecking.Primitive |
PrimType | Agda.TypeChecking.Primitive |
primType | Agda.TypeChecking.Primitive |
primVisible | Agda.TypeChecking.Monad.Builtin |
primZero | Agda.TypeChecking.Monad.Builtin |
print | Agda.TypeChecking.Monad.Benchmark |
printErrorInfo | Agda.Interaction.Highlighting.Generate |
printHighlightingInfo | Agda.Interaction.Highlighting.Generate |
PrintRange | |
1 (Type/Class) | Agda.Syntax.Position |
2 (Data Constructor) | Agda.Syntax.Position |
printScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
printStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad |
printTestCase | Agda.Utils.QuickCheck |
printUnsolvedInfo | Agda.Interaction.Highlighting.Generate |
printUsage | Agda.Main |
printVersion | Agda.Main |
Prio | Agda.Auto.NarrowingSearch |
prioAbsurdLambda | Agda.Auto.SearchControl |
prioCompareArgList | Agda.Auto.SearchControl |
prioCompBeta | Agda.Auto.SearchControl |
prioCompBetaStructured | Agda.Auto.SearchControl |
prioCompChoice | Agda.Auto.SearchControl |
prioCompCopy | Agda.Auto.SearchControl |
prioCompIota | Agda.Auto.SearchControl |
prioCompUnif | Agda.Auto.SearchControl |
prioInferredTypeUnknown | Agda.Auto.SearchControl |
PrioMeta | |
1 (Type/Class) | Agda.Auto.NarrowingSearch |
2 (Data Constructor) | Agda.Auto.NarrowingSearch |
prioNo | Agda.Auto.SearchControl |
prioNoIota | Agda.Auto.SearchControl |
prioProjIndex | Agda.Auto.SearchControl |
prioTypecheck | Agda.Auto.SearchControl |
prioTypecheckArgList | Agda.Auto.SearchControl |
prioTypeUnknown | Agda.Auto.SearchControl |
Private | Agda.Syntax.Concrete |
PrivateAccess | Agda.Syntax.Common |
PrivateNS | Agda.Syntax.Scope.Base |
prNatEquality | Agda.Compiler.Epic.Primitive |
Problem | |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
Problem' | Agda.TypeChecking.Rules.LHS.Problem |
ProblemConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
problemFromPats | Agda.TypeChecking.Rules.LHS.ProblemRest |
ProblemId | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
problemInPat | Agda.TypeChecking.Rules.LHS.Problem |
problemOutPat | Agda.TypeChecking.Rules.LHS.Problem |
ProblemPart | Agda.TypeChecking.Rules.LHS.Problem |
ProblemRest | |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
problemRest | Agda.TypeChecking.Rules.LHS.Problem |
problemTel | Agda.TypeChecking.Rules.LHS.Problem |
problemType | Agda.TypeChecking.MetaVars |
Proj | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Syntax.Internal |
projArgInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
projCase | Agda.TypeChecking.CompiledClause |
ProjDBP | Agda.Termination.Monad |
projDropPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ProjectedVar | Agda.TypeChecking.MetaVars |
Projection | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
projectionArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
ProjectionLikeness | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
projectionMismatch | Agda.TypeChecking.Rules.LHS.Unify |
ProjectionReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ProjectionView | |
1 (Type/Class) | Agda.TypeChecking.ProjectionLike |
2 (Data Constructor) | Agda.TypeChecking.ProjectionLike |
ProjectRoot | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
projectRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
projectTyped | Agda.TypeChecking.Records |
projFreq | Agda.TypeChecking.Test.Generators |
projFromType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
projIndex | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ProjMP | Agda.TypeChecking.Coverage.Match |
ProjName | |
1 (Type/Class) | Agda.TypeChecking.Test.Generators |
2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
ProjP | Agda.Syntax.Internal |
projPatterns | Agda.TypeChecking.CompiledClause |
projProper | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
projUseSizeLt | Agda.Termination.Monad |
ProjVarExc | |
1 (Type/Class) | Agda.TypeChecking.MetaVars |
2 (Data Constructor) | Agda.TypeChecking.MetaVars |
projView | Agda.TypeChecking.ProjectionLike |
projViewProj | Agda.TypeChecking.ProjectionLike |
projViewSelf | Agda.TypeChecking.ProjectionLike |
projViewSpine | Agda.TypeChecking.ProjectionLike |
proofIrrelevance | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
Prop | |
1 (Type/Class) | Agda.Auto.NarrowingSearch |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Syntax.Internal |
propagatePrio | Agda.Auto.NarrowingSearch |
propAssociative | Agda.TypeChecking.SizedTypes.Tests |
propBoundedSemiLattice | Agda.TypeChecking.SizedTypes.Tests |
propCommutative | Agda.TypeChecking.SizedTypes.Tests |
propDioid | Agda.TypeChecking.SizedTypes.Tests |
propDioid_Gen | Agda.TypeChecking.SizedTypes.Tests |
propDistL | Agda.TypeChecking.SizedTypes.Tests |
propDistR | Agda.TypeChecking.SizedTypes.Tests |
propDistributive | Agda.TypeChecking.SizedTypes.Tests |
properlyMatching | Agda.Syntax.Internal |
properSplit | Agda.TypeChecking.CompiledClause.Compile |
Property | Agda.Utils.QuickCheck |
property | Agda.Utils.QuickCheck |
property_not_null_singleton | Agda.Utils.Favorites |
property_null_empty | Agda.Utils.Favorites |
property_seqPO | Agda.Utils.PartialOrd |
propFreq | Agda.TypeChecking.Test.Generators |
propIdempotent | Agda.TypeChecking.SizedTypes.Tests |
propMonoid | Agda.TypeChecking.SizedTypes.Tests |
PropMustBeSingleton | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
propSemiLattice | Agda.TypeChecking.SizedTypes.Tests |
propUnit | Agda.TypeChecking.SizedTypes.Tests |
propZero | Agda.TypeChecking.SizedTypes.Tests |
prop_associative_orPO | Agda.Utils.PartialOrd |
prop_associative_seqPO | Agda.Utils.PartialOrd |
prop_BiMap_invariant | Agda.Utils.BiMap |
prop_BoundedSemiLattice_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_commonPrefix | Agda.Utils.List |
prop_commonSuffix | Agda.Utils.List |
prop_commutative_orPO | Agda.Utils.PartialOrd |
prop_commutative_seqPO | Agda.Utils.PartialOrd |
prop_comparable_PartialOrdering | Agda.Utils.PartialOrd |
prop_comparable_related | Agda.Utils.PartialOrd |
prop_compareWithFavorites | Agda.Utils.Favorites |
prop_ComposeComplete | Agda.TypeChecking.SizedTypes.Tests |
prop_ComposeSound | Agda.TypeChecking.SizedTypes.Tests |
prop_count_empty | Agda.Utils.Bag |
prop_count_insert | Agda.Utils.Bag |
prop_count_singleton | Agda.Utils.Bag |
prop_Dioid_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_Dioid_Weight | Agda.TypeChecking.SizedTypes.Tests |
prop_disjoint | Agda.Utils.Warshall |
prop_distinct_fastDistinct | Agda.Utils.List |
prop_DistL_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_distributive_seqPO_orPO | Agda.Utils.PartialOrd |
prop_DistR_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_Dist_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_extractNthElement | Agda.Utils.List |
prop_flattenTelInv | Agda.TypeChecking.Tests |
prop_flattenTelScope | Agda.TypeChecking.Tests |
prop_fromList_after_toList | Agda.Utils.Favorites |
prop_fromList_toList | Agda.Utils.Bag |
prop_fromOrderings_after_toOrderings | Agda.Utils.PartialOrd |
prop_galois | Agda.TypeChecking.Irrelevance |
prop_genericElemIndex | Agda.Utils.List |
prop_groupBy' | Agda.Utils.List |
prop_idempotent_orPO | Agda.Utils.PartialOrd |
prop_idempotent_seqPO | Agda.Utils.PartialOrd |
prop_identity_seqPO | Agda.Utils.PartialOrd |
prop_keys_fromList | Agda.Utils.Bag |
prop_leqPO_sound | Agda.Utils.PartialOrd |
prop_map_compose | Agda.Utils.Bag |
prop_map_id | Agda.Utils.Bag |
prop_MeetComplete | Agda.TypeChecking.SizedTypes.Tests |
prop_MeetSound | Agda.TypeChecking.SizedTypes.Tests |
prop_Monoid_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_nonempty_groups | Agda.Utils.Bag |
prop_Occurrence_distributive | Agda.TypeChecking.Positivity.Occurrence |
prop_Occurrence_oplus_associative | Agda.TypeChecking.Positivity.Occurrence |
prop_Occurrence_oplus_commutative | Agda.TypeChecking.Positivity.Occurrence |
prop_Occurrence_oplus_ozero | Agda.TypeChecking.Positivity.Occurrence |
prop_Occurrence_ostar | Agda.TypeChecking.Positivity.Occurrence |
prop_Occurrence_otimes_associative | Agda.TypeChecking.Positivity.Occurrence |
prop_Occurrence_otimes_oone | Agda.TypeChecking.Positivity.Occurrence |
prop_Occurrence_otimes_ozero | Agda.TypeChecking.Positivity.Occurrence |
prop_oplus_Occurrence_Edge | Agda.TypeChecking.Positivity.Tests |
prop_oppPO | Agda.Utils.PartialOrd |
prop_orPO_sound | Agda.Utils.PartialOrd |
prop_path | Agda.Utils.Warshall |
prop_related_pair | Agda.Utils.PartialOrd |
prop_reorderTelStable | Agda.TypeChecking.Tests |
prop_SemiLattice_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_seqPO | Agda.Utils.PartialOrd |
prop_size_fromList | Agda.Utils.Bag |
prop_size_union | Agda.Utils.Bag |
prop_smaller | Agda.Utils.Warshall |
prop_sorted_toOrderings | Agda.Utils.PartialOrd |
prop_splitTelescopePermScope | Agda.TypeChecking.Tests |
prop_splitTelescopeScope | Agda.TypeChecking.Tests |
prop_stable | Agda.Utils.Warshall |
prop_telToListInv | Agda.TypeChecking.Tests |
prop_toList_fromList | Agda.Utils.Bag |
prop_toOrderings_after_fromOrdering | Agda.Utils.PartialOrd |
prop_toOrderings_after_fromOrderings | Agda.Utils.PartialOrd |
prop_traverse_id | Agda.Utils.Bag |
prop_union_union2 | Agda.Utils.Favorites |
prop_uniqOn | Agda.Utils.List |
prop_Unit_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_updateAt | Agda.Utils.List |
prop_updateHead | Agda.Utils.List |
prop_updateLast | Agda.Utils.List |
prop_wellScopedVars | Agda.TypeChecking.Test.Generators |
prop_Zero_Label | Agda.TypeChecking.SizedTypes.Tests |
prop_zero_orPO | Agda.Utils.PartialOrd |
prop_zero_seqPO | Agda.Utils.PartialOrd |
prop_zipWith' | Agda.Utils.List |
prPred | Agda.Compiler.Epic.Primitive |
prSuc | Agda.Compiler.Epic.Primitive |
prTrue | Agda.Compiler.Epic.Primitive |
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 |
prZero | Agda.Compiler.Epic.Primitive |
PState | Agda.Syntax.Parser.Monad |
PStr | Agda.Utils.Pretty |
PTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ptext | Agda.Utils.Pretty |
Ptr | Agda.Utils.Pointer, Agda.Syntax.Internal |
pts | Agda.TypeChecking.Substitute |
ptsRule | Agda.TypeChecking.Rules.Term |
PublicAccess | Agda.Syntax.Common |
publicModules | Agda.Syntax.Scope.Base |
PublicNS | Agda.Syntax.Scope.Base |
publicOpen | Agda.Syntax.Concrete |
punct | Agda.Compiler.JS.Parser |
punctuate | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
pureTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
purgeNonvariant | Agda.TypeChecking.Polarity |
pushContext | Agda.Syntax.Parser.Monad |
pushCurrentContext | Agda.Syntax.Parser.Monad |
pushLexState | Agda.Syntax.Parser.Monad |
putAllConstraintsToSleep | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
putAllowedReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
putBenchmark | Agda.Utils.Benchmark |
putConArity | Agda.Compiler.Epic.CompileState |
putConstrTag | Agda.Compiler.Epic.CompileState |
putDelayed | Agda.Compiler.Epic.CompileState |
putForcedArgs | Agda.Compiler.Epic.CompileState |
putIncludeDirs | Agda.Interaction.Options.Lenses |
putMain | Agda.Compiler.Epic.CompileState |
putPersistentVerbosity | Agda.Interaction.Options.Lenses |
putResponse | |
1 (Function) | Agda.Interaction.EmacsCommand |
2 (Function) | Agda.Interaction.InteractionTop |
putSafeMode | Agda.Interaction.Options.Lenses |
putVerbosity | Agda.Interaction.Options.Lenses |
PVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
PWild | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
pwords | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |