| 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.Foil.Syntax |
| Term' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| termIsNF | Language.Rzk.Foil.Syntax |
| termIsWHNF | Language.Rzk.Foil.Syntax |
| TermSig | Language.Rzk.Foil.Syntax |
| TermT | Language.Rzk.Foil.Syntax |
| TI | Language.Rzk.Syntax.Lex |
| TK | Language.Rzk.Syntax.Lex |
| TL | Language.Rzk.Syntax.Lex |
| tModAccum | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| TModality | Language.Rzk.Foil.Names |
| tModVar | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| toBinder | Language.Rzk.Foil.Names |
| 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 |
| tokenizeCommands | Language.Rzk.VSCode.Tokenize |
| tokenizeConstructor | Language.Rzk.VSCode.Tokenize |
| tokenizeDataBody | Language.Rzk.VSCode.Tokenize |
| tokenizeDataElim | Language.Rzk.VSCode.Tokenize |
| tokenizeDataSort | Language.Rzk.VSCode.Tokenize |
| tokenizeDeclUsedVars | Language.Rzk.VSCode.Tokenize |
| tokenizeLanguageDecl | Language.Rzk.VSCode.Tokenize |
| tokenizeMatchBranch | 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 |
| tokenizeSectionName | Language.Rzk.VSCode.Tokenize |
| tokenizeSigmaParam | Language.Rzk.VSCode.Tokenize |
| tokenizeSyntaxSymbols | 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 |
| tokensToUtf16 | Language.Rzk.VSCode.PositionEncoding |
| tokenText | Language.Rzk.Syntax.Lex |
| TokSymbol | |
| 1 (Type/Class) | Language.Rzk.Syntax.Lex |
| 2 (Data Constructor) | Language.Rzk.Syntax.Lex |
| toModality | Language.Rzk.Foil.Names |
| TopDown | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TopeAnd | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TopeAndF | Language.Rzk.Foil.Syntax |
| TopeAndT | Language.Rzk.Foil.Syntax |
| topeAndT | Language.Rzk.Foil.Syntax |
| TopeBottom | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TopeBottomF | Language.Rzk.Foil.Syntax |
| TopeBottomT | Language.Rzk.Foil.Syntax |
| topeBottomT | Language.Rzk.Foil.Syntax |
| TopeEQ | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TopeEQF | Language.Rzk.Foil.Syntax |
| TopeEQT | Language.Rzk.Foil.Syntax |
| topeEQT | Language.Rzk.Foil.Syntax |
| topeInfo | Language.Rzk.Foil.Syntax |
| TopeInv | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TopeInvF | Language.Rzk.Foil.Syntax |
| TopeInvT | Language.Rzk.Foil.Syntax |
| topeInvT | Language.Rzk.Foil.Syntax |
| TopeLEQ | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TopeLEQF | Language.Rzk.Foil.Syntax |
| TopeLEQT | Language.Rzk.Foil.Syntax |
| topeLEQT | Language.Rzk.Foil.Syntax |
| TopeOr | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TopeOrF | Language.Rzk.Foil.Syntax |
| TopeOrT | Language.Rzk.Foil.Syntax |
| topeOrT | Language.Rzk.Foil.Syntax |
| topePoints | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| topesEquiv | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| topeT | Language.Rzk.Foil.Syntax |
| TopeTop | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TopeTopF | Language.Rzk.Foil.Syntax |
| TopeTopT | Language.Rzk.Foil.Syntax |
| topeTopT | Language.Rzk.Foil.Syntax |
| TopeUninv | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TopeUninvF | Language.Rzk.Foil.Syntax |
| TopeUninvT | Language.Rzk.Foil.Syntax |
| topeUninvT | Language.Rzk.Foil.Syntax |
| toScopedAnon | Language.Rzk.Foil.Convert |
| toScopedPattern | Language.Rzk.Foil.Convert |
| toScopedPatternWith | Language.Rzk.Foil.Convert |
| toTerm | Language.Rzk.Foil.Convert |
| toTermClosed | Language.Rzk.Foil.Convert |
| trace' | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| traceTypeCheck | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| tryCheck | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| tryDataElimStep | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| tryExtractMarkdownCodeBlocks | Language.Rzk.Syntax |
| tryOrDisplayException | Language.Rzk.Syntax |
| tryOrDisplayExceptionIO | Language.Rzk.Syntax |
| tryRestriction | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| TS | Language.Rzk.Syntax.Lex |
| tsID | Language.Rzk.Syntax.Lex |
| tsText | Language.Rzk.Syntax.Lex |
| tTope | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Tuple | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TV | Language.Rzk.Syntax.Lex |
| TypeAsc | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TypeAscF | Language.Rzk.Foil.Syntax |
| TypeAscT | Language.Rzk.Foil.Syntax |
| typeAscT | Language.Rzk.Foil.Syntax |
| TypeCheck | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| typecheck | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| typecheckFromConfigFile | Language.Rzk.VSCode.Handlers |
| typecheckModules | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| typecheckModulesWithHoles | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| typecheckModulesWithHolesAndLemmas | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| typecheckString | Rzk.Main |
| TypeError | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorCannotInferBareLambda | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorCannotInferBareRefl | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorCannotInferHole | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorDuplicateTopLevel | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| typeErrorHere | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| TypeErrorImplicitAssumption | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorInScopedContext | |
| 1 (Type/Class) | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorInvalidArgumentType | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorMatchBranchArity | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorMatchCannotInfer | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorMatchDuplicateBranch | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorMatchMissingBranch | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorMatchScrutineeNotData | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorMatchUnknownBranch | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorModalityMismatch | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorNotFunction | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorNotIntervalCube | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorNotModal | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorNotPair | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorNotTypeInModal | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorOther | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorReascribedTypeMismatch | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorRepeatedBinder | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| typeErrorTag | Rzk.Diagnostic |
| typeErrorTagInScopedContext | Rzk.Diagnostic |
| TypeErrorTopeContextDisjoint | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorTopeNotSatisfied | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorTopesNotEquivalent | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnaccessibleVar | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUndefined | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnexpectedLambda | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnexpectedPair | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnexpectedRefl | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnify | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnifyTerms | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnsolvedHole | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnusedUsedVariables | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeErrorUnusedVariable | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| TypeFun | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TypeFunF | Language.Rzk.Foil.Syntax |
| TypeFunT | Language.Rzk.Foil.Syntax |
| typeFunT | Language.Rzk.Foil.Syntax |
| TypeId | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TypeIdF | Language.Rzk.Foil.Syntax |
| TypeIdSimple | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TypeIdT | Language.Rzk.Foil.Syntax |
| typeIdT | Language.Rzk.Foil.Syntax |
| TypeInfo | |
| 1 (Type/Class) | Language.Rzk.Foil.Names |
| 2 (Data Constructor) | Language.Rzk.Foil.Names |
| typeInfoOf | Language.Rzk.Foil.Syntax |
| TypeModal | Language.Rzk.Foil.Syntax |
| TypeModalF | Language.Rzk.Foil.Syntax |
| TypeModalT | Language.Rzk.Foil.Syntax |
| typeModalT | Language.Rzk.Foil.Syntax |
| typeOf | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| typeOfUncomputed | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| typeOfVar | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| TypeRestricted | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TypeRestrictedF | Language.Rzk.Foil.Syntax |
| TypeRestrictedT | Language.Rzk.Foil.Syntax |
| typeRestrictedT | Language.Rzk.Foil.Syntax |
| TypeSigma | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| TypeSigmaF | Language.Rzk.Foil.Syntax |
| TypeSigmaModal | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TypeSigmaT | Language.Rzk.Foil.Syntax |
| typeSigmaT | Language.Rzk.Foil.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.Foil.Syntax |
| TypeUnitF | Language.Rzk.Foil.Syntax |
| TypeUnitT | Language.Rzk.Foil.Syntax |
| typeUnitT | Language.Rzk.Foil.Syntax |
| TypeView | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| T_HoleIdentToken | Language.Rzk.Syntax.Lex |
| T_VarIdentToken | Language.Rzk.Syntax.Lex |