| TC | Language.Rzk.Syntax.Lex |
| TD | Language.Rzk.Syntax.Lex |
| Tentative | Language.Rzk.Syntax.Layout |
| Term | |
| 1 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Free.Syntax |
| Term' | |
| 1 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Free.Syntax |
| TermF | Language.Rzk.Free.Syntax |
| termF | Free.Scoped |
| termIsNF | Language.Rzk.Free.Syntax |
| termIsWHNF | Language.Rzk.Free.Syntax |
| TermT | Language.Rzk.Free.Syntax |
| TermT' | Language.Rzk.Free.Syntax |
| TI | Language.Rzk.Syntax.Lex |
| TK | Language.Rzk.Syntax.Lex |
| TL | Language.Rzk.Syntax.Lex |
| Tok | Language.Rzk.Syntax.Lex |
| tok | Language.Rzk.Syntax.Lex |
| Token | Language.Rzk.Syntax.Lex |
| tokenLength | Language.Rzk.Syntax.Layout |
| tokenLineCol | Language.Rzk.Syntax.Lex |
| tokenPos | Language.Rzk.Syntax.Lex |
| tokenPosn | Language.Rzk.Syntax.Lex |
| tokens | Language.Rzk.Syntax.Lex |
| tokenText | Language.Rzk.Syntax.Lex |
| TokSymbol | |
| 1 (Type/Class) | Language.Rzk.Syntax.Lex |
| 2 (Data Constructor) | Language.Rzk.Syntax.Lex |
| TopeAnd | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeAndE | Language.Rzk.Free.Syntax |
| TopeAndF | Language.Rzk.Free.Syntax |
| TopeAndT | Language.Rzk.Free.Syntax |
| topeAndT | Rzk.TypeCheck |
| TopeAndTE | Language.Rzk.Free.Syntax |
| TopeBottom | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeBottomE | Language.Rzk.Free.Syntax |
| TopeBottomF | Language.Rzk.Free.Syntax |
| TopeBottomT | Language.Rzk.Free.Syntax |
| topeBottomT | Rzk.TypeCheck |
| TopeBottomTE | Language.Rzk.Free.Syntax |
| TopeEQ | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeEQE | Language.Rzk.Free.Syntax |
| TopeEQF | Language.Rzk.Free.Syntax |
| TopeEQT | Language.Rzk.Free.Syntax |
| topeEQT | Rzk.TypeCheck |
| TopeEQTE | Language.Rzk.Free.Syntax |
| TopeLEQ | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeLEQE | Language.Rzk.Free.Syntax |
| TopeLEQF | Language.Rzk.Free.Syntax |
| TopeLEQT | Language.Rzk.Free.Syntax |
| topeLEQT | Rzk.TypeCheck |
| TopeLEQTE | Language.Rzk.Free.Syntax |
| TopeOr | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeOrE | Language.Rzk.Free.Syntax |
| TopeOrF | Language.Rzk.Free.Syntax |
| TopeOrT | Language.Rzk.Free.Syntax |
| topeOrT | Rzk.TypeCheck |
| TopeOrTE | Language.Rzk.Free.Syntax |
| topePoints | Rzk.TypeCheck |
| topesEquiv | Rzk.TypeCheck |
| topeT | Rzk.TypeCheck |
| TopeTop | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeTopE | Language.Rzk.Free.Syntax |
| TopeTopF | Language.Rzk.Free.Syntax |
| TopeTopT | Language.Rzk.Free.Syntax |
| topeTopT | Rzk.TypeCheck |
| TopeTopTE | Language.Rzk.Free.Syntax |
| toScope | Language.Rzk.Free.Syntax |
| toScopePattern | Language.Rzk.Free.Syntax |
| toTerm | Language.Rzk.Free.Syntax |
| toTerm' | Language.Rzk.Free.Syntax |
| trace' | Rzk.TypeCheck |
| traceAction' | Rzk.TypeCheck |
| traceStartAndFinish | Rzk.TypeCheck |
| traceTypeCheck | Rzk.TypeCheck |
| transFS | Free.Scoped |
| tryExtractMarkdownCodeBlocks | Language.Rzk.Syntax |
| tryRestriction | Rzk.TypeCheck |
| TS | Language.Rzk.Syntax.Lex |
| tsID | Language.Rzk.Syntax.Lex |
| tsText | Language.Rzk.Syntax.Lex |
| TV | Language.Rzk.Syntax.Lex |
| Type | |
| 1 (Type/Class) | Language.Rzk.Free.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeAsc | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeAscE | Language.Rzk.Free.Syntax |
| TypeAscF | Language.Rzk.Free.Syntax |
| TypeAscT | Language.Rzk.Free.Syntax |
| typeAscT | Rzk.TypeCheck |
| TypeAscTE | Language.Rzk.Free.Syntax |
| TypeCheck | Rzk.TypeCheck |
| typecheck | Rzk.TypeCheck |
| typecheckModule | Rzk.TypeCheck |
| typecheckModules | Rzk.TypeCheck |
| typecheckModulesWithLocation | Rzk.TypeCheck |
| typecheckModuleWithLocation | Rzk.TypeCheck |
| typecheckString | Rzk.Main |
| TypeError | Rzk.TypeCheck |
| TypeError' | Rzk.TypeCheck |
| TypeErrorCannotInferBareLambda | Rzk.TypeCheck |
| TypeErrorCannotInferBareRefl | Rzk.TypeCheck |
| typeErrorContext | Rzk.TypeCheck |
| TypeErrorDuplicateTopLevel | Rzk.TypeCheck |
| typeErrorError | Rzk.TypeCheck |
| TypeErrorImplicitAssumption | Rzk.TypeCheck |
| TypeErrorInContext | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| TypeErrorInScopedContext | Rzk.TypeCheck |
| TypeErrorInvalidArgumentType | Rzk.TypeCheck |
| TypeErrorNotFunction | Rzk.TypeCheck |
| TypeErrorNotPair | Rzk.TypeCheck |
| TypeErrorOther | Rzk.TypeCheck |
| TypeErrorTopeNotSatisfied | Rzk.TypeCheck |
| TypeErrorTopesNotEquivalent | Rzk.TypeCheck |
| TypeErrorUndefined | Rzk.TypeCheck |
| TypeErrorUnexpectedLambda | Rzk.TypeCheck |
| TypeErrorUnexpectedPair | Rzk.TypeCheck |
| TypeErrorUnexpectedRefl | Rzk.TypeCheck |
| TypeErrorUnify | Rzk.TypeCheck |
| TypeErrorUnifyTerms | Rzk.TypeCheck |
| TypeErrorUnusedUsedVariables | Rzk.TypeCheck |
| TypeErrorUnusedVariable | Rzk.TypeCheck |
| typeExtension | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TypeFun | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeFunE | Language.Rzk.Free.Syntax |
| TypeFunF | Language.Rzk.Free.Syntax |
| TypeFunT | Language.Rzk.Free.Syntax |
| typeFunT | Rzk.TypeCheck |
| TypeFunTE | Language.Rzk.Free.Syntax |
| TypeId | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeIdE | Language.Rzk.Free.Syntax |
| TypeIdF | Language.Rzk.Free.Syntax |
| TypeIdSimple | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TypeIdT | Language.Rzk.Free.Syntax |
| typeIdT | Rzk.TypeCheck |
| TypeIdTE | Language.Rzk.Free.Syntax |
| TypeInfo | |
| 1 (Type/Class) | Language.Rzk.Free.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| typeOf | Rzk.TypeCheck |
| typeOfUncomputed | Rzk.TypeCheck |
| typeOfVar | Rzk.TypeCheck |
| TypeRestricted | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeRestrictedE | Language.Rzk.Free.Syntax |
| TypeRestrictedF | Language.Rzk.Free.Syntax |
| TypeRestrictedT | Language.Rzk.Free.Syntax |
| typeRestrictedT | Rzk.TypeCheck |
| TypeRestrictedTE | Language.Rzk.Free.Syntax |
| TypeSigma | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeSigmaE | Language.Rzk.Free.Syntax |
| TypeSigmaF | Language.Rzk.Free.Syntax |
| TypeSigmaT | Language.Rzk.Free.Syntax |
| typeSigmaT | Rzk.TypeCheck |
| TypeSigmaTE | Language.Rzk.Free.Syntax |
| T_HoleIdent | Language.Rzk.Syntax.Lex |
| T_VarIdent | Language.Rzk.Syntax.Lex |