| $$ | Language.PTS.Script, Language.PTS |
| $$$ | Language.PTS.Pretty |
| -:- | Language.PTS.Smart, Language.PTS |
| .= | Language.PTS.Smart, Language.PTS |
| <+> | Language.PTS.Pretty |
| </> | Language.PTS.Pretty |
| >>== | Language.PTS.Bound |
| >>>= | Language.PTS.Bound |
| @@ | Language.PTS.Smart, Language.PTS |
| @@@ | Language.PTS.Smart, Language.PTS |
| abstract | Language.PTS.Bound |
| abstract1HSym | Language.PTS.Bound |
| abstract1Sym | Language.PTS.Bound |
| abstract2HSym | Language.PTS.Bound |
| abstract3HSym | Language.PTS.Bound |
| abstractH | Language.PTS.Bound |
| abstractHEither | Language.PTS.Bound |
| Absurd | Language.PTS.Term, Language.PTS |
| Ann | Language.PTS.Term, Language.PTS |
| annotationError | Language.PTS.Examples.Errors, Language.PTS.Examples |
| ann_ | Language.PTS.Smart, Language.PTS |
| App | Language.PTS.Term, Language.PTS |
| ApplyPanic | Language.PTS.Error, Language.PTS |
| apps_ | Language.PTS.Smart, Language.PTS |
| AsErr | Language.PTS.Error, Language.PTS |
| axiom | Language.PTS.Specification, Language.PTS |
| B | Language.PTS.Bound |
| basicCtx | Language.PTS.Examples.Contexts, Language.PTS.Examples |
| bindings | Language.PTS.Bound |
| bindingsH | Language.PTS.Bound |
| booleansPrimScript | Language.PTS.Examples.Booleans, Language.PTS.Examples |
| booleansScript | Language.PTS.Examples.Booleans, Language.PTS.Examples |
| Bound | Language.PTS.Bound |
| box_ | Language.PTS.Specification, Language.PTS |
| CanApp | Language.PTS.Smart, Language.PTS |
| CanLam | Language.PTS.Smart, Language.PTS |
| CanPi | Language.PTS.Smart, Language.PTS |
| CanSort | Language.PTS.Smart, Language.PTS |
| check_ | Language.PTS.Check, Language.PTS |
| churchBooleansScript | Language.PTS.Examples.Booleans, Language.PTS.Examples |
| CoC | Language.PTS.Systems |
| CoCBox | Language.PTS.Systems |
| CoCStar | Language.PTS.Systems |
| comment_ | Language.PTS.Script, Language.PTS |
| Convert | Language.PTS.Smart, Language.PTS |
| convert | Language.PTS.Smart, Language.PTS |
| defineChk_ | Language.PTS.Script, Language.PTS |
| defineInf_ | Language.PTS.Script, Language.PTS |
| defineU | Language.PTS.Examples.Hurkens, Language.PTS.Examples |
| define_ | Language.PTS.Script, Language.PTS |
| demo_ | Language.PTS |
| Doc | Language.PTS.Pretty |
| dumpDefs_ | Language.PTS.Script, Language.PTS |
| eitherScript | Language.PTS.Examples.Sigma |
| Empty | Language.PTS.Term, Language.PTS |
| emptyCtx | Language.PTS.Examples.Contexts, Language.PTS.Examples |
| Equality | Language.PTS.Term, Language.PTS |
| equalityScript | Language.PTS.Examples.Equality |
| equivalenceScript | Language.PTS.Examples.Equality |
| Err | Language.PTS.Error, Language.PTS |
| errorlessValueElim | Language.PTS.Value, Language.PTS |
| errorlessValueElim' | Language.PTS.Value, Language.PTS |
| errorlessValueIntro | Language.PTS.Value, Language.PTS |
| errorlessValueIntro' | Language.PTS.Value, Language.PTS |
| evaluatorError | Language.PTS.Examples.Errors, Language.PTS.Examples |
| evenOrOddScript | Language.PTS.Examples.EvenOrOdd |
| example_ | Language.PTS.Script, Language.PTS |
| F | Language.PTS.Bound |
| foralls_ | Language.PTS.Smart, Language.PTS |
| forall_ | Language.PTS.Smart, Language.PTS |
| fromScope | Language.PTS.Bound |
| fromScopeH | Language.PTS.Bound |
| fromTermInf | Language.PTS.Smart, Language.PTS |
| Hadron | Language.PTS.Term, Language.PTS |
| HasBox | Language.PTS.Specification, Language.PTS |
| HasTriangle | Language.PTS.Specification, Language.PTS |
| HindleyMilner | Language.PTS.Systems |
| hindleyMilnerIdentity | Language.PTS.Examples.Identity, Language.PTS.Examples |
| HMMono | Language.PTS.Systems |
| HMPoly | Language.PTS.Systems |
| HOL | Language.PTS.Systems |
| HOLBox | Language.PTS.Systems |
| HOLStar | Language.PTS.Systems |
| HOLTri | Language.PTS.Systems |
| hurkensScript | Language.PTS.Examples.Hurkens, Language.PTS.Examples |
| I | Language.PTS.Term, Language.PTS |
| inequalityScript | Language.PTS.Examples.Equality |
| Inf | Language.PTS.Term, Language.PTS |
| instantiate1 | Language.PTS.Bound |
| instantiate1H | Language.PTS.Bound |
| instantiate1Hreturn | Language.PTS.Bound |
| instantiate1return | Language.PTS.Bound |
| instantiate2 | Language.PTS.Bound |
| instantiate2H | Language.PTS.Bound |
| instantiate2Hreturn | Language.PTS.Bound |
| instantiate2return | Language.PTS.Bound |
| instantiate3 | Language.PTS.Bound |
| instantiate3H | Language.PTS.Bound |
| instantiate3Hreturn | Language.PTS.Bound |
| instantiate3return | Language.PTS.Bound |
| instantiateHEither | Language.PTS.Bound |
| IrrSym | |
| 1 (Type/Class) | Language.PTS.Sym, Language.PTS |
| 2 (Data Constructor) | Language.PTS.Sym, Language.PTS |
| IrrSym1 | Language.PTS.Sym, Language.PTS |
| IrrSym2 | |
| 1 (Type/Class) | Language.PTS.Sym, Language.PTS |
| 2 (Data Constructor) | Language.PTS.Sym, Language.PTS |
| irrSym2Bool | Language.PTS.Sym, Language.PTS |
| irrSym2fold | Language.PTS.Sym, Language.PTS |
| IrrSym3 | Language.PTS.Sym, Language.PTS |
| irrSym3fold | Language.PTS.Sym, Language.PTS |
| IrrSymI | Language.PTS.Sym, Language.PTS |
| IrrSymJ | Language.PTS.Sym, Language.PTS |
| IrrSymK | Language.PTS.Sym, Language.PTS |
| J | Language.PTS.Term, Language.PTS |
| Lam | Language.PTS.Term, Language.PTS |
| LambdaNotPi | Language.PTS.Error, Language.PTS |
| LambdaStar | |
| 1 (Type/Class) | Language.PTS.Systems |
| 2 (Data Constructor) | Language.PTS.Systems |
| lambdaStarIdentity | Language.PTS.Examples.Identity, Language.PTS.Examples |
| lambdaStarPlus | Language.PTS.Examples |
| lams_ | Language.PTS.Smart, Language.PTS |
| lam_ | Language.PTS.Smart, Language.PTS |
| leibnizScript | Language.PTS.Examples.Equality |
| let_ | Language.PTS.Smart, Language.PTS |
| liftH | Language.PTS.Bound |
| liftPpp | Language.PTS.Pretty |
| liftS | Language.PTS.Bound |
| mapValueIntroError | Language.PTS.Value, Language.PTS |
| MartinLof | |
| 1 (Type/Class) | Language.PTS.Systems |
| 2 (Data Constructor) | Language.PTS.Systems |
| martinLofIdentity | Language.PTS.Examples.Identity, Language.PTS.Examples |
| Match | Language.PTS.Term, Language.PTS |
| MismatchFailure | Language.PTS.Error, Language.PTS |
| Module | Language.PTS.Bound |
| MonadErr | Language.PTS.Error, Language.PTS |
| monadScript | Language.PTS.Examples.Quarks |
| natCtx | Language.PTS.Examples |
| natCtx' | Language.PTS.Examples |
| natScript | Language.PTS.Examples |
| natSucc | Language.PTS.Examples |
| naturalsPrimScript | Language.PTS.Examples.Naturals |
| NonEqual | Language.PTS.Error, Language.PTS |
| NoRule | Language.PTS.Error, Language.PTS |
| NotAFunction | Language.PTS.Error, Language.PTS |
| NotAPair | Language.PTS.Error, Language.PTS |
| OccursFailure | Language.PTS.Error, Language.PTS |
| P | |
| 1 (Type/Class) | Text.Show.Extras |
| 2 (Data Constructor) | Text.Show.Extras |
| Pair | Language.PTS.Term, Language.PTS |
| PairNotSigma | Language.PTS.Error, Language.PTS |
| pairScript | Language.PTS.Examples.Sigma |
| Pi | Language.PTS.Term, Language.PTS |
| pi_ | Language.PTS.Smart, Language.PTS |
| polymorphicIdentity | Language.PTS.Examples.Identity, Language.PTS.Examples |
| PPArrow | Language.PTS.Pretty |
| PPExists | Language.PTS.Pretty |
| PPForall | Language.PTS.Pretty |
| ppp | Language.PTS.Pretty |
| ppp0 | Language.PTS.Pretty |
| ppp1 | Language.PTS.Pretty |
| pppAnnotation | Language.PTS.Pretty |
| pppAnnotationPi | Language.PTS.Pretty |
| pppApplication | Language.PTS.Pretty |
| pppCatPunctuated | Language.PTS.Pretty |
| pppChar | Language.PTS.Pretty |
| pppColon | Language.PTS.Pretty |
| pppComma_ | Language.PTS.Pretty |
| pppElim | Language.PTS.Value, Language.PTS |
| pppFreshSym | Language.PTS.Pretty |
| pppHadron | Language.PTS.Pretty |
| pppHang | Language.PTS.Pretty |
| pppHsepPunctuated | Language.PTS.Pretty |
| PPPi | |
| 1 (Type/Class) | Language.PTS.Pretty |
| 2 (Data Constructor) | Language.PTS.Pretty |
| pppIntegral | Language.PTS.Pretty |
| pppIntegralSub | Language.PTS.Pretty |
| pppIntro | Language.PTS.Value, Language.PTS |
| pppLambda | Language.PTS.Pretty |
| pppMarkSym | Language.PTS.Pretty |
| pppParens | Language.PTS.Pretty |
| pppPi | Language.PTS.Pretty |
| pppQuark | Language.PTS.Pretty |
| pppQuarkElim | Language.PTS.Pretty |
| pppScopedIrrSym | Language.PTS.Pretty |
| pppScopedSym | Language.PTS.Pretty |
| pppSepPunctuated | Language.PTS.Pretty |
| pppText | Language.PTS.Pretty |
| PPSigma | Language.PTS.Pretty |
| Prec | Language.PTS.Pretty |
| PrecAnn | Language.PTS.Pretty |
| PrecApp | Language.PTS.Pretty |
| PrecDef | Language.PTS.Pretty |
| PrecLambda | Language.PTS.Pretty |
| PrecPi | Language.PTS.Pretty |
| predPrec | Language.PTS.Pretty |
| PrettyM | Language.PTS.Pretty |
| PrettyPrec | Language.PTS.Pretty |
| PrettyPrec1 | Language.PTS.Pretty |
| prettyPut | Language.PTS.Pretty |
| prettyPutWith | Language.PTS.Pretty |
| prettyShow | Language.PTS.Pretty |
| prettyShowWith | Language.PTS.Pretty |
| pureValueElim | Language.PTS.Value, Language.PTS |
| pureValueIntro | Language.PTS.Value, Language.PTS |
| Quark | Language.PTS.Term, Language.PTS |
| QuarkElim | Language.PTS.Term, Language.PTS |
| QuarkNotHadron | Language.PTS.Error, Language.PTS |
| QuarkNotInHadron | Language.PTS.Error, Language.PTS |
| quarkSyntaxScript | Language.PTS.Examples.Quarks |
| Quote | Language.PTS.Quote, Language.PTS |
| quote_ | Language.PTS.Quote, Language.PTS |
| Refl | Language.PTS.Term, Language.PTS |
| ReflNotEquality | Language.PTS.Error, Language.PTS |
| rule | Language.PTS.Specification, Language.PTS |
| runLoud | Language.PTS.Script, Language.PTS |
| runSilent | Language.PTS.Script, Language.PTS |
| runString | Language.PTS.Script, Language.PTS |
| Scope | |
| 1 (Type/Class) | Language.PTS.Bound |
| 2 (Data Constructor) | Language.PTS.Bound |
| ScopeChkInf | Language.PTS.Term, Language.PTS |
| scopeError | Language.PTS.Examples.Errors, Language.PTS.Examples |
| ScopeH | |
| 1 (Type/Class) | Language.PTS.Bound |
| 2 (Data Constructor) | Language.PTS.Bound |
| ScopeInf | Language.PTS.Term, Language.PTS |
| Script | Language.PTS.Script, Language.PTS |
| ScriptT | Language.PTS.Script, Language.PTS |
| section_ | Language.PTS.Script, Language.PTS |
| showsQuadWith | Text.Show.Extras |
| showsQuintWith | Text.Show.Extras |
| showsTernaryWith | Text.Show.Extras |
| Sigma | Language.PTS.Term, Language.PTS |
| sigma_ | Language.PTS.Smart, Language.PTS |
| SomeErr | Language.PTS.Error, Language.PTS |
| Sort | Language.PTS.Term, Language.PTS |
| SortMismatch | Language.PTS.Error, Language.PTS |
| SortWithoutAxiom | Language.PTS.Error, Language.PTS |
| sort_ | Language.PTS.Smart, Language.PTS |
| Specification | Language.PTS.Specification, Language.PTS |
| specificationDoc | Language.PTS.Specification, Language.PTS |
| spec_ | Language.PTS.Script, Language.PTS |
| star_ | Language.PTS.Specification, Language.PTS |
| STLC | Language.PTS.Systems |
| stlcBoolIdentity | Language.PTS.Examples.Identity, Language.PTS.Examples |
| STLCBox | Language.PTS.Systems |
| stlcIdentity | Language.PTS.Examples.Identity, Language.PTS.Examples |
| STLCStar | Language.PTS.Systems |
| stlcUnitIdentity | Language.PTS.Examples.Identity, Language.PTS.Examples |
| subDigit | Language.PTS.Sym, Language.PTS |
| subsection_ | Language.PTS.Script, Language.PTS |
| Sym | |
| 1 (Type/Class) | Language.PTS.Sym, Language.PTS |
| 2 (Data Constructor) | Language.PTS.Sym, Language.PTS |
| SysFBox | Language.PTS.Systems |
| SysFStar | Language.PTS.Systems |
| SystemF | Language.PTS.Systems |
| systemfIdentity | Language.PTS.Examples.Identity, Language.PTS.Examples |
| SystemU | Language.PTS.Systems |
| SysUBox | Language.PTS.Systems |
| SysUStar | Language.PTS.Systems |
| SysUTri | Language.PTS.Systems |
| Term | Language.PTS.Term, Language.PTS |
| TermAnd | Language.PTS.Term, Language.PTS |
| TermBool | Language.PTS.Term, Language.PTS |
| TermBoolElim | Language.PTS.Term, Language.PTS |
| TermChk | Language.PTS.Term, Language.PTS |
| TermConv | Language.PTS.Smart, Language.PTS |
| TermFalse | Language.PTS.Term, Language.PTS |
| TermInf | Language.PTS.Term, Language.PTS |
| TermNat | Language.PTS.Term, Language.PTS |
| TermNatElim | Language.PTS.Term, Language.PTS |
| TermNatS | Language.PTS.Term, Language.PTS |
| TermNatZ | Language.PTS.Term, Language.PTS |
| TermPlus | Language.PTS.Term, Language.PTS |
| TermTimes | Language.PTS.Term, Language.PTS |
| TermTrue | Language.PTS.Term, Language.PTS |
| throwErr | Language.PTS.Error, Language.PTS |
| toScope | Language.PTS.Bound |
| toTermChk | Language.PTS.Smart, Language.PTS |
| toValueIntro | Language.PTS.Smart, Language.PTS |
| transverseScope | Language.PTS.Bound |
| triangle_ | Language.PTS.Specification, Language.PTS |
| TypeMismatch | Language.PTS.Error, Language.PTS |
| typeSort | Language.PTS.Specification, Language.PTS |
| typeSortSort | Language.PTS.Specification, Language.PTS |
| type_ | Language.PTS.Check, Language.PTS |
| Unit | Language.PTS.Term, Language.PTS |
| unscope | Language.PTS.Bound |
| unscopeH | Language.PTS.Bound |
| unsubDigit | Language.PTS.Sym, Language.PTS |
| unusedScope | Language.PTS.Bound |
| unvar | Language.PTS.Bound |
| V3 | |
| 1 (Type/Class) | Language.PTS.Sym, Language.PTS |
| 2 (Data Constructor) | Language.PTS.Sym, Language.PTS |
| Value | Language.PTS.Value, Language.PTS |
| ValueAbsurd | Language.PTS.Value, Language.PTS |
| valueAbsurd | Language.PTS.Value, Language.PTS |
| ValueAnd | Language.PTS.Value, Language.PTS |
| valueAnd | Language.PTS.Value, Language.PTS |
| ValueApp | Language.PTS.Value, Language.PTS |
| valueApp | Language.PTS.Value, Language.PTS |
| ValueBool | Language.PTS.Value, Language.PTS |
| ValueBoolElim | Language.PTS.Value, Language.PTS |
| valueBoolElim | Language.PTS.Value, Language.PTS |
| ValueCoerce | Language.PTS.Value, Language.PTS |
| ValueConv | Language.PTS.Smart, Language.PTS |
| ValueElim | Language.PTS.Value, Language.PTS |
| ValueEmpty | Language.PTS.Value, Language.PTS |
| ValueEquality | Language.PTS.Value, Language.PTS |
| ValueErr | Language.PTS.Value, Language.PTS |
| ValueFalse | Language.PTS.Value, Language.PTS |
| ValueHadron | Language.PTS.Value, Language.PTS |
| ValueI | Language.PTS.Value, Language.PTS |
| ValueIntro | Language.PTS.Value, Language.PTS |
| ValueJ | Language.PTS.Value, Language.PTS |
| valueJ | Language.PTS.Value, Language.PTS |
| ValueLam | Language.PTS.Value, Language.PTS |
| ValueMatch | Language.PTS.Value, Language.PTS |
| valueMatch | Language.PTS.Value, Language.PTS |
| ValueNat | Language.PTS.Value, Language.PTS |
| ValueNatElim | Language.PTS.Value, Language.PTS |
| valueNatElim | Language.PTS.Value, Language.PTS |
| ValueNatS | Language.PTS.Value, Language.PTS |
| ValueNatZ | Language.PTS.Value, Language.PTS |
| ValuePair | Language.PTS.Value, Language.PTS |
| ValuePi | Language.PTS.Value, Language.PTS |
| ValuePlus | Language.PTS.Value, Language.PTS |
| valuePlus | Language.PTS.Value, Language.PTS |
| ValueQuark | Language.PTS.Value, Language.PTS |
| ValueQuarkElim | Language.PTS.Value, Language.PTS |
| valueQuarkElim | Language.PTS.Value, Language.PTS |
| ValueRefl | Language.PTS.Value, Language.PTS |
| ValueSigma | Language.PTS.Value, Language.PTS |
| ValueSort | Language.PTS.Value, Language.PTS |
| ValueTimes | Language.PTS.Value, Language.PTS |
| valueTimes | Language.PTS.Value, Language.PTS |
| ValueTrue | Language.PTS.Value, Language.PTS |
| valueType_ | Language.PTS.Value.Check |
| ValueUnit | Language.PTS.Value, Language.PTS |
| ValueVar | Language.PTS.Value, Language.PTS |
| Var | |
| 1 (Type/Class) | Language.PTS.Bound |
| 2 (Data Constructor) | Language.PTS.Term, Language.PTS |
| VariableNotInScope | Language.PTS.Error, Language.PTS |
| WHNF | Language.PTS.WHNF, Language.PTS |
| whnf | Language.PTS.WHNF, Language.PTS |
| _Err | Language.PTS.Error, Language.PTS |
| ~> | Language.PTS.Smart, Language.PTS |