| abstractName | Language.Rzk.Foil.Syntax |
| abstractOver | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| accessibleTopes | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Action | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionCheckCoherence | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionCheckLetValue | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionCloseSection | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionContextEntailedBy | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionContextEntails | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionContextEntailsUnion | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionInfer | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionNF | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionTypeCheck | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionUnify | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionUnifyTerms | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ActionWHNF | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| addBinderNames | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| addImplicit | Language.Rzk.Syntax.Layout |
| addParamDecls | Rzk.TypeCheck.Decl.Data |
| addParams | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| afterPrev | Language.Rzk.Syntax.Layout |
| AlexA# | Language.Rzk.Syntax.Lex |
| AlexAcc | |
| 1 (Type/Class) | Language.Rzk.Syntax.Lex |
| 2 (Data Constructor) | Language.Rzk.Syntax.Lex |
| AlexAccNone | Language.Rzk.Syntax.Lex |
| AlexAccSkip | Language.Rzk.Syntax.Lex |
| AlexAddr | Language.Rzk.Syntax.Lex |
| AlexEOF | Language.Rzk.Syntax.Lex |
| AlexError | Language.Rzk.Syntax.Lex |
| alexGetByte | Language.Rzk.Syntax.Lex |
| alexIndexInt16OffAddr | Language.Rzk.Syntax.Lex |
| alexIndexInt32OffAddr | Language.Rzk.Syntax.Lex |
| AlexInput | Language.Rzk.Syntax.Lex |
| alexInputPrevChar | Language.Rzk.Syntax.Lex |
| AlexLastAcc | |
| 1 (Type/Class) | Language.Rzk.Syntax.Lex |
| 2 (Data Constructor) | Language.Rzk.Syntax.Lex |
| AlexLastSkip | Language.Rzk.Syntax.Lex |
| alexMove | Language.Rzk.Syntax.Lex |
| AlexNone | Language.Rzk.Syntax.Lex |
| AlexReturn | Language.Rzk.Syntax.Lex |
| alexScan | Language.Rzk.Syntax.Lex |
| alexScanUser | Language.Rzk.Syntax.Lex |
| AlexSkip | Language.Rzk.Syntax.Lex |
| alexStartPos | Language.Rzk.Syntax.Lex |
| AlexToken | Language.Rzk.Syntax.Lex |
| alex_accept | Language.Rzk.Syntax.Lex |
| alex_actions | Language.Rzk.Syntax.Lex |
| alex_action_3 | Language.Rzk.Syntax.Lex |
| alex_action_4 | Language.Rzk.Syntax.Lex |
| alex_action_5 | Language.Rzk.Syntax.Lex |
| alex_action_6 | Language.Rzk.Syntax.Lex |
| alex_action_7 | Language.Rzk.Syntax.Lex |
| alex_base | Language.Rzk.Syntax.Lex |
| alex_check | Language.Rzk.Syntax.Lex |
| alex_deflt | Language.Rzk.Syntax.Lex |
| alex_scan_tkn | Language.Rzk.Syntax.Lex |
| alex_table | Language.Rzk.Syntax.Lex |
| alex_tab_size | Language.Rzk.Syntax.Lex |
| allEliminationsInto | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| allIntroductionsOf | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| allM | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| allowHoles | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| allTopePoints | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| alphaEq | Rzk.TypeCheck.Unify |
| alphaEqT | Language.Rzk.Foil.Syntax |
| App | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| AppF | Language.Rzk.Foil.Syntax |
| applyModality | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| applyModalityToTopes | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| applyNeutral | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| applyPlan | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| applySpine | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| applyToAssumption | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| applyTyped | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| applyWhnfFun | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| AppT | Language.Rzk.Foil.Syntax |
| appT | Language.Rzk.Foil.Syntax |
| armCount | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| ASCII_Cube2_0 | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_Cube2_1 | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_CubeFlip | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_CubeI | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_CubeInf | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_CubeI_0 | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_CubeI_1 | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_CubeProduct | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_CubeSup | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_CubeUnflip | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_CubeUnitStar | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_First | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_Flat | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_Lambda | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_MatchBranch | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_matchBranchNoParams | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_ModalColonFlat | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_ModalColonOp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_ModalColonSharp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_Op | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_Restriction | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_Second | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_Sharp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TopeAnd | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TopeBottom | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TopeEQ | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_TopeInv | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TopeLEQ | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TopeOr | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TopeTop | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_TopeUninv | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TypeFun | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TypeSigma | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ascii_TypeSigmaModal | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ASCII_TypeSigmaTuple | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| assume | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| AssumeInSection | Language.Rzk.VSCode.ReferenceIndex |
| AssumeScope | Language.Rzk.VSCode.ReferenceIndex |
| assumeScopeAt | Language.Rzk.VSCode.ReferenceIndex |
| assumeSites | Language.Rzk.VSCode.ReferenceIndex |
| AssumeTopLevel | Language.Rzk.VSCode.ReferenceIndex |
| assumptionDepsOf | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| AssumptionUnused | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| AssumptionUse | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| AssumptionUsed | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| AstralLines | Language.Rzk.VSCode.PositionEncoding |
| astralLines | Language.Rzk.VSCode.PositionEncoding |
| atPosition | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| atSrcPos | Language.Rzk.Foil.Syntax |
| atSurface | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| availableTopes | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| availableTopesNF | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| B | Language.Rzk.Syntax.Lex |
| betaMotiveApps | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| Bind | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Bind' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Binder | Language.Rzk.Foil.Names |
| binderDisplayName | Language.Rzk.Foil.Names |
| binderInfo | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| binderIsCompound | Language.Rzk.Foil.Names |
| binderLeaves | Language.Rzk.Foil.Names |
| binderName | Language.Rzk.Foil.Names |
| binderOfName | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| BinderPair | Language.Rzk.Foil.Names |
| binderPaths | Language.Rzk.Foil.Names |
| binderToPattern | Language.Rzk.Foil.Names |
| binderTypeEntries | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| binderTypesOfFile | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| binderTypesOfTerm | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| BinderTypeView | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| BinderUnit | Language.Rzk.Foil.Names |
| BinderVar | Language.Rzk.Foil.Names |
| Binding | |
| 1 (Type/Class) | Language.Rzk.VSCode.ReferenceIndex |
| 2 (Data Constructor) | Language.Rzk.VSCode.ReferenceIndex |
| bindingDef | Language.Rzk.VSCode.ReferenceIndex |
| bindingName | Language.Rzk.VSCode.ReferenceIndex |
| bindingRefs | Language.Rzk.VSCode.ReferenceIndex |
| bindings | Language.Rzk.Foil.Convert |
| bindingSites | Language.Rzk.VSCode.ReferenceIndex |
| bindingType | Language.Rzk.VSCode.ReferenceIndex |
| BindPattern | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| BindPatternType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Block | Language.Rzk.Syntax.Layout |
| block | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| BNFC'NoPosition | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| BNFC'Position | |
| 1 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| BottomUp | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| Branching | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| BTree | Language.Rzk.Syntax.Lex |
| BuildFlag | |
| 1 (Type/Class) | Rzk.Version |
| 2 (Data Constructor) | Rzk.Version |
| buildFlagName | Rzk.Version |
| buildFlags | Rzk.Version |
| buildFlagState | Rzk.Version |
| bumpDataRoleParams | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| bySubtyping | Rzk.TypeCheck.Unify |
| Byte | Language.Rzk.Syntax.Lex |
| cachedModuleChecked | Language.Rzk.VSCode.Env |
| cachedModuleDecls | Language.Rzk.VSCode.Env |
| cachedModuleErrors | Language.Rzk.VSCode.Env |
| CachedSaturation | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| cacheReferenceIndex | Language.Rzk.VSCode.Env |
| cacheTypecheckedModules | Language.Rzk.VSCode.Env |
| Camera | |
| 1 (Type/Class) | Rzk.Render.Geometry |
| 2 (Data Constructor) | Rzk.Render.Geometry |
| cameraAngleX | Rzk.Render.Geometry |
| cameraAngleY | Rzk.Render.Geometry |
| cameraAspectRatio | Rzk.Render.Geometry |
| cameraFoV | Rzk.Render.Geometry |
| cameraPos | Rzk.Render.Geometry |
| checkCoherence | Rzk.TypeCheck.Unify |
| checkCommands | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkDefined | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkDefinedVar | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| Checked | |
| 1 (Type/Class) | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkedErrors | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkedModules | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkedWarnings | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkEntails | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| checkHoleAgainstShape | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| CheckLog | |
| 1 (Type/Class) | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| checkLog | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| checkMatch | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| checkMatchArms | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| checkModule | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkModules | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkModuleWithLocation | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| checkNameShadowing | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| checkRecOrAgainst | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| checkTope | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| checkTopeAgainstContext | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| checkTopeEntails | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| checkTopLevelDuplicate | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| checkUnder | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| checkUnderWith | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| CheckWarning | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| checkWarningTag | Rzk.Diagnostic |
| classifySymbol | Language.Rzk.VSCode.Tokenize |
| classifyToken | Language.Rzk.VSCode.Tokenize |
| closedScope | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| coe | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| colFromUtf16 | Language.Rzk.VSCode.PositionEncoding |
| collectAppSpine | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| collectSectionDecls | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| collectVarIdents | Language.Rzk.Foil.Convert |
| colToUtf16 | Language.Rzk.VSCode.PositionEncoding |
| Column | Language.Rzk.Syntax.Layout |
| column | Language.Rzk.Syntax.Layout |
| Command | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Command' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandAssume | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandCheck | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandCompute | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandComputeNF | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandComputeWHNF | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandData | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| commandDataNoParams | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| commandDef | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandDefine | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| commandDefineNoParams | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| commandDefNoParams | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandPostulate | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| commandPostulateNoParams | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandSection | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandSectionEnd | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandSetOption | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| CommandUnsetOption | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| commandVariable | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| commandVariables | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Comp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| comp | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| componentWiseEQT | Rzk.TypeCheck.Render |
| computeRules | Rzk.TypeCheck.Decl.Data |
| concatD | Language.Rzk.Syntax.Print |
| concatS | Language.Rzk.Syntax.Print |
| confirm | Language.Rzk.Syntax.Layout |
| ConSort | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Constructor | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Constructor' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| constructorNoParams | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ConstructorType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ConstructorType' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| constScope | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| containsHole | Language.Rzk.Foil.Syntax |
| containsUniverse | Language.Rzk.Foil.Syntax |
| Context | |
| 1 (Type/Class) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| contextEntails | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| contextEntailsBottom | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| contextEntailsUnion | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| Contravariant | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Conversion | Rzk.TypeCheck.NbE |
| Convertible | Rzk.TypeCheck.NbE |
| countCommands | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| Covariance | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Covariant | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| coverageHolds | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| ctxActionStack | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxActionStackDepth | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxBound | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxCovariance | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxCurrentCommand | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxDeferHoleMismatches | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxDiscreteTopes | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxHintLemmas | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxHolesAreErrors | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxLocation | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxMetaPrefixSensitivity | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxNamed | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxRenderBackend | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxRenderHideTerm | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxScope | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxSections | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxShadow | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxTopes | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxTopesEntailBottom | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxTopesNF | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxTopesNFUnion | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxTopesSaturated | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxVars | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxVerbosity | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ctxWarnOverhang | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Cube2 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| Cube2F | Language.Rzk.Foil.Syntax |
| cube2powerT | Rzk.TypeCheck.Render |
| Cube2T | Language.Rzk.Foil.Syntax |
| cube2T | Language.Rzk.Foil.Syntax |
| Cube2_0 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| Cube2_0F | Language.Rzk.Foil.Syntax |
| Cube2_0T | Language.Rzk.Foil.Syntax |
| cube2_0T | Language.Rzk.Foil.Syntax |
| Cube2_1 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| Cube2_1F | Language.Rzk.Foil.Syntax |
| Cube2_1T | Language.Rzk.Foil.Syntax |
| cube2_1T | Language.Rzk.Foil.Syntax |
| CubeCoords2D | |
| 1 (Type/Class) | Rzk.Render.Geometry |
| 2 (Data Constructor) | Rzk.Render.Geometry |
| CubeFlip | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeFlipF | Language.Rzk.Foil.Syntax |
| CubeFlipT | Language.Rzk.Foil.Syntax |
| cubeFlipT | Language.Rzk.Foil.Syntax |
| CubeI | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeIF | Language.Rzk.Foil.Syntax |
| CubeInf | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeInfF | Language.Rzk.Foil.Syntax |
| CubeInfT | Language.Rzk.Foil.Syntax |
| cubeInfT | Language.Rzk.Foil.Syntax |
| CubeIT | Language.Rzk.Foil.Syntax |
| cubeIT | Language.Rzk.Foil.Syntax |
| CubeI_0 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeI_0F | Language.Rzk.Foil.Syntax |
| CubeI_0T | Language.Rzk.Foil.Syntax |
| cubeI_0T | Language.Rzk.Foil.Syntax |
| CubeI_1 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeI_1F | Language.Rzk.Foil.Syntax |
| CubeI_1T | Language.Rzk.Foil.Syntax |
| cubeI_1T | Language.Rzk.Foil.Syntax |
| CubeProduct | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeProductF | Language.Rzk.Foil.Syntax |
| CubeProductT | Language.Rzk.Foil.Syntax |
| cubeProductT | Language.Rzk.Foil.Syntax |
| CubeSup | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeSupF | Language.Rzk.Foil.Syntax |
| CubeSupT | Language.Rzk.Foil.Syntax |
| cubeSupT | Language.Rzk.Foil.Syntax |
| cubeT | Language.Rzk.Foil.Syntax |
| CubeUnflip | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeUnflipF | Language.Rzk.Foil.Syntax |
| CubeUnflipT | Language.Rzk.Foil.Syntax |
| cubeUnflipT | Language.Rzk.Foil.Syntax |
| CubeUnit | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeUnitF | Language.Rzk.Foil.Syntax |
| CubeUnitStar | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| CubeUnitStarF | Language.Rzk.Foil.Syntax |
| CubeUnitStarT | Language.Rzk.Foil.Syntax |
| cubeUnitStarT | Language.Rzk.Foil.Syntax |
| CubeUnitT | Language.Rzk.Foil.Syntax |
| cubeUnitT | Language.Rzk.Foil.Syntax |
| dataAppliedIndices | Rzk.TypeCheck.Decl.Data |
| DataBody | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| DataBody' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| dataBodyParts | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DataCompute | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| dataConFieldPats | Rzk.TypeCheck.Decl.Data |
| dataConFields | Rzk.TypeCheck.Decl.Data |
| DataConKind | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| dataConLocalNames | Rzk.TypeCheck.Decl.Data |
| dataConName | Rzk.TypeCheck.Decl.Data |
| dataConNonRec | Rzk.TypeCheck.Decl.Data |
| DataConPath | Rzk.TypeCheck.Decl.Data |
| DataConPoint | Rzk.TypeCheck.Decl.Data |
| dataConProbe | Rzk.TypeCheck.Decl.Data |
| dataConRecursive | Rzk.TypeCheck.Decl.Data |
| dataConRetIndices | Rzk.TypeCheck.Decl.Data |
| DataConSort | Rzk.TypeCheck.Decl.Data |
| dataConSort | Rzk.TypeCheck.Decl.Data |
| dataConstructorsOf | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| DataConSurface | |
| 1 (Type/Class) | Rzk.TypeCheck.Decl.Data |
| 2 (Data Constructor) | Rzk.TypeCheck.Decl.Data |
| dataConSurface | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| dataConType | Rzk.TypeCheck.Decl.Data |
| DataElim | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| DataElim' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| dataEliminatorsOf | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| DataElimKind | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| dataFieldToParamDecl | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| dataParamVars | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DataRole | |
| 1 (Type/Class) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| dataRoleDataType | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| DataRoleKind | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| dataRoleKind | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| dataRoleNumParams | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| DataSort | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| DataSort' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| dataSortIndices | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| Debug | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Decl | |
| 1 (Type/Class) | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declBinderTypes | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| declIsAssumption | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclKind | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclKindData | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclKindDataCon | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclKindDataElim | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclKindDefine | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclKindPostulate | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declLocation | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declName | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declNameOf | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declType | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclUsedVars | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| declUsedVars | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclUsedVars' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| declValue | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| DeclView | |
| 1 (Type/Class) | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declViewIsAssumption | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declViewKind | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declViewLocation | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declViewName | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declViews | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| declViewType | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| defaultCamera | Rzk.Render.Geometry |
| defaultRzkEnv | Language.Rzk.VSCode.Env |
| defaultVarIdents | Language.Rzk.Foil.Names |
| Definitive | Language.Rzk.Syntax.Layout |
| delimClose | Language.Rzk.Syntax.Layout |
| delimOpen | Language.Rzk.Syntax.Layout |
| delimSep | Language.Rzk.Syntax.Layout |
| destructuringBinder | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| desugarTuple | Language.Rzk.Foil.Names |
| diagnoseCheckWarning | Rzk.Diagnostic |
| diagnoseHole | Rzk.Diagnostic |
| diagnoseTypeError | Rzk.Diagnostic |
| Diagnostic | |
| 1 (Type/Class) | Rzk.Diagnostic |
| 2 (Data Constructor) | Rzk.Diagnostic |
| diagnosticCode | Rzk.Diagnostic |
| diagnosticHole | Rzk.Diagnostic |
| diagnosticLocation | Rzk.Diagnostic |
| diagnosticMessage | Rzk.Diagnostic |
| diagnosticSeverity | Rzk.Diagnostic |
| dimOf | Rzk.TypeCheck.Render |
| discreteAxiomOf | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| Display | Language.Rzk.Foil.Names |
| displayNameOf | Language.Rzk.Foil.Print |
| displayOf | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| Doc | Language.Rzk.Syntax.Print |
| doc | Language.Rzk.Syntax.Print |
| doesShadowName | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| domainEntails | Rzk.TypeCheck.Unify |
| DontKnow | Rzk.TypeCheck.NbE |
| drawCube | Rzk.TypeCheck.Render |
| duplicateBinders | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| Edge3D | Rzk.Render.Geometry |
| edges | Rzk.Render.Geometry |
| eitherResIdent | Language.Rzk.Syntax.Lex |
| elaborate | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| elaborateUnder | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| elemModalTope | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| elemName | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| elemT | Language.Rzk.Foil.Syntax |
| ElimCost | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| eliminatorsOf | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| ElimInd | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ElimKind | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ElimRec | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ElimSpec | |
| 1 (Type/Class) | Rzk.TypeCheck.Decl.Data |
| 2 (Data Constructor) | Rzk.TypeCheck.Decl.Data |
| ElimTerms | |
| 1 (Type/Class) | Rzk.TypeCheck.Decl.Data |
| 2 (Data Constructor) | Rzk.TypeCheck.Decl.Data |
| elimTerms | Rzk.TypeCheck.Decl.Data |
| emptyChecked | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| emptyCheckedWithHoles | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| emptyCheckLog | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| emptyContext | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| emptyReferenceIndexCache | Language.Rzk.VSCode.Env |
| emptyTopeContext | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| endpointsAgree | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| endSection | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| entailContextM | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| entailM | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| entailSaturatedM | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| enterBinder | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| enterModality | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| Env | Language.Rzk.Foil.Convert |
| eqModalTope | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| eqT | Language.Rzk.Foil.Syntax |
| Err | Language.Rzk.Syntax.Lex |
| esConsData | Rzk.TypeCheck.Decl.Data |
| esEndpointV | Rzk.TypeCheck.Decl.Data |
| esIhNames | Rzk.TypeCheck.Decl.Data |
| esIndexDecls | Rzk.TypeCheck.Decl.Data |
| esIndexVars | Rzk.TypeCheck.Decl.Data |
| esMethodVars | Rzk.TypeCheck.Decl.Data |
| esMotiveV | Rzk.TypeCheck.Decl.Data |
| esName | Rzk.TypeCheck.Decl.Data |
| esParamDecls | Rzk.TypeCheck.Decl.Data |
| esParamVars | Rzk.TypeCheck.Decl.Data |
| esPathData | Rzk.TypeCheck.Decl.Data |
| esPathV | Rzk.TypeCheck.Decl.Data |
| esScrutV | Rzk.TypeCheck.Decl.Data |
| esTransportV | Rzk.TypeCheck.Decl.Data |
| etaExpand | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| etaMatch | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| exclude | Rzk.Project.Config |
| expandRzkPathsOrYaml | Rzk.Main |
| Explicit | Language.Rzk.Syntax.Layout |
| extractFilesFromRzkYaml | Rzk.Main |
| extractMarkdownCodeBlocks | Language.Rzk.Syntax |
| Face3D | Rzk.Render.Geometry |
| faces | Rzk.Render.Geometry |
| fileOccurrences | Language.Rzk.VSCode.ReferenceIndex |
| filterAccessible | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| findDefinition | Language.Rzk.VSCode.Handlers |
| findReferences | Language.Rzk.VSCode.Handlers |
| First | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| firstDuplicate | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| FirstF | Language.Rzk.Foil.Syntax |
| firstMatching | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| FirstT | Language.Rzk.Foil.Syntax |
| firstT | Language.Rzk.Foil.Syntax |
| fitsInto | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| FlagOff | Rzk.Version |
| FlagOn | Rzk.Version |
| FlagState | Rzk.Version |
| Flat | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Names |
| flattenBinderApp | Language.Rzk.Foil.Names |
| format | Rzk.Format |
| formatDocument | |
| 1 (Function) | Rzk.Format |
| 2 (Function) | Language.Rzk.VSCode.Handlers |
| formatEnabled | Language.Rzk.VSCode.Config |
| formatFile | Rzk.Format |
| formatFileWrite | Rzk.Format |
| formatSignature | Language.Rzk.VSCode.Handlers |
| formatTextEdits | Rzk.Format |
| FormattingEdit | |
| 1 (Type/Class) | Rzk.Format |
| 2 (Data Constructor) | Rzk.Format |
| freeVarsDeep | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| freeVarsOfTerm | Language.Rzk.Foil.Syntax |
| freeVarsOfTermT | Language.Rzk.Foil.Syntax |
| freshenBinder | Language.Rzk.Foil.Print |
| freshenBinderLeaves | Language.Rzk.Foil.Names |
| freshenBinderLeavesIn | Language.Rzk.Foil.Names |
| freshIdent | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| freshIdents | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| fromAffine | Rzk.Render.Geometry |
| fromMod | Language.Rzk.Foil.Names |
| fromTerm | Language.Rzk.Foil.Print |
| fromTermClosed | Language.Rzk.Foil.Print |
| fromTModalityToModalColon | Language.Rzk.Foil.Names |
| fromVarIdent | Language.Rzk.Foil.Names |
| generateTopes | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| generateTopesForPointsM | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| getCachedReferenceIndex | Language.Rzk.VSCode.Env |
| getCachedTypecheckedModules | Language.Rzk.VSCode.Env |
| getRendered | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| getVarIdent | Language.Rzk.Foil.Names |
| globNonEmpty | Rzk.Main |
| handleFilesChanged | Language.Rzk.VSCode.Handlers |
| handlers | Language.Rzk.VSCode.Lsp |
| happyError | Language.Rzk.Syntax.Par |
| HasPosition | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| hasPosition | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| hideTermData | Rzk.Render.Geometry |
| hidingTerm | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| Hole | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| holeCandidates | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeCubeVars | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| HoleData | |
| 1 (Type/Class) | Rzk.Diagnostic |
| 2 (Data Constructor) | Rzk.Diagnostic |
| holeData | Rzk.Diagnostic |
| holeDataCubeVars | Rzk.Diagnostic |
| holeDataGoal | Rzk.Diagnostic |
| holeDataName | Rzk.Diagnostic |
| holeDataShape | Rzk.Diagnostic |
| holeDataTermVars | Rzk.Diagnostic |
| holeDataTopes | Rzk.Diagnostic |
| holeDiagram | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| HoleEntry | |
| 1 (Type/Class) | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeEntryName | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeEntryType | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| HoleF | Language.Rzk.Foil.Syntax |
| holeGoal | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeGoalShape | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| HoleIdent | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| HoleIdent' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| HoleIdentToken | |
| 1 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| holeIdentToken | Language.Rzk.Foil.Names |
| HoleInfo | |
| 1 (Type/Class) | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeIntroductions | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeLocation | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeName | |
| 1 (Function) | Language.Rzk.Foil.Names |
| 2 (Function) | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeNamesOf | Language.Rzk.Foil.Syntax |
| HoleT | Language.Rzk.Foil.Syntax |
| holeT | Language.Rzk.Foil.Syntax |
| holeTermVars | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| holeTopes | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| Id | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Names |
| iden | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| identTokenOf | Rzk.TypeCheck.Decl.Data |
| IdJ | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| IdJF | Language.Rzk.Foil.Syntax |
| IdJT | Language.Rzk.Foil.Syntax |
| idJT | Language.Rzk.Foil.Syntax |
| Implicit | Language.Rzk.Syntax.Layout |
| inAllSubContexts | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| incIndex | Language.Rzk.Foil.Names |
| include | Rzk.Project.Config |
| inContext | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| inCubeLayer | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| incVarIdentIndex | Language.Rzk.Foil.Names |
| indentation | Language.Rzk.Syntax.Layout |
| indexCacheModules | Language.Rzk.VSCode.Env |
| indexCacheResult | Language.Rzk.VSCode.Env |
| indexModules | Language.Rzk.VSCode.ReferenceIndex |
| indTypeTerm | Rzk.TypeCheck.Decl.Data |
| infer | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| inferAs | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| infoNF | Language.Rzk.Foil.Names |
| infoOfVar | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| infoType | Language.Rzk.Foil.Names |
| infoWHNF | Language.Rzk.Foil.Names |
| inScope | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| inScope2 | Rzk.TypeCheck.Unify |
| inScopeMaybeTope | Rzk.TypeCheck.Render |
| inScopeWith | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| insertVarInfo | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| instantiate | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| instantiateT | Language.Rzk.Foil.Syntax |
| instantiateUntyped | Language.Rzk.Foil.Syntax |
| inTopeLayer | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| Invariant | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| isAccessible | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| isAnonymous | Rzk.TypeCheck.Render |
| isCubeOrTopeType | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| isCubeType | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| isHoleHeadedT | Language.Rzk.Foil.Syntax |
| isHoleT | Language.Rzk.Foil.Syntax |
| isImplicit | Language.Rzk.Syntax.Layout |
| isLatticePoint | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| isLayout | Language.Rzk.Syntax.Layout |
| isLayoutClose | Language.Rzk.Syntax.Layout |
| isLayoutOpen | Language.Rzk.Syntax.Layout |
| isLayoutSep | Language.Rzk.Syntax.Layout |
| isMetaType | Rzk.TypeCheck.MetaPrefix |
| isoCommitDate | Rzk.Version |
| isParenClose | Language.Rzk.Syntax.Layout |
| isParenOpen | Language.Rzk.Syntax.Layout |
| isRA | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| isStop | Language.Rzk.Syntax.Layout |
| issueTypeError | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| issueWarning | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| isTokenIn | Language.Rzk.Syntax.Layout |
| isTopLevelVar | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| isWellFormatted | Rzk.Format |
| isWellFormattedFile | Rzk.Format |
| Lambda | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| LambdaF | Language.Rzk.Foil.Syntax |
| lambdaHoleOf | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| LambdaParam | |
| 1 (Type/Class) | Language.Rzk.Foil.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| LambdaT | Language.Rzk.Foil.Syntax |
| lambdaT | Language.Rzk.Foil.Syntax |
| Language | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Language' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| LanguageDecl | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| LanguageDecl' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| LargeInductiveTypeWarning | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| layoutClose | Language.Rzk.Syntax.Layout |
| LayoutDelimiters | |
| 1 (Type/Class) | Language.Rzk.Syntax.Layout |
| 2 (Data Constructor) | Language.Rzk.Syntax.Layout |
| layoutError | Language.Rzk.Syntax.Layout |
| layoutOpen | Language.Rzk.Syntax.Layout |
| layoutSep | Language.Rzk.Syntax.Layout |
| layoutStopWords | Language.Rzk.Syntax.Layout |
| layoutWords | Language.Rzk.Syntax.Layout |
| lemmaHypotheses | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| Let | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| LetF | Language.Rzk.Foil.Syntax |
| LetMod | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| LetModBind | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| LetModBindInto | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| LetModF | Language.Rzk.Foil.Syntax |
| LetModFramed | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| LetModFramedInto | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| LetModInto | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| LetModT | Language.Rzk.Foil.Syntax |
| letModT | Language.Rzk.Foil.Syntax |
| LetT | Language.Rzk.Foil.Syntax |
| letT | Language.Rzk.Foil.Syntax |
| limitLength | Rzk.Render.Geometry |
| Line | Language.Rzk.Syntax.Layout |
| line | Language.Rzk.Syntax.Layout |
| localHideTerm | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| localHypotheses | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| localMetaPrefixSensitivity | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| localRenderBackend | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| localTope | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| localVerbosity | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| localWarnOverhang | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| Location | |
| 1 (Type/Class) | Language.Rzk.VSCode.ReferenceIndex |
| 2 (Data Constructor) | Language.Rzk.VSCode.ReferenceIndex |
| locationColumn | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| locationFilePath | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| LocationInfo | |
| 1 (Type/Class) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| locationLine | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| locationOfTypeError | Rzk.Diagnostic |
| locationPath | Language.Rzk.VSCode.ReferenceIndex |
| locationRange | Language.Rzk.VSCode.ReferenceIndex |
| locationToJSON | Rzk.Diagnostic |
| locationUri | Language.Rzk.VSCode.ReferenceIndex |
| locksOfVar | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| logDebug | Language.Rzk.VSCode.Logging |
| logError | Language.Rzk.VSCode.Logging |
| logHolesRev | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| logInfo | Language.Rzk.VSCode.Logging |
| logWarning | Language.Rzk.VSCode.Logging |
| logWarningsRev | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| lookupAt | Language.Rzk.VSCode.ReferenceIndex |
| lookupNamed | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| lookupVarInfo | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| LSP | Language.Rzk.VSCode.Env |
| makeAssumptionExplicit | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| mapNameMap | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| markUnresolved | Language.Rzk.Foil.Names |
| Match | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| MatchArm | Language.Rzk.Foil.Syntax |
| MatchArmF | Language.Rzk.Foil.Syntax |
| matchArms | Language.Rzk.Foil.Print |
| MatchArmT | Language.Rzk.Foil.Syntax |
| MatchBranch | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| MatchBranch' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| matchBranchNoParams | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| matchesDataApplied | Rzk.TypeCheck.Decl.Data |
| MatchF | Language.Rzk.Foil.Syntax |
| matchHoleOf | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| MatchInd | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| MatchInto | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| MatchPlan | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| MatchRec | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| MatchT | Language.Rzk.Foil.Syntax |
| Matrix3D | |
| 1 (Type/Class) | Rzk.Render.Geometry |
| 2 (Data Constructor) | Rzk.Render.Geometry |
| matrix3Dto4D | Rzk.Render.Geometry |
| Matrix4D | |
| 1 (Type/Class) | Rzk.Render.Geometry |
| 2 (Data Constructor) | Rzk.Render.Geometry |
| matrixVectorMult4D | Rzk.Render.Geometry |
| maxActionStackDepth | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| maxDiagnosticCount | Language.Rzk.VSCode.Lsp |
| maxEliminationDepth | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| maxRenderDim | Rzk.TypeCheck.Render |
| memoizeWHNF | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| memoWHNF | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| mergeTokens | Language.Rzk.VSCode.Tokenize |
| MetaPrefixBoth | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| metaPrefixOf | Rzk.TypeCheck.MetaPrefix |
| MetaPrefixOff | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| MetaPrefixRule | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| MetaPrefixSensitivity | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| MetaPrefixStrict | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| MetaPrefixStrictOnly | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| MetaPrefixStructural | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| MetaPrefixWarning | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| mkEsc | Language.Rzk.Syntax.Print |
| mkHole | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| mkNamedHole | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| mkPosToken | Language.Rzk.Syntax.Lex |
| mkToken | Language.Rzk.VSCode.Tokenize |
| ModalColon | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ModalColon' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ModalColonFlat | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ModalColonId | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| modalColonModality | Language.Rzk.Foil.Names |
| ModalColonOp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ModalColonSharp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| modalColonToTModality | Language.Rzk.Foil.Names |
| modalFieldError | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| Modality | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Modality' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| modalityOfVar | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| ModalTope | |
| 1 (Type/Class) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ModApp | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| ModAppF | Language.Rzk.Foil.Syntax |
| ModAppT | Language.Rzk.Foil.Syntax |
| modAppT | Language.Rzk.Foil.Syntax |
| ModComp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ModComp' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ModeTheory | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ModExtract | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| ModExtractF | Language.Rzk.Foil.Syntax |
| ModExtractT | Language.Rzk.Foil.Syntax |
| modExtractT | Language.Rzk.Foil.Syntax |
| modifyLog | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| ModType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Module | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Module' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| motiveFromGoal | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| motiveOf | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| motiveType | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| myLexer | Language.Rzk.Syntax.Par |
| N | Language.Rzk.Syntax.Lex |
| namedBlock | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| nameIdsOf | Language.Rzk.Foil.Print |
| Naming | |
| 1 (Type/Class) | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| namingOf | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| namingOfContext | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| namingSupply | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| namingUsed | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| narrowLocation | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| nbeConvertible | Rzk.TypeCheck.NbE |
| newLine | Language.Rzk.Syntax.Layout |
| nextPos | Language.Rzk.Syntax.Layout |
| nfInfT | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| nfSupT | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| nfT | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| nfTope | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| NoConstructorType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| NoDataBody | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| NoDataSort | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| noDeclUsedVars | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Normal | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| normalizeTabs | Rzk.Format |
| NoSectionName | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| noSrcPos | Language.Rzk.Foil.Syntax |
| notElemName | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| notElemT | Language.Rzk.Foil.Syntax |
| nthByConstruction | Rzk.TypeCheck.Decl.Data |
| nubModalTopes | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| nubNames | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| nubOrd | Language.Rzk.Foil.Convert |
| nubT | Language.Rzk.Foil.Syntax |
| occurrences | Language.Rzk.VSCode.ReferenceIndex |
| Op | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Names |
| openScoped | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| openWith | Language.Rzk.Foil.Syntax |
| OutputDirection | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| Pair | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| pairEtaCollapse | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| PairF | Language.Rzk.Foil.Syntax |
| PairT | Language.Rzk.Foil.Syntax |
| pairT | Language.Rzk.Foil.Syntax |
| panicImpossible | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| Param | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Param' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamDecl | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamDecl' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamPattern | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamPatternModalShape | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamPatternModalType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamPatternShape | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamPatternType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamTermModalShape | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamTermModalType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamTermShape | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamTermType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| paramToParamDecl | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| ParamType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| parenClose | Language.Rzk.Syntax.Layout |
| parenOpen | Language.Rzk.Syntax.Layout |
| parenth | Language.Rzk.Syntax.Print |
| ParsedFromBuffer | Language.Rzk.VSCode.Env |
| ParsedFromDisk | Language.Rzk.VSCode.Env |
| ParsedModule | |
| 1 (Type/Class) | Language.Rzk.VSCode.Env |
| 2 (Data Constructor) | Language.Rzk.VSCode.Env |
| parsedModule | Language.Rzk.VSCode.Env |
| parsedSource | Language.Rzk.VSCode.Env |
| ParseInvalidated | Language.Rzk.VSCode.Env |
| parseModule | Language.Rzk.Syntax |
| parseModuleFile | Language.Rzk.Syntax |
| parseModuleRzk | Language.Rzk.Syntax |
| parseModuleSafe | Language.Rzk.Syntax |
| parseRzkFilesOrStdin | Rzk.Main |
| parsesBackTo | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| ParseSource | Language.Rzk.VSCode.Env |
| parseStdin | Rzk.Main |
| parseTerm | Language.Rzk.Syntax |
| partitionAccessible | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| PathCon | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Pattern | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Pattern' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| PatternPair | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| patternToTerm | Language.Rzk.Foil.Names |
| PatternTuple | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| PatternUnit | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| PatternVar | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| pBind | Language.Rzk.Syntax.Par |
| pCommand | Language.Rzk.Syntax.Par |
| pConstructor | Language.Rzk.Syntax.Par |
| pConstructorType | Language.Rzk.Syntax.Par |
| pDataBody | Language.Rzk.Syntax.Par |
| pDataElim | Language.Rzk.Syntax.Par |
| pDataSort | Language.Rzk.Syntax.Par |
| pDeclUsedVars | Language.Rzk.Syntax.Par |
| peelLambdas | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| performing | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| PFst | Language.Rzk.Foil.Names |
| pHoleIdent | Language.Rzk.Syntax.Par |
| plainTope | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| pLanguage | Language.Rzk.Syntax.Par |
| pLanguageDecl | Language.Rzk.Syntax.Par |
| pListCommand | Language.Rzk.Syntax.Par |
| pListConstructor | Language.Rzk.Syntax.Par |
| pListDataElim | Language.Rzk.Syntax.Par |
| pListMatchBranch | Language.Rzk.Syntax.Par |
| pListParam | Language.Rzk.Syntax.Par |
| pListPattern | Language.Rzk.Syntax.Par |
| pListPattern1 | Language.Rzk.Syntax.Par |
| pListRestriction | Language.Rzk.Syntax.Par |
| pListSigmaParam | Language.Rzk.Syntax.Par |
| pListTerm | Language.Rzk.Syntax.Par |
| pListVarIdent | Language.Rzk.Syntax.Par |
| pMatchBranch | Language.Rzk.Syntax.Par |
| pModalColon | Language.Rzk.Syntax.Par |
| pModality | Language.Rzk.Syntax.Par |
| pModComp | Language.Rzk.Syntax.Par |
| pModule | Language.Rzk.Syntax.Par |
| Pn | Language.Rzk.Syntax.Lex |
| Point2D | Rzk.Render.Geometry |
| Point3D | Rzk.Render.Geometry |
| point3Dto2D | Rzk.Render.Geometry |
| PointCon | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| PointId | Rzk.Render.Geometry |
| Position | |
| 1 (Type/Class) | Language.Rzk.Syntax.Layout |
| 2 (Type/Class) | Language.Rzk.VSCode.ReferenceIndex |
| 3 (Data Constructor) | Language.Rzk.VSCode.ReferenceIndex |
| positionCharacter | Language.Rzk.VSCode.ReferenceIndex |
| positionFromUtf16 | Language.Rzk.VSCode.PositionEncoding |
| positionLine | Language.Rzk.VSCode.ReferenceIndex |
| positionOfTerm | Language.Rzk.Foil.Syntax |
| positionTable | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| posLineCol | Language.Rzk.Syntax.Lex |
| Posn | Language.Rzk.Syntax.Lex |
| ppAction | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| pParam | Language.Rzk.Syntax.Par |
| pParamDecl | Language.Rzk.Syntax.Par |
| pPattern | Language.Rzk.Syntax.Par |
| pPattern1 | Language.Rzk.Syntax.Par |
| ppCheckWarning | Rzk.Diagnostic |
| ppContext | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| ppHoleInfo | Rzk.Diagnostic |
| ppInContext | Rzk.TypeCheck.Render |
| ppLocationInfo | Rzk.Diagnostic |
| ppModality | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| ppName | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| ppRzkPosition | Language.Rzk.Foil.Names |
| ppTerm | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| ppTermT | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| ppTypeError | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| ppTypeErrorInScopedContext | Rzk.TypeCheck.Error, Rzk.TypeCheck |
| ppVarIdentWithLocation | Language.Rzk.Foil.Names |
| ppVersionInfo | Rzk.Version |
| prefixedIdent | Rzk.TypeCheck.Decl.Data |
| pRestriction | Language.Rzk.Syntax.Par |
| Print | Language.Rzk.Syntax.Print, Language.Rzk.Syntax |
| printPosn | Language.Rzk.Syntax.Lex |
| printString | Language.Rzk.Syntax.Print |
| printTree | |
| 1 (Function) | Language.Rzk.Syntax.Print |
| 2 (Function) | Language.Rzk.Syntax |
| Proj | Language.Rzk.Foil.Names |
| project2D | Rzk.Render.Geometry |
| ProjectConfig | |
| 1 (Type/Class) | Rzk.Project.Config |
| 2 (Data Constructor) | Rzk.Project.Config |
| provideCompletions | Language.Rzk.VSCode.Handlers |
| provideHover | Language.Rzk.VSCode.Handlers |
| provideSemanticTokens | Language.Rzk.VSCode.Handlers |
| provideSymbols | Language.Rzk.VSCode.Handlers |
| provideWorkspaceSymbols | Language.Rzk.VSCode.Handlers |
| prPrec | Language.Rzk.Syntax.Print |
| prt | Language.Rzk.Syntax.Print, Language.Rzk.Syntax |
| prToken | Language.Rzk.Syntax.Lex |
| pruneVacuousFaces | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| pSectionName | Language.Rzk.Syntax.Par |
| pSigmaParam | Language.Rzk.Syntax.Par |
| PSnd | Language.Rzk.Foil.Names |
| PT | Language.Rzk.Syntax.Lex |
| pTerm | Language.Rzk.Syntax.Par |
| pTerm1 | Language.Rzk.Syntax.Par |
| pTerm2 | Language.Rzk.Syntax.Par |
| pTerm3 | Language.Rzk.Syntax.Par |
| pTerm4 | Language.Rzk.Syntax.Par |
| pTerm5 | Language.Rzk.Syntax.Par |
| pTerm6 | Language.Rzk.Syntax.Par |
| pTerm7 | Language.Rzk.Syntax.Par |
| pVarIdent | Language.Rzk.Syntax.Par |
| quickIndex | Language.Rzk.Syntax.Lex |
| Range | |
| 1 (Type/Class) | Language.Rzk.VSCode.ReferenceIndex |
| 2 (Data Constructor) | Language.Rzk.VSCode.ReferenceIndex |
| rangeEnd | Language.Rzk.VSCode.ReferenceIndex |
| rangeStart | Language.Rzk.VSCode.ReferenceIndex |
| rangeToUtf16 | Language.Rzk.VSCode.PositionEncoding |
| RecBottom | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| recBottomCandidates | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| RecBottomF | Language.Rzk.Foil.Syntax |
| RecBottomT | Language.Rzk.Foil.Syntax |
| recBottomT | Language.Rzk.Foil.Syntax |
| recheckFrom | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| RecOr | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| recOrCandidates | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| recordCheckWarning | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| recordHole | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| recordHoleInfo | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| recordHoleShape | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| recordInSection | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| recordMetaPrefixUses | Rzk.TypeCheck.MetaPrefix |
| RecOrF | Language.Rzk.Foil.Syntax |
| RecOrT | Language.Rzk.Foil.Syntax |
| recOrT | Language.Rzk.Foil.Syntax |
| recPositionsOf | Rzk.TypeCheck.Decl.Data |
| recTypeTerm | Rzk.TypeCheck.Decl.Data |
| ReferenceIndex | |
| 1 (Type/Class) | Language.Rzk.VSCode.ReferenceIndex |
| 2 (Data Constructor) | Language.Rzk.VSCode.ReferenceIndex |
| ReferenceIndexCache | |
| 1 (Type/Class) | Language.Rzk.VSCode.Env |
| 2 (Data Constructor) | Language.Rzk.VSCode.Env |
| Refl | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| ReflF | Language.Rzk.Foil.Syntax |
| ReflT | Language.Rzk.Foil.Syntax |
| reflT | Language.Rzk.Foil.Syntax |
| ReflTerm | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ReflTermType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| refreshVar | Language.Rzk.Foil.Names |
| refreshVarIn | Language.Rzk.Foil.Names |
| render | Language.Rzk.Syntax.Print |
| renderApplied | Rzk.TypeCheck.Render |
| RenderBackend | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| renderCube | Rzk.Render.Geometry |
| Rendered | |
| 1 (Type/Class) | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| renderForSubShapeSVG | Rzk.TypeCheck.Render |
| renderForSVG | Rzk.TypeCheck.Render |
| renderGoalCellSVG | Rzk.TypeCheck.Render |
| renderHere | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| RenderLaTeX | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| RenderObjectData | |
| 1 (Type/Class) | Rzk.Render.Geometry |
| 2 (Data Constructor) | Rzk.Render.Geometry |
| renderObjectDataColor | Rzk.Render.Geometry |
| renderObjectDataFullLabel | Rzk.Render.Geometry |
| renderObjectDataLabel | Rzk.Render.Geometry |
| renderObjectsFor | Rzk.TypeCheck.Render |
| renderObjectsInSubShapeFor | Rzk.TypeCheck.Render |
| RenderSVG | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| renderTerm | Rzk.TypeCheck.Display, Rzk.TypeCheck |
| renderTermSVG | Rzk.TypeCheck.Render |
| renderTermSVG' | Rzk.TypeCheck.Render |
| renderTermSVGFor | Rzk.TypeCheck.Render |
| replicateS | Language.Rzk.Syntax.Print |
| resetCacheForAllFiles | Language.Rzk.VSCode.Env |
| resetCacheForFiles | Language.Rzk.VSCode.Env |
| resolveLayout | |
| 1 (Function) | Language.Rzk.Syntax.Layout |
| 2 (Function) | Language.Rzk.Syntax |
| Restriction | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Restriction' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| resWords | Language.Rzk.Syntax.Lex |
| rotateX | Rzk.Render.Geometry |
| rotateY | Rzk.Render.Geometry |
| rotateZ | Rzk.Render.Geometry |
| runLsp | Language.Rzk.VSCode.Lsp |
| runTypeCheck | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| runTypeCheckIn | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| runTypeCheckWith | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| Rzk1 | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| RzkCachedModule | |
| 1 (Type/Class) | Language.Rzk.VSCode.Env |
| 2 (Data Constructor) | Language.Rzk.VSCode.Env |
| RzkEnv | |
| 1 (Type/Class) | Language.Rzk.VSCode.Env |
| 2 (Data Constructor) | Language.Rzk.VSCode.Env |
| rzkEnvReferenceIndexCache | Language.Rzk.VSCode.Env |
| rzkEnvTypecheckCache | Language.Rzk.VSCode.Env |
| rzkEnvTypecheckWorker | Language.Rzk.VSCode.Env |
| rzkFilePath | Language.Rzk.Foil.Names |
| rzkLineCol | Language.Rzk.Foil.Names |
| RzkPosition | |
| 1 (Type/Class) | Language.Rzk.Foil.Names |
| 2 (Data Constructor) | Language.Rzk.Foil.Names |
| RzkTypecheckCache | Language.Rzk.VSCode.Env |
| saturateBottom | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| saturateForEntailment | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| saturateInv | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| saturateTopes | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| saturateWith | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| saturateWithHoles | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| SaturationCached | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| SaturationUncached | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ScopedTerm | Language.Rzk.Foil.Syntax |
| ScopedTermT | Language.Rzk.Foil.Syntax |
| scopeUsesItsBinder | Language.Rzk.Foil.Print |
| Second | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| SecondF | Language.Rzk.Foil.Syntax |
| SecondT | Language.Rzk.Foil.Syntax |
| secondT | Language.Rzk.Foil.Syntax |
| sectionEntries | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| SectionInfo | |
| 1 (Type/Class) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| SectionName | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| sectionName | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| SectionName' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ServerConfig | |
| 1 (Type/Class) | Language.Rzk.VSCode.Config |
| 2 (Data Constructor) | Language.Rzk.VSCode.Config |
| setOption | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| setVariance | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| Severity | Rzk.Diagnostic |
| SeverityError | Rzk.Diagnostic |
| SeverityHint | Rzk.Diagnostic |
| SeverityInformation | Rzk.Diagnostic |
| SeverityWarning | Rzk.Diagnostic |
| shadowedBy | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| ShapeId | Rzk.Render.Geometry |
| ShapeView | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| Sharp | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Names |
| SigmaParam | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| SigmaParam' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| SigmaParamModal | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| sigmaParamToTypeSigma | Language.Rzk.Foil.Names |
| Silent | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| simplifyLHSwithDisjunctions | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| Single | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| sinkBound | Language.Rzk.Foil.Convert |
| sinkContextUnchecked | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| sinkDecl | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| sinkDeclGroups | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| sinkDecls | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| sinkNamed | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| sinkNames | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| sinkTopes | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| sinkVars | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| skippingCommand | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| solveRHS | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| solveRHSM | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| SomeConstructorType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| SomeDataBody | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| SomeDataSort | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| SomeSectionName | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| SortIndex | |
| 1 (Type/Class) | Rzk.TypeCheck.Decl.Data |
| 2 (Data Constructor) | Rzk.TypeCheck.Decl.Data |
| sortIndexType | Rzk.TypeCheck.Decl.Data |
| sortIndexVar | Rzk.TypeCheck.Decl.Data |
| sourceResolvesTo | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| spawnTypecheckWorker | Language.Rzk.VSCode.Env |
| SpineStep | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| splits | Rzk.TypeCheck.Render |
| splitSectionCommands | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| splitViewM | Rzk.TypeCheck.BinderTypes, Rzk.TypeCheck |
| SrcPos | |
| 1 (Type/Class) | Language.Rzk.Foil.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| startSection | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| Status | Language.Rzk.Syntax.Layout |
| sToken | Language.Rzk.Syntax.Layout |
| stripTypeRestrictions | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| structuralHoleUnify | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| subPoints | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| substituteName | Language.Rzk.Foil.Syntax |
| substituteT | Language.Rzk.Foil.Syntax |
| subTopes2 | Rzk.TypeCheck.Render |
| suppressing | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| surfaceApps | Rzk.TypeCheck.Decl.Data |
| surfaceAppSpine | Rzk.TypeCheck.Decl.Data |
| surfaceArrow | Rzk.TypeCheck.Decl.Data |
| surfaceLambda | Rzk.TypeCheck.Decl.Data |
| surfacePatternVars | Rzk.TypeCheck.Decl.Data |
| surfacePi | Rzk.TypeCheck.Decl.Data |
| surfacePiSpine | Rzk.TypeCheck.Decl.Data |
| surfaceVar | Rzk.TypeCheck.Decl.Data |
| surfaceVarTokens | Rzk.TypeCheck.Decl.Data |
| switchVariance | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| syncOptions | Language.Rzk.VSCode.Lsp |
| 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 |
| underBinder | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| underScope | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| underScope2 | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| underscoreIdent | Rzk.TypeCheck.Decl.Data |
| unescapeInitTail | Language.Rzk.Syntax.Lex |
| unicode_TypeSigmaAlt | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| unicode_TypeSigmaTupleAlt | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| unify | Rzk.TypeCheck.Unify |
| unifyInCurrentContext | Rzk.TypeCheck.Unify |
| unifyTerms | Rzk.TypeCheck.Unify |
| unifyTopes | Rzk.TypeCheck.Unify |
| unifyTypes | Rzk.TypeCheck.Unify |
| unifyViaDecompose | Rzk.TypeCheck.Unify |
| Unit | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| UnitF | Language.Rzk.Foil.Syntax |
| unitPointCollapse | Rzk.TypeCheck.Judgements, Rzk.TypeCheck |
| UnitT | Language.Rzk.Foil.Syntax |
| unitT | Language.Rzk.Foil.Syntax |
| Universe | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| UniverseCube | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| UniverseCubeF | Language.Rzk.Foil.Syntax |
| UniverseCubeT | Language.Rzk.Foil.Syntax |
| UniverseF | Language.Rzk.Foil.Syntax |
| UniverseT | Language.Rzk.Foil.Syntax |
| universeT | Language.Rzk.Foil.Syntax |
| UniverseTope | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Foil.Syntax |
| UniverseTopeF | Language.Rzk.Foil.Syntax |
| UniverseTopeT | Language.Rzk.Foil.Syntax |
| unmarkUnresolved | Language.Rzk.Foil.Names |
| unsafeTermToPattern | Language.Rzk.Foil.Names |
| unsetOption | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| untyped | Language.Rzk.Foil.Syntax |
| UntypedNode | Language.Rzk.Foil.Syntax |
| Uri | |
| 1 (Type/Class) | Language.Rzk.VSCode.ReferenceIndex |
| 2 (Data Constructor) | Language.Rzk.VSCode.ReferenceIndex |
| uriPath | Language.Rzk.VSCode.ReferenceIndex |
| useSiteTokens | Language.Rzk.VSCode.Handlers |
| utf16Length | Language.Rzk.VSCode.PositionEncoding |
| utf8Encode | Language.Rzk.Syntax.Lex |
| valueInfo | Language.Rzk.Foil.Syntax |
| valueOfVar | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| Var | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| varDataRole | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varDeclaredAssumptions | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| VarIdent | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 3 (Type/Class) | Language.Rzk.Foil.Names |
| 4 (Data Constructor) | Language.Rzk.Foil.Names |
| varIdent | Language.Rzk.Foil.Names |
| VarIdent' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| varIdentAt | Language.Rzk.Foil.Names |
| VarIdentToken | |
| 1 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| VarInfo | |
| 1 (Type/Class) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varInfos | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varIsAssumption | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varIsTopLevel | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varLocation | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varMetaPrefix | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varModAccum | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varModality | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varOrig | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varsInScope | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varType | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| varValue | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| Vector3D | |
| 1 (Type/Class) | Rzk.Render.Geometry |
| 2 (Data Constructor) | Rzk.Render.Geometry |
| Vector4D | |
| 1 (Type/Class) | Rzk.Render.Geometry |
| 2 (Data Constructor) | Rzk.Render.Geometry |
| Verbosity | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| version | Rzk.Version |
| VersionInfo | |
| 1 (Type/Class) | Rzk.Version |
| 2 (Data Constructor) | Rzk.Version |
| versionInfo | Rzk.Version |
| versionInfoCommit | Rzk.Version |
| versionInfoCommitDate | Rzk.Version |
| versionInfoCompiler | Rzk.Version |
| versionInfoFlags | Rzk.Version |
| versionInfoPlatform | Rzk.Version |
| versionInfoVersion | Rzk.Version |
| versionString | Rzk.Version |
| vertices | Rzk.Render.Geometry |
| verticesFrom | Rzk.TypeCheck.Render |
| viewRotateX | Rzk.Render.Geometry |
| viewRotateY | Rzk.Render.Geometry |
| viewTranslate | Rzk.Render.Geometry |
| Volume3D | Rzk.Render.Geometry |
| volumes | Rzk.Render.Geometry |
| warningLocation | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| whnfT | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| withBinder | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| withCommand | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| withDataDecls | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| withFreshBinder | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| withFreshIn | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| withHintLemmas | Rzk.TypeCheck.Context, Rzk.TypeCheck |
| withLocation | Rzk.TypeCheck.Monad, Rzk.TypeCheck |
| withOpenTerm | Language.Rzk.Foil.Convert |
| withRefreshedTopes | Rzk.TypeCheck.Eval, Rzk.TypeCheck |
| withScopedT | Language.Rzk.Foil.Syntax |
| withScopedT2 | Language.Rzk.Foil.Syntax |
| withSection | Rzk.TypeCheck.Decl, Rzk.TypeCheck |
| withTopLevel | Rzk.TypeCheck.Decl, Rzk.TypeCheck |