| :+: | Free.Scoped |
| abstract | Free.Scoped |
| abstractAssumption | Rzk.TypeCheck |
| accessibleTopes | Rzk.TypeCheck |
| Action | Rzk.TypeCheck |
| Action' | Rzk.TypeCheck |
| ActionCheckCoherence | Rzk.TypeCheck |
| ActionCheckLetValue | Rzk.TypeCheck |
| ActionCloseSection | Rzk.TypeCheck |
| ActionContextEntailedBy | Rzk.TypeCheck |
| ActionContextEntails | Rzk.TypeCheck |
| ActionContextEntailsUnion | Rzk.TypeCheck |
| ActionInfer | Rzk.TypeCheck |
| ActionNF | Rzk.TypeCheck |
| actionStack | Rzk.TypeCheck |
| ActionTypeCheck | Rzk.TypeCheck |
| ActionUnify | Rzk.TypeCheck |
| ActionUnifyTerms | Rzk.TypeCheck |
| ActionWHNF | Rzk.TypeCheck |
| addImplicit | Language.Rzk.Syntax.Layout |
| addModalityToScope | Rzk.TypeCheck |
| addParamDecls | Rzk.TypeCheck |
| addParams | Rzk.TypeCheck |
| addVarInCurrentScope | Rzk.TypeCheck |
| addVarToScope | 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 |
| allIntroductionsOf | Rzk.TypeCheck |
| allowHoles | Rzk.TypeCheck |
| allTopePoints | Rzk.TypeCheck |
| AnnF | |
| 1 (Type/Class) | Free.Scoped |
| 2 (Data Constructor) | Free.Scoped |
| annF | Free.Scoped |
| App | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| AppE | Language.Rzk.Free.Syntax |
| AppF | Language.Rzk.Free.Syntax |
| applyModality | Rzk.TypeCheck |
| applyModalityToScopes | Rzk.TypeCheck |
| applyModalityToTopes | Rzk.TypeCheck |
| AppT | Language.Rzk.Free.Syntax |
| appT | Rzk.TypeCheck |
| AppTE | Language.Rzk.Free.Syntax |
| 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_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_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_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_TypeExtensionDeprecated | 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 |
| askCurrentScope | Rzk.TypeCheck |
| availableTopes | Rzk.TypeCheck |
| availableTopesNF | Rzk.TypeCheck |
| B | Language.Rzk.Syntax.Lex |
| Bind | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Bind' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Binder | Language.Rzk.Free.Syntax |
| binderDisplayName | Language.Rzk.Free.Syntax |
| binderIsCompound | Language.Rzk.Free.Syntax |
| binderLeaves | Language.Rzk.Free.Syntax |
| binderName | Language.Rzk.Free.Syntax |
| BinderPair | Language.Rzk.Free.Syntax |
| binderPaths | Language.Rzk.Free.Syntax |
| binderProjMap | Rzk.TypeCheck |
| binderToPattern | Language.Rzk.Free.Syntax |
| binderToTerm | Language.Rzk.Free.Syntax |
| BinderUnit | Language.Rzk.Free.Syntax |
| BinderVar | Language.Rzk.Free.Syntax |
| BindPattern | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| BindPatternType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Block | Language.Rzk.Syntax.Layout |
| block | 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 |
| Branching | Rzk.TypeCheck |
| BTree | Language.Rzk.Syntax.Lex |
| Byte | Language.Rzk.Syntax.Lex |
| cachedModuleDecls | Language.Rzk.VSCode.Env |
| cachedModuleErrors | Language.Rzk.VSCode.Env |
| cacheTypecheckedModules | Language.Rzk.VSCode.Env |
| Camera | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| cameraAngleX | Rzk.TypeCheck |
| cameraAngleY | Rzk.TypeCheck |
| cameraAspectRatio | Rzk.TypeCheck |
| cameraFoV | Rzk.TypeCheck |
| cameraPos | Rzk.TypeCheck |
| checkCoherence | Rzk.TypeCheck |
| checkDefinedVar | Rzk.TypeCheck |
| checkEntails | Rzk.TypeCheck |
| checkHoleAgainstShape | Rzk.TypeCheck |
| checkNameShadowing | Rzk.TypeCheck |
| checkRecOrAgainst | Rzk.TypeCheck |
| checkTope | Rzk.TypeCheck |
| checkTopeAgainstContext | Rzk.TypeCheck |
| checkTopeEntails | Rzk.TypeCheck |
| checkTopLevelDuplicate | Rzk.TypeCheck |
| closeScope | Rzk.TypeCheck |
| coe | Rzk.TypeCheck |
| collectScopeDecls | Rzk.TypeCheck |
| 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 |
| 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 |
| componentWiseEQT | Rzk.TypeCheck |
| concatD | Language.Rzk.Syntax.Print |
| concatS | Language.Rzk.Syntax.Print |
| confirm | Language.Rzk.Syntax.Layout |
| containsHole | Rzk.TypeCheck |
| Context | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| contextBinders | Rzk.TypeCheck |
| contextEntails | Rzk.TypeCheck |
| contextEntailsBottom | Rzk.TypeCheck |
| contextEntailsUnion | Rzk.TypeCheck |
| Contravariant | Rzk.TypeCheck |
| countCommands | Rzk.TypeCheck |
| Covariance | Rzk.TypeCheck |
| covariance | Rzk.TypeCheck |
| Covariant | Rzk.TypeCheck |
| coverageHolds | Rzk.TypeCheck |
| Cube2 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| Cube2E | Language.Rzk.Free.Syntax |
| Cube2F | Language.Rzk.Free.Syntax |
| cube2powerT | Rzk.TypeCheck |
| Cube2T | Language.Rzk.Free.Syntax |
| cube2T | Rzk.TypeCheck |
| Cube2TE | Language.Rzk.Free.Syntax |
| Cube2_0 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| Cube2_0E | Language.Rzk.Free.Syntax |
| Cube2_0F | Language.Rzk.Free.Syntax |
| Cube2_0T | Language.Rzk.Free.Syntax |
| cube2_0T | Rzk.TypeCheck |
| Cube2_0TE | Language.Rzk.Free.Syntax |
| Cube2_1 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| Cube2_1E | Language.Rzk.Free.Syntax |
| Cube2_1F | Language.Rzk.Free.Syntax |
| Cube2_1T | Language.Rzk.Free.Syntax |
| cube2_1T | Rzk.TypeCheck |
| Cube2_1TE | Language.Rzk.Free.Syntax |
| CubeCoords2D | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| CubeFlip | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| CubeFlipE | Language.Rzk.Free.Syntax |
| CubeFlipF | Language.Rzk.Free.Syntax |
| CubeFlipT | Language.Rzk.Free.Syntax |
| cubeFlipT | Rzk.TypeCheck |
| CubeFlipTE | Language.Rzk.Free.Syntax |
| CubeI | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| CubeIE | Language.Rzk.Free.Syntax |
| CubeIF | Language.Rzk.Free.Syntax |
| CubeIT | Language.Rzk.Free.Syntax |
| cubeIT | Rzk.TypeCheck |
| CubeITE | Language.Rzk.Free.Syntax |
| CubeI_0 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| CubeI_0E | Language.Rzk.Free.Syntax |
| CubeI_0F | Language.Rzk.Free.Syntax |
| CubeI_0T | Language.Rzk.Free.Syntax |
| cubeI_0T | Rzk.TypeCheck |
| CubeI_0TE | Language.Rzk.Free.Syntax |
| CubeI_1 | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| CubeI_1E | Language.Rzk.Free.Syntax |
| CubeI_1F | Language.Rzk.Free.Syntax |
| CubeI_1T | Language.Rzk.Free.Syntax |
| cubeI_1T | Rzk.TypeCheck |
| CubeI_1TE | Language.Rzk.Free.Syntax |
| CubeProduct | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| CubeProductE | Language.Rzk.Free.Syntax |
| CubeProductF | Language.Rzk.Free.Syntax |
| CubeProductT | Language.Rzk.Free.Syntax |
| cubeProductT | Rzk.TypeCheck |
| CubeProductTE | Language.Rzk.Free.Syntax |
| cubeSubTopes | Rzk.TypeCheck |
| cubeT | Rzk.TypeCheck |
| CubeUnflip | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| CubeUnflipE | Language.Rzk.Free.Syntax |
| CubeUnflipF | Language.Rzk.Free.Syntax |
| CubeUnflipT | Language.Rzk.Free.Syntax |
| cubeUnflipT | Rzk.TypeCheck |
| CubeUnflipTE | Language.Rzk.Free.Syntax |
| CubeUnit | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| CubeUnitE | Language.Rzk.Free.Syntax |
| CubeUnitF | Language.Rzk.Free.Syntax |
| CubeUnitStar | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| CubeUnitStarE | Language.Rzk.Free.Syntax |
| CubeUnitStarF | Language.Rzk.Free.Syntax |
| CubeUnitStarT | Language.Rzk.Free.Syntax |
| cubeUnitStarT | Rzk.TypeCheck |
| CubeUnitStarTE | Language.Rzk.Free.Syntax |
| CubeUnitT | Language.Rzk.Free.Syntax |
| cubeUnitT | Rzk.TypeCheck |
| CubeUnitTE | Language.Rzk.Free.Syntax |
| currentCommand | Rzk.TypeCheck |
| Debug | Rzk.TypeCheck |
| Decl | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| Decl' | Rzk.TypeCheck |
| declIsAssumption | Rzk.TypeCheck |
| declLocation | Rzk.TypeCheck |
| declName | Rzk.TypeCheck |
| declType | 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 |
| DeclUsedVars' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| declValue | Rzk.TypeCheck |
| defaultCamera | Rzk.TypeCheck |
| defaultRzkEnv | Language.Rzk.VSCode.Env |
| defaultTypeCheck | Rzk.TypeCheck |
| defaultTypeCheckWithHoles | Rzk.TypeCheck |
| defaultTypeCheckWithHoles' | Rzk.TypeCheck |
| defaultVarIdents | Language.Rzk.Free.Syntax |
| deferHoleMismatches | Rzk.TypeCheck |
| Definitive | Language.Rzk.Syntax.Layout |
| delimClose | Language.Rzk.Syntax.Layout |
| delimOpen | Language.Rzk.Syntax.Layout |
| delimSep | Language.Rzk.Syntax.Layout |
| destructuringBinder | Rzk.TypeCheck |
| desugarTuple | Language.Rzk.Free.Syntax |
| 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 |
| Doc | Language.Rzk.Syntax.Print |
| doc | Language.Rzk.Syntax.Print |
| doesShadowName | Rzk.TypeCheck |
| Edge3D | Rzk.TypeCheck |
| edges | Rzk.TypeCheck |
| eitherResIdent | Language.Rzk.Syntax.Lex |
| ElimCost | Rzk.TypeCheck |
| eliminatorsOf | Rzk.TypeCheck |
| Empty | Free.Scoped |
| emptyContext | Rzk.TypeCheck |
| emptyTopeContext | Rzk.TypeCheck |
| endpointsAgree | Rzk.TypeCheck |
| endSection | Rzk.TypeCheck |
| entailM | Rzk.TypeCheck |
| entailTraceM | Rzk.TypeCheck |
| enterModality | Rzk.TypeCheck |
| enterScope | Rzk.TypeCheck |
| enterScopeContext | Rzk.TypeCheck |
| enterScopeMaybe | Rzk.TypeCheck |
| enterScopeWithBind | Rzk.TypeCheck |
| Err | Language.Rzk.Syntax.Lex |
| etaExpand | Rzk.TypeCheck |
| etaMatch | Rzk.TypeCheck |
| exclude | Rzk.Project.Config |
| expandRzkPathsOrYaml | Rzk.Main |
| Explicit | Language.Rzk.Syntax.Layout |
| ExtE | Free.Scoped |
| extractFilesFromRzkYaml | Rzk.Main |
| extractMarkdownCodeBlocks | Language.Rzk.Syntax |
| Face3D | Rzk.TypeCheck |
| faces | Rzk.TypeCheck |
| filterAccessible | Rzk.TypeCheck |
| filterInaccessible | Rzk.TypeCheck |
| First | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| FirstE | Language.Rzk.Free.Syntax |
| FirstF | Language.Rzk.Free.Syntax |
| FirstT | Language.Rzk.Free.Syntax |
| firstT | Rzk.TypeCheck |
| FirstTE | Language.Rzk.Free.Syntax |
| fitsInto | Rzk.TypeCheck |
| Flat | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| flattenBinderApp | Language.Rzk.Free.Syntax |
| foldBinderProjections | Language.Rzk.Free.Syntax |
| foldBinderProjectionsT | Language.Rzk.Free.Syntax |
| 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 |
| formatTextEdits | Rzk.Format |
| FormattingEdit | |
| 1 (Type/Class) | Rzk.Format |
| 2 (Data Constructor) | Rzk.Format |
| Free | Free.Scoped |
| freeVars | Language.Rzk.Free.Syntax |
| freeVarsT | Language.Rzk.Free.Syntax |
| freeVarsT_ | Rzk.TypeCheck |
| freshBinders | Rzk.TypeCheck |
| freshenBinderLeaves | Language.Rzk.Free.Syntax |
| fromAffine | Rzk.TypeCheck |
| fromMod | Language.Rzk.Free.Syntax |
| fromScope' | Language.Rzk.Free.Syntax |
| fromScopeBinder' | Language.Rzk.Free.Syntax |
| fromTerm' | Language.Rzk.Free.Syntax |
| fromTermWith' | Language.Rzk.Free.Syntax |
| fromTModalityToModalColon | Language.Rzk.Free.Syntax |
| fromTypeError | Rzk.TypeCheck |
| fromVarIdent | Language.Rzk.Free.Syntax |
| FS | Free.Scoped |
| generateTopes | Rzk.TypeCheck |
| generateTopesForModalCubeVarsM | Rzk.TypeCheck |
| generateTopesForPointsM | Rzk.TypeCheck |
| getCachedTypecheckedModules | Language.Rzk.VSCode.Env |
| getType | Language.Rzk.Free.Syntax |
| getVarIdent | Language.Rzk.Free.Syntax |
| 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.TypeCheck |
| hidingTerm | Rzk.TypeCheck |
| hintLemmas | Rzk.TypeCheck |
| Hole | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| holeCandidates | Rzk.TypeCheck |
| holeCubeVars | 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 |
| HoleE | Language.Rzk.Free.Syntax |
| HoleEntry | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| holeEntryName | Rzk.TypeCheck |
| holeEntryType | Rzk.TypeCheck |
| HoleF | Language.Rzk.Free.Syntax |
| holeGoal | Rzk.TypeCheck |
| holeGoalShape | 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.Free.Syntax |
| HoleInfo | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| holeIntroductions | Rzk.TypeCheck |
| holeLocation | Rzk.TypeCheck |
| holeName | |
| 1 (Function) | Language.Rzk.Free.Syntax |
| 2 (Function) | Rzk.TypeCheck |
| holesAreErrors | Rzk.TypeCheck |
| HoleT | Language.Rzk.Free.Syntax |
| HoleTE | Language.Rzk.Free.Syntax |
| holeTermVars | Rzk.TypeCheck |
| holeTopes | Rzk.TypeCheck |
| Id | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| iden | Rzk.TypeCheck |
| IdJ | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| IdJE | Language.Rzk.Free.Syntax |
| IdJF | Language.Rzk.Free.Syntax |
| IdJT | Language.Rzk.Free.Syntax |
| idJT | Rzk.TypeCheck |
| IdJTE | Language.Rzk.Free.Syntax |
| Implicit | Language.Rzk.Syntax.Layout |
| inAllSubContexts | Rzk.TypeCheck |
| Inc | Free.Scoped |
| incIndex | Language.Rzk.Free.Syntax |
| include | Rzk.Project.Config |
| inCubeLayer | Rzk.TypeCheck |
| incVarIdentIndex | Language.Rzk.Free.Syntax |
| indentation | Language.Rzk.Syntax.Layout |
| infer | Rzk.TypeCheck |
| inferAs | Rzk.TypeCheck |
| inferStandalone | Rzk.TypeCheck |
| infoNF | Language.Rzk.Free.Syntax |
| infoType | Language.Rzk.Free.Syntax |
| infoWHNF | Language.Rzk.Free.Syntax |
| InL | Free.Scoped |
| InR | Free.Scoped |
| insertExplicitAssumptionFor | Rzk.TypeCheck |
| insertExplicitAssumptionFor' | Rzk.TypeCheck |
| instantiate | Free.Scoped |
| inTopeLayer | Rzk.TypeCheck |
| invalidateWHNF | Language.Rzk.Free.Syntax |
| Invariant | Rzk.TypeCheck |
| isAccessible | Rzk.TypeCheck |
| isCubeOrTopeType | Rzk.TypeCheck |
| isCubeType | Rzk.TypeCheck |
| isHoleT | Rzk.TypeCheck |
| isImplicit | Language.Rzk.Syntax.Layout |
| isLayout | Language.Rzk.Syntax.Layout |
| isLayoutClose | Language.Rzk.Syntax.Layout |
| isLayoutOpen | Language.Rzk.Syntax.Layout |
| isLayoutSep | Language.Rzk.Syntax.Layout |
| isParenClose | Language.Rzk.Syntax.Layout |
| isParenOpen | Language.Rzk.Syntax.Layout |
| isRA | Rzk.TypeCheck |
| isStop | Language.Rzk.Syntax.Layout |
| issueTypeError | Rzk.TypeCheck |
| issueWarning | Rzk.TypeCheck |
| isTokenIn | Language.Rzk.Syntax.Layout |
| isTopLevelVar | Rzk.TypeCheck |
| isWellFormatted | Rzk.Format |
| isWellFormattedFile | Rzk.Format |
| Lambda | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| LambdaE | Language.Rzk.Free.Syntax |
| LambdaF | Language.Rzk.Free.Syntax |
| LambdaT | Language.Rzk.Free.Syntax |
| lambdaT | Rzk.TypeCheck |
| LambdaTE | Language.Rzk.Free.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 |
| 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 |
| Let | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| LetE | Language.Rzk.Free.Syntax |
| LetF | Language.Rzk.Free.Syntax |
| LetMod | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| LetModE | Language.Rzk.Free.Syntax |
| LetModF | Language.Rzk.Free.Syntax |
| LetModT | Language.Rzk.Free.Syntax |
| letModT | Rzk.TypeCheck |
| LetModTE | Language.Rzk.Free.Syntax |
| LetT | Language.Rzk.Free.Syntax |
| letT | Rzk.TypeCheck |
| LetTE | Language.Rzk.Free.Syntax |
| limitLength | Rzk.TypeCheck |
| Line | Language.Rzk.Syntax.Layout |
| line | Language.Rzk.Syntax.Layout |
| localDecl | Rzk.TypeCheck |
| localDeclPrepared | Rzk.TypeCheck |
| localDecls | Rzk.TypeCheck |
| localDeclsPrepared | Rzk.TypeCheck |
| localHideTerm | Rzk.TypeCheck |
| localRenderBackend | Rzk.TypeCheck |
| localScopes | Rzk.TypeCheck |
| localTope | Rzk.TypeCheck |
| localTopes | Rzk.TypeCheck |
| localTopesEntailBottom | Rzk.TypeCheck |
| localTopesNF | Rzk.TypeCheck |
| localTopesNFUnion | Rzk.TypeCheck |
| localVerbosity | Rzk.TypeCheck |
| location | Rzk.TypeCheck |
| locationFilePath | Rzk.TypeCheck |
| LocationInfo | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| locationLine | Rzk.TypeCheck |
| locationOfTypeError | Rzk.Diagnostic |
| locationToJSON | Rzk.Diagnostic |
| locksOfVar | Rzk.TypeCheck |
| logDebug | Language.Rzk.VSCode.Logging |
| logError | Language.Rzk.VSCode.Logging |
| logInfo | Language.Rzk.VSCode.Logging |
| logWarning | Language.Rzk.VSCode.Logging |
| LSP | Language.Rzk.VSCode.Env |
| makeAssumptionExplicit | Rzk.TypeCheck |
| makeCompletePragma | Free.Scoped.TH |
| makeCompletePragmaE | Free.Scoped.TH |
| makeCompletePragmaT | Free.Scoped.TH |
| makeCompletePragmaTE | Free.Scoped.TH |
| makePatternEFor | Free.Scoped.TH |
| makePatternFor | Free.Scoped.TH |
| makePatternsAll | Free.Scoped.TH |
| makePatternTEFor | Free.Scoped.TH |
| makePatternTFor | Free.Scoped.TH |
| Matrix3D | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| matrix3Dto4D | Rzk.TypeCheck |
| Matrix4D | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| matrixVectorMult4D | Rzk.TypeCheck |
| maxDiagnosticCount | Language.Rzk.VSCode.Lsp |
| maxEliminationDepth | Rzk.TypeCheck |
| memoizeWHNF | Rzk.TypeCheck |
| mkConP | Free.Scoped.TH |
| mkEsc | Language.Rzk.Syntax.Print |
| mkPosToken | Language.Rzk.Syntax.Lex |
| mkToken | Language.Rzk.VSCode.Tokenize |
| modAccum | Rzk.TypeCheck |
| 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.Free.Syntax |
| ModalColonOp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ModalColonSharp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| modalColonToTModality | Language.Rzk.Free.Syntax |
| Modality | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Modality' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| modalityOfVar | Rzk.TypeCheck |
| ModalTope | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| ModApp | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| ModAppE | Language.Rzk.Free.Syntax |
| ModAppF | Language.Rzk.Free.Syntax |
| ModAppT | Language.Rzk.Free.Syntax |
| modAppT | Rzk.TypeCheck |
| ModAppTE | Language.Rzk.Free.Syntax |
| ModComp | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ModComp' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| modCompToMods | Language.Rzk.Free.Syntax |
| ModeTheory | Rzk.TypeCheck |
| ModExtract | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| ModExtractE | Language.Rzk.Free.Syntax |
| ModExtractF | Language.Rzk.Free.Syntax |
| ModExtractT | Language.Rzk.Free.Syntax |
| modExtractT | Rzk.TypeCheck |
| ModExtractTE | Language.Rzk.Free.Syntax |
| modsToModComp | Language.Rzk.Free.Syntax |
| 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 |
| myLexer | Language.Rzk.Syntax.Par |
| N | Language.Rzk.Syntax.Lex |
| namedBlock | Rzk.TypeCheck |
| newLine | Language.Rzk.Syntax.Layout |
| nextPos | Language.Rzk.Syntax.Layout |
| nfT | Rzk.TypeCheck |
| nfTope | Rzk.TypeCheck |
| noDeclUsedVars | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Normal | Rzk.TypeCheck |
| normalizeTabs | Rzk.Format |
| NoSectionName | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| nubTermT | Rzk.TypeCheck |
| Op | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| OutputDirection | Rzk.TypeCheck |
| Pair | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| PairE | Language.Rzk.Free.Syntax |
| PairF | Language.Rzk.Free.Syntax |
| PairT | Language.Rzk.Free.Syntax |
| pairT | Rzk.TypeCheck |
| PairTE | Language.Rzk.Free.Syntax |
| panicImpossible | 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 |
| ParamPatternShapeDeprecated | 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 |
| ParamTermTypeDeprecated | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| paramToParamDecl | Rzk.TypeCheck |
| ParamType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamVarShapeDeprecated | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| paramVarShapeDeprecated | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| parenClose | Language.Rzk.Syntax.Layout |
| parenOpen | Language.Rzk.Syntax.Layout |
| parenth | Language.Rzk.Syntax.Print |
| parseModule | Language.Rzk.Syntax |
| parseModuleFile | Language.Rzk.Syntax |
| parseModuleRzk | Language.Rzk.Syntax |
| parseModuleSafe | Language.Rzk.Syntax |
| parseRzkFilesOrStdin | Rzk.Main |
| parseStdin | Rzk.Main |
| parseTerm | Language.Rzk.Syntax |
| partialFreeVarsT | Language.Rzk.Free.Syntax |
| partitionAccessible | 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.Free.Syntax |
| 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 |
| pDeclUsedVars | Language.Rzk.Syntax.Par |
| performing | Rzk.TypeCheck |
| PFst | Language.Rzk.Free.Syntax |
| pHoleIdent | Language.Rzk.Syntax.Par |
| plainTope | Rzk.TypeCheck |
| PlainTypeError | Rzk.TypeCheck |
| pLanguage | Language.Rzk.Syntax.Par |
| pLanguageDecl | Language.Rzk.Syntax.Par |
| pListCommand | 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 |
| 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.TypeCheck |
| Point3D | Rzk.TypeCheck |
| point3Dto2D | Rzk.TypeCheck |
| PointId | Rzk.TypeCheck |
| Position | Language.Rzk.Syntax.Layout |
| posLineCol | Language.Rzk.Syntax.Lex |
| Posn | Language.Rzk.Syntax.Lex |
| ppAction | Rzk.TypeCheck |
| pParam | Language.Rzk.Syntax.Par |
| pParamDecl | Language.Rzk.Syntax.Par |
| pPattern | Language.Rzk.Syntax.Par |
| pPattern1 | Language.Rzk.Syntax.Par |
| ppContext' | Rzk.TypeCheck |
| ppFoldT | Rzk.TypeCheck |
| ppFoldU | Rzk.TypeCheck |
| ppHoleInfo | Rzk.Diagnostic |
| ppLocationInfo | Rzk.Diagnostic |
| ppModality | Rzk.TypeCheck |
| ppRzkPosition | Language.Rzk.Free.Syntax |
| ppSomeAction | Rzk.TypeCheck |
| ppTermInContext | Rzk.TypeCheck |
| ppTypeError' | Rzk.TypeCheck |
| ppTypeErrorInContext | Rzk.TypeCheck |
| ppTypeErrorInScopedContext' | Rzk.TypeCheck |
| ppTypeErrorInScopedContextWith' | Rzk.TypeCheck |
| ppVarIdentWithLocation | Language.Rzk.Free.Syntax |
| 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.Free.Syntax |
| projChain | Language.Rzk.Free.Syntax |
| projChainT | Language.Rzk.Free.Syntax |
| project2D | Rzk.TypeCheck |
| ProjectConfig | |
| 1 (Type/Class) | Rzk.Project.Config |
| 2 (Data Constructor) | Rzk.Project.Config |
| provideCompletions | Language.Rzk.VSCode.Handlers |
| provideSemanticTokens | 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 |
| pSectionName | Language.Rzk.Syntax.Par |
| pSigmaParam | Language.Rzk.Syntax.Par |
| PSnd | Language.Rzk.Free.Syntax |
| 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 |
| Pure | Free.Scoped |
| pVarIdent | Language.Rzk.Syntax.Par |
| quickIndex | Language.Rzk.Syntax.Lex |
| RecBottom | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| recBottomCandidates | Rzk.TypeCheck |
| RecBottomE | Language.Rzk.Free.Syntax |
| RecBottomF | Language.Rzk.Free.Syntax |
| RecBottomT | Language.Rzk.Free.Syntax |
| recBottomT | Rzk.TypeCheck |
| RecBottomTE | Language.Rzk.Free.Syntax |
| RecOr | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| recOrCandidates | Rzk.TypeCheck |
| RecOrDeprecated | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| recordHole | Rzk.TypeCheck |
| recordHoleShape | Rzk.TypeCheck |
| RecOrE | Language.Rzk.Free.Syntax |
| RecOrF | Language.Rzk.Free.Syntax |
| RecOrT | Language.Rzk.Free.Syntax |
| recOrT | Rzk.TypeCheck |
| RecOrTE | Language.Rzk.Free.Syntax |
| Refl | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| ReflE | Language.Rzk.Free.Syntax |
| ReflF | Language.Rzk.Free.Syntax |
| ReflT | Language.Rzk.Free.Syntax |
| reflT | Rzk.TypeCheck |
| ReflTE | Language.Rzk.Free.Syntax |
| ReflTerm | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ReflTermType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| refreshVar | Language.Rzk.Free.Syntax |
| render | Language.Rzk.Syntax.Print |
| RenderBackend | Rzk.TypeCheck |
| renderBackend | Rzk.TypeCheck |
| renderCube | Rzk.TypeCheck |
| renderForSubShapeSVG | Rzk.TypeCheck |
| renderForSVG | Rzk.TypeCheck |
| renderGoalCellSVG | Rzk.TypeCheck |
| renderHideTerm | Rzk.TypeCheck |
| RenderLaTeX | Rzk.TypeCheck |
| RenderObjectData | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| renderObjectDataColor | Rzk.TypeCheck |
| renderObjectDataFullLabel | Rzk.TypeCheck |
| renderObjectDataLabel | Rzk.TypeCheck |
| renderObjectsFor | Rzk.TypeCheck |
| renderObjectsInSubShapeFor | Rzk.TypeCheck |
| RenderSVG | Rzk.TypeCheck |
| renderTermSVG | Rzk.TypeCheck |
| renderTermSVG' | Rzk.TypeCheck |
| renderTermSVGFor | Rzk.TypeCheck |
| 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 |
| restorePatternVars | Language.Rzk.Free.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.TypeCheck |
| rotateY | Rzk.TypeCheck |
| rotateZ | Rzk.TypeCheck |
| runLsp | Language.Rzk.VSCode.Lsp |
| 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 |
| rzkEnvTypecheckCache | Language.Rzk.VSCode.Env |
| rzkFilePath | Language.Rzk.Free.Syntax |
| rzkLineCol | Language.Rzk.Free.Syntax |
| RzkPosition | |
| 1 (Type/Class) | Language.Rzk.Free.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| RzkTypecheckCache | Language.Rzk.VSCode.Env |
| S | Free.Scoped |
| saturateBottom | Rzk.TypeCheck |
| saturateInv | Rzk.TypeCheck |
| saturateTopes | Rzk.TypeCheck |
| saturateWith | Rzk.TypeCheck |
| Scope | Free.Scoped |
| ScopedTypeError | Rzk.TypeCheck |
| ScopeInfo | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| scopeName | Rzk.TypeCheck |
| scopeToDecls | Rzk.TypeCheck |
| scopeVars | Rzk.TypeCheck |
| Second | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| SecondE | Language.Rzk.Free.Syntax |
| SecondF | Language.Rzk.Free.Syntax |
| SecondT | Language.Rzk.Free.Syntax |
| secondT | Rzk.TypeCheck |
| SecondTE | Language.Rzk.Free.Syntax |
| SectionName | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 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 |
| setVariance | Rzk.TypeCheck |
| Severity | Rzk.Diagnostic |
| SeverityError | Rzk.Diagnostic |
| SeverityHint | Rzk.Diagnostic |
| SeverityInformation | Rzk.Diagnostic |
| SeverityWarning | Rzk.Diagnostic |
| ShapeId | Rzk.TypeCheck |
| Sharp | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| 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.Free.Syntax |
| Silent | Rzk.TypeCheck |
| simplifyLHS | Rzk.TypeCheck |
| simplifyLHSwithDisjunctions | Rzk.TypeCheck |
| Single | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| solveRHS | Rzk.TypeCheck |
| solveRHSM | Rzk.TypeCheck |
| SomeSectionName | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| SpineStep | Rzk.TypeCheck |
| splits | Rzk.TypeCheck |
| splitSectionCommands | Rzk.TypeCheck |
| startSection | Rzk.TypeCheck |
| Status | Language.Rzk.Syntax.Layout |
| sToken | Language.Rzk.Syntax.Layout |
| stripTypeRestrictions | Rzk.TypeCheck |
| structuralHoleUnify | Rzk.TypeCheck |
| subPoints | Rzk.TypeCheck |
| substitute | Free.Scoped |
| substituteT | Language.Rzk.Free.Syntax |
| subTopes2 | Rzk.TypeCheck |
| Sum | Free.Scoped |
| switchVariance | 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.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 |
| 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 |
| unifyInCurrentContext | Rzk.TypeCheck |
| unifyTerms | Rzk.TypeCheck |
| unifyTopes | Rzk.TypeCheck |
| unifyTypes | Rzk.TypeCheck |
| unifyViaDecompose | Rzk.TypeCheck |
| Unit | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| UnitE | Language.Rzk.Free.Syntax |
| UnitF | Language.Rzk.Free.Syntax |
| UnitT | Language.Rzk.Free.Syntax |
| unitT | Rzk.TypeCheck |
| UnitTE | Language.Rzk.Free.Syntax |
| Universe | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| UniverseCube | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| UniverseCubeE | Language.Rzk.Free.Syntax |
| UniverseCubeF | Language.Rzk.Free.Syntax |
| UniverseCubeT | Language.Rzk.Free.Syntax |
| UniverseCubeTE | Language.Rzk.Free.Syntax |
| UniverseE | Language.Rzk.Free.Syntax |
| UniverseF | Language.Rzk.Free.Syntax |
| UniverseT | Language.Rzk.Free.Syntax |
| universeT | Rzk.TypeCheck |
| UniverseTE | Language.Rzk.Free.Syntax |
| UniverseTope | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| UniverseTopeE | Language.Rzk.Free.Syntax |
| UniverseTopeF | Language.Rzk.Free.Syntax |
| UniverseTopeT | Language.Rzk.Free.Syntax |
| UniverseTopeTE | Language.Rzk.Free.Syntax |
| unsafeInferStandalone' | Rzk.TypeCheck |
| unsafeTermToPattern | Language.Rzk.Free.Syntax |
| unsafeTraceAction' | Rzk.TypeCheck |
| unsafeTypeCheck' | Rzk.TypeCheck |
| unsetOption | Rzk.TypeCheck |
| untyped | Free.Scoped |
| utf8Encode | Language.Rzk.Syntax.Lex |
| valueOfVar | Rzk.TypeCheck |
| Var | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| varBinders | Rzk.TypeCheck |
| varDeclaredAssumptions | 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.Free.Syntax |
| 4 (Data Constructor) | Language.Rzk.Free.Syntax |
| varIdent | Language.Rzk.Free.Syntax |
| VarIdent' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| varIdentAt | Language.Rzk.Free.Syntax |
| 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 |
| 2 (Data Constructor) | Rzk.TypeCheck |
| varInfos | Rzk.TypeCheck |
| varIsAssumption | Rzk.TypeCheck |
| varIsTopLevel | Rzk.TypeCheck |
| varLocation | Rzk.TypeCheck |
| varLocks | Rzk.TypeCheck |
| varModalities | Rzk.TypeCheck |
| varModality | Rzk.TypeCheck |
| varOrig | Rzk.TypeCheck |
| varOrigs | Rzk.TypeCheck |
| varTopLevels | Rzk.TypeCheck |
| varType | Rzk.TypeCheck |
| varTypes | Rzk.TypeCheck |
| varValue | Rzk.TypeCheck |
| varValues | Rzk.TypeCheck |
| Vector3D | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| Vector4D | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| Verbosity | Rzk.TypeCheck |
| verbosity | Rzk.TypeCheck |
| vertices | Rzk.TypeCheck |
| verticesFrom | Rzk.TypeCheck |
| viewRotateX | Rzk.TypeCheck |
| viewRotateY | Rzk.TypeCheck |
| viewTranslate | Rzk.TypeCheck |
| Volume3D | Rzk.TypeCheck |
| volumes | Rzk.TypeCheck |
| whnfT | Rzk.TypeCheck |
| withCommand | Rzk.TypeCheck |
| withHintLemmas | Rzk.TypeCheck |
| withLocation | Rzk.TypeCheck |
| withPartialDecls | Rzk.TypeCheck |
| withSection | Rzk.TypeCheck |
| Z | Free.Scoped |