| 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 |
| tModAccum | Rzk.TypeCheck |
| TModality | Language.Rzk.Free.Syntax |
| tModVar | Rzk.TypeCheck |
| Tok | Language.Rzk.Syntax.Lex |
| tok | Language.Rzk.Syntax.Lex |
| Token | Language.Rzk.Syntax.Lex |
| tokenizeBind | Language.Rzk.VSCode.Tokenize |
| tokenizeCommand | Language.Rzk.VSCode.Tokenize |
| tokenizeLanguageDecl | Language.Rzk.VSCode.Tokenize |
| tokenizeModalColon | Language.Rzk.VSCode.Tokenize |
| tokenizeModality | Language.Rzk.VSCode.Tokenize |
| tokenizeModComp | Language.Rzk.VSCode.Tokenize |
| tokenizeModule | Language.Rzk.VSCode.Tokenize |
| tokenizeParam | Language.Rzk.VSCode.Tokenize |
| tokenizeParamDecl | Language.Rzk.VSCode.Tokenize |
| tokenizePattern | Language.Rzk.VSCode.Tokenize |
| tokenizeRestriction | Language.Rzk.VSCode.Tokenize |
| tokenizeSigmaParam | Language.Rzk.VSCode.Tokenize |
| tokenizeTerm | Language.Rzk.VSCode.Tokenize |
| tokenizeTerm' | Language.Rzk.VSCode.Tokenize |
| tokenizeTope | Language.Rzk.VSCode.Tokenize |
| 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 |
| toModality | Language.Rzk.Free.Syntax |
| TopDown | Rzk.TypeCheck |
| 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 |
| TopeInv | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeInvE | Language.Rzk.Free.Syntax |
| TopeInvF | Language.Rzk.Free.Syntax |
| TopeInvT | Language.Rzk.Free.Syntax |
| topeInvT | Rzk.TypeCheck |
| TopeInvTE | 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 |
| TopeUninv | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeUninvE | Language.Rzk.Free.Syntax |
| TopeUninvF | Language.Rzk.Free.Syntax |
| TopeUninvT | Language.Rzk.Free.Syntax |
| topeUninvT | Rzk.TypeCheck |
| TopeUninvTE | 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 |
| tryOrDisplayException | Language.Rzk.Syntax |
| tryOrDisplayExceptionIO | Language.Rzk.Syntax |
| tryRestriction | Rzk.TypeCheck |
| TS | Language.Rzk.Syntax.Lex |
| tsID | Language.Rzk.Syntax.Lex |
| tsText | Language.Rzk.Syntax.Lex |
| tTope | Rzk.TypeCheck |
| Tuple | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 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 |
| typecheckFromConfigFile | Language.Rzk.VSCode.Handlers |
| typecheckModule | Rzk.TypeCheck |
| typecheckModules | Rzk.TypeCheck |
| typecheckModulesWithHoles | Rzk.TypeCheck |
| typecheckModulesWithHolesAndLemmas | Rzk.TypeCheck |
| typecheckModulesWithLocation | Rzk.TypeCheck |
| typecheckModulesWithLocation' | Rzk.TypeCheck |
| typecheckModulesWithLocationIncremental | Rzk.TypeCheck |
| typecheckModuleWithLocation | Rzk.TypeCheck |
| typecheckString | Rzk.Main |
| TypeError | Rzk.TypeCheck |
| TypeError' | Rzk.TypeCheck |
| TypeErrorCannotInferBareLambda | Rzk.TypeCheck |
| TypeErrorCannotInferBareRefl | Rzk.TypeCheck |
| TypeErrorCannotInferHole | 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 |
| TypeErrorModalityMismatch | Rzk.TypeCheck |
| TypeErrorNotFunction | Rzk.TypeCheck |
| TypeErrorNotModal | Rzk.TypeCheck |
| TypeErrorNotPair | Rzk.TypeCheck |
| TypeErrorNotTypeInModal | Rzk.TypeCheck |
| TypeErrorOther | Rzk.TypeCheck |
| typeErrorTag | Rzk.Diagnostic |
| typeErrorTagInScopedContext | Rzk.Diagnostic |
| TypeErrorTopeContextDisjoint | Rzk.TypeCheck |
| TypeErrorTopeNotSatisfied | Rzk.TypeCheck |
| TypeErrorTopesNotEquivalent | Rzk.TypeCheck |
| TypeErrorUnaccessibleVar | Rzk.TypeCheck |
| TypeErrorUndefined | Rzk.TypeCheck |
| TypeErrorUnexpectedLambda | Rzk.TypeCheck |
| TypeErrorUnexpectedPair | Rzk.TypeCheck |
| TypeErrorUnexpectedRefl | Rzk.TypeCheck |
| TypeErrorUnify | Rzk.TypeCheck |
| TypeErrorUnifyTerms | Rzk.TypeCheck |
| TypeErrorUnsolvedHole | Rzk.TypeCheck |
| TypeErrorUnusedUsedVariables | Rzk.TypeCheck |
| TypeErrorUnusedVariable | Rzk.TypeCheck |
| TypeExtensionDeprecated | 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 |
| TypeModal | Language.Rzk.Free.Syntax |
| TypeModalE | Language.Rzk.Free.Syntax |
| TypeModalF | Language.Rzk.Free.Syntax |
| TypeModalT | Language.Rzk.Free.Syntax |
| typeModalT | Rzk.TypeCheck |
| TypeModalTE | 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 |
| TypeSigmaModal | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TypeSigmaT | Language.Rzk.Free.Syntax |
| typeSigmaT | Rzk.TypeCheck |
| TypeSigmaTE | Language.Rzk.Free.Syntax |
| TypeSigmaTuple | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TypeUnit | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeUnitE | Language.Rzk.Free.Syntax |
| TypeUnitF | Language.Rzk.Free.Syntax |
| TypeUnitT | Language.Rzk.Free.Syntax |
| typeUnitT | Rzk.TypeCheck |
| TypeUnitTE | Language.Rzk.Free.Syntax |
| T_HoleIdentToken | Language.Rzk.Syntax.Lex |
| T_VarIdentToken | Language.Rzk.Syntax.Lex |