| :+: | Free.Scoped |
| abstract | Free.Scoped |
| abstractAssumption | Rzk.TypeCheck |
| Action | Rzk.TypeCheck |
| Action' | Rzk.TypeCheck |
| ActionCheckCoherence | Rzk.TypeCheck |
| ActionCloseSection | Rzk.TypeCheck |
| ActionContextEntailedBy | Rzk.TypeCheck |
| ActionContextEntails | Rzk.TypeCheck |
| ActionContextEquiv | 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 |
| 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 |
| 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 |
| AppT | Language.Rzk.Free.Syntax |
| appT | Rzk.TypeCheck |
| AppTE | Language.Rzk.Free.Syntax |
| askCurrentScope | Rzk.TypeCheck |
| B | Language.Rzk.Syntax.Lex |
| Block | Language.Rzk.Syntax.Layout |
| 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 |
| BTree | Language.Rzk.Syntax.Lex |
| Byte | Language.Rzk.Syntax.Lex |
| 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 |
| checkNameShadowing | Rzk.TypeCheck |
| checkTope | Rzk.TypeCheck |
| checkTopeEntails | Rzk.TypeCheck |
| checkTopLevelDuplicate | 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 |
| 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 |
| componentWiseEQT | Rzk.TypeCheck |
| concatD | Language.Rzk.Syntax.Print |
| concatS | Language.Rzk.Syntax.Print |
| confirm | Language.Rzk.Syntax.Layout |
| Context | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| contextEntailedBy | Rzk.TypeCheck |
| contextEntails | Rzk.TypeCheck |
| contextEquiv | Rzk.TypeCheck |
| Contravariant | Rzk.TypeCheck |
| countCommands | Rzk.TypeCheck |
| Covariance | Rzk.TypeCheck |
| covariance | Rzk.TypeCheck |
| Covariant | 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 |
| 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 |
| 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 |
| 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 |
| defaultTypeCheck | Rzk.TypeCheck |
| defaultVarIdents | Language.Rzk.Free.Syntax |
| Definitive | Language.Rzk.Syntax.Layout |
| delimClose | Language.Rzk.Syntax.Layout |
| delimOpen | Language.Rzk.Syntax.Layout |
| delimSep | Language.Rzk.Syntax.Layout |
| Doc | Language.Rzk.Syntax.Print |
| doc | Language.Rzk.Syntax.Print |
| doesShadowName | Rzk.TypeCheck |
| Edge3D | Rzk.TypeCheck |
| edges | Rzk.TypeCheck |
| eitherResIdent | Language.Rzk.Syntax.Lex |
| Empty | Free.Scoped |
| emptyContext | Rzk.TypeCheck |
| endSection | Rzk.TypeCheck |
| entail | Rzk.TypeCheck |
| enterScope | Rzk.TypeCheck |
| enterScopeContext | Rzk.TypeCheck |
| Err | Language.Rzk.Syntax.Lex |
| etaExpand | Rzk.TypeCheck |
| etaMatch | Rzk.TypeCheck |
| Explicit | Language.Rzk.Syntax.Layout |
| ExtE | Free.Scoped |
| extractMarkdownCodeBlocks | Language.Rzk.Syntax |
| Face3D | Rzk.TypeCheck |
| faces | 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 |
| Free | Free.Scoped |
| freeVars | Language.Rzk.Free.Syntax |
| freeVarsT | Language.Rzk.Free.Syntax |
| freeVarsT_ | Rzk.TypeCheck |
| fromAffine | Rzk.TypeCheck |
| fromScope' | Language.Rzk.Free.Syntax |
| fromTerm' | Language.Rzk.Free.Syntax |
| fromTermWith' | Language.Rzk.Free.Syntax |
| FS | Free.Scoped |
| generateTopes | Rzk.TypeCheck |
| generateTopesForPoints | Rzk.TypeCheck |
| getType | Language.Rzk.Free.Syntax |
| happyError | Language.Rzk.Syntax.Par |
| HasPosition | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| hasPosition | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Hole | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| HoleIdent | |
| 1 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 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 |
| inCubeLayer | Rzk.TypeCheck |
| 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 |
| 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 |
| isStop | Language.Rzk.Syntax.Layout |
| issueTypeError | Rzk.TypeCheck |
| issueWarning | Rzk.TypeCheck |
| isTokenIn | Language.Rzk.Syntax.Layout |
| 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 |
| 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 |
| 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 |
| main | Rzk.Main |
| 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 |
| mkConP | Free.Scoped.TH |
| mkEsc | Language.Rzk.Syntax.Print |
| mkPosToken | Language.Rzk.Syntax.Lex |
| 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 |
| 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 |
| NoSectionName | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| nubTermT | 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 |
| ParamPatternShape | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamPatternType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| paramToParamDecl | Rzk.TypeCheck |
| ParamType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamVarShape | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| paramVarShape | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamVarType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| paramVarType | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| ParamWildcardType | 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 |
| parseTerm | Language.Rzk.Syntax |
| partialFreeVarsT | Language.Rzk.Free.Syntax |
| Pattern | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| Pattern' | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| PatternPair | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| PatternVar | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| PatternWildcard | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| pCommand | Language.Rzk.Syntax.Par |
| pDeclUsedVars | Language.Rzk.Syntax.Par |
| performing | 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 |
| pListRestriction | Language.Rzk.Syntax.Par |
| pListTerm | Language.Rzk.Syntax.Par |
| pListVarIdent | 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 |
| ppContext' | Rzk.TypeCheck |
| ppSomeAction | Rzk.TypeCheck |
| ppTermInContext | Rzk.TypeCheck |
| ppTypeError' | Rzk.TypeCheck |
| ppTypeErrorInContext | Rzk.TypeCheck |
| ppTypeErrorInScopedContext' | Rzk.TypeCheck |
| ppTypeErrorInScopedContextWith' | Rzk.TypeCheck |
| ppUsage | Rzk.Main |
| pRestriction | Language.Rzk.Syntax.Par |
| Print | Language.Rzk.Syntax.Print |
| printPosn | Language.Rzk.Syntax.Lex |
| printString | Language.Rzk.Syntax.Print |
| printTree | Language.Rzk.Syntax.Print, Language.Rzk.Syntax |
| project2D | Rzk.TypeCheck |
| prPrec | Language.Rzk.Syntax.Print |
| prt | Language.Rzk.Syntax.Print |
| prToken | Language.Rzk.Syntax.Lex |
| pSectionName | Language.Rzk.Syntax.Par |
| 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 |
| quickIndex | Language.Rzk.Syntax.Lex |
| RecBottom | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| 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 |
| recOr | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 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 |
| 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 |
| resolveLayout | Language.Rzk.Syntax.Layout |
| 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 |
| Rzk1 | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| S | Free.Scoped |
| 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 |
| setOption | Rzk.TypeCheck |
| ShapeId | Rzk.TypeCheck |
| Silent | Rzk.TypeCheck |
| simplifyLHS | Rzk.TypeCheck |
| solveRHS | Rzk.TypeCheck |
| SomeSectionName | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| splits | Rzk.TypeCheck |
| startSection | Rzk.TypeCheck |
| Status | Language.Rzk.Syntax.Layout |
| sToken | Language.Rzk.Syntax.Layout |
| stripTypeRestrictions | Rzk.TypeCheck |
| subPoints | Rzk.TypeCheck |
| substitute | Free.Scoped |
| substituteT | Language.Rzk.Free.Syntax |
| subTopes2 | Rzk.TypeCheck |
| Sum | Free.Scoped |
| switchVariance | Rzk.TypeCheck |
| TC | Language.Rzk.Syntax.Lex |
| TD | Language.Rzk.Syntax.Lex |
| Tentative | Language.Rzk.Syntax.Layout |
| Term | |
| 1 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Free.Syntax |
| Term' | |
| 1 (Type/Class) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Type/Class) | Language.Rzk.Free.Syntax |
| TermF | Language.Rzk.Free.Syntax |
| termF | Free.Scoped |
| termIsNF | Language.Rzk.Free.Syntax |
| termIsWHNF | Language.Rzk.Free.Syntax |
| TermT | Language.Rzk.Free.Syntax |
| TermT' | Language.Rzk.Free.Syntax |
| TI | Language.Rzk.Syntax.Lex |
| TK | Language.Rzk.Syntax.Lex |
| TL | Language.Rzk.Syntax.Lex |
| Tok | Language.Rzk.Syntax.Lex |
| tok | Language.Rzk.Syntax.Lex |
| Token | Language.Rzk.Syntax.Lex |
| tokenLength | Language.Rzk.Syntax.Layout |
| tokenLineCol | Language.Rzk.Syntax.Lex |
| tokenPos | Language.Rzk.Syntax.Lex |
| tokenPosn | Language.Rzk.Syntax.Lex |
| tokens | Language.Rzk.Syntax.Lex |
| tokenText | Language.Rzk.Syntax.Lex |
| TokSymbol | |
| 1 (Type/Class) | Language.Rzk.Syntax.Lex |
| 2 (Data Constructor) | Language.Rzk.Syntax.Lex |
| TopeAnd | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeAndE | Language.Rzk.Free.Syntax |
| TopeAndF | Language.Rzk.Free.Syntax |
| TopeAndT | Language.Rzk.Free.Syntax |
| topeAndT | Rzk.TypeCheck |
| TopeAndTE | Language.Rzk.Free.Syntax |
| TopeBottom | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeBottomE | Language.Rzk.Free.Syntax |
| TopeBottomF | Language.Rzk.Free.Syntax |
| TopeBottomT | Language.Rzk.Free.Syntax |
| topeBottomT | Rzk.TypeCheck |
| TopeBottomTE | Language.Rzk.Free.Syntax |
| TopeEQ | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeEQE | Language.Rzk.Free.Syntax |
| TopeEQF | Language.Rzk.Free.Syntax |
| TopeEQT | Language.Rzk.Free.Syntax |
| topeEQT | Rzk.TypeCheck |
| TopeEQTE | Language.Rzk.Free.Syntax |
| TopeLEQ | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeLEQE | Language.Rzk.Free.Syntax |
| TopeLEQF | Language.Rzk.Free.Syntax |
| TopeLEQT | Language.Rzk.Free.Syntax |
| topeLEQT | Rzk.TypeCheck |
| TopeLEQTE | Language.Rzk.Free.Syntax |
| TopeOr | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeOrE | Language.Rzk.Free.Syntax |
| TopeOrF | Language.Rzk.Free.Syntax |
| TopeOrT | Language.Rzk.Free.Syntax |
| topeOrT | Rzk.TypeCheck |
| TopeOrTE | Language.Rzk.Free.Syntax |
| topePoints | Rzk.TypeCheck |
| topesEquiv | Rzk.TypeCheck |
| topeT | Rzk.TypeCheck |
| TopeTop | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TopeTopE | Language.Rzk.Free.Syntax |
| TopeTopF | Language.Rzk.Free.Syntax |
| TopeTopT | Language.Rzk.Free.Syntax |
| topeTopT | Rzk.TypeCheck |
| TopeTopTE | Language.Rzk.Free.Syntax |
| toScope | Language.Rzk.Free.Syntax |
| toScopePattern | Language.Rzk.Free.Syntax |
| toTerm | Language.Rzk.Free.Syntax |
| toTerm' | Language.Rzk.Free.Syntax |
| trace' | Rzk.TypeCheck |
| traceAction' | Rzk.TypeCheck |
| traceStartAndFinish | Rzk.TypeCheck |
| traceTypeCheck | Rzk.TypeCheck |
| transFS | Free.Scoped |
| tryExtractMarkdownCodeBlocks | Language.Rzk.Syntax |
| tryRestriction | Rzk.TypeCheck |
| TS | Language.Rzk.Syntax.Lex |
| tsID | Language.Rzk.Syntax.Lex |
| tsText | Language.Rzk.Syntax.Lex |
| TV | Language.Rzk.Syntax.Lex |
| Type | |
| 1 (Type/Class) | Language.Rzk.Free.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeAsc | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeAscE | Language.Rzk.Free.Syntax |
| TypeAscF | Language.Rzk.Free.Syntax |
| TypeAscT | Language.Rzk.Free.Syntax |
| typeAscT | Rzk.TypeCheck |
| TypeAscTE | Language.Rzk.Free.Syntax |
| TypeCheck | Rzk.TypeCheck |
| typecheck | Rzk.TypeCheck |
| typecheckModule | Rzk.TypeCheck |
| typecheckModules | Rzk.TypeCheck |
| typecheckModulesWithLocation | Rzk.TypeCheck |
| typecheckModuleWithLocation | Rzk.TypeCheck |
| typecheckString | Rzk.Main |
| TypeError | Rzk.TypeCheck |
| TypeError' | Rzk.TypeCheck |
| TypeErrorCannotInferBareLambda | Rzk.TypeCheck |
| TypeErrorCannotInferBareRefl | Rzk.TypeCheck |
| typeErrorContext | Rzk.TypeCheck |
| TypeErrorDuplicateTopLevel | Rzk.TypeCheck |
| typeErrorError | Rzk.TypeCheck |
| TypeErrorImplicitAssumption | Rzk.TypeCheck |
| TypeErrorInContext | |
| 1 (Type/Class) | Rzk.TypeCheck |
| 2 (Data Constructor) | Rzk.TypeCheck |
| TypeErrorInScopedContext | Rzk.TypeCheck |
| TypeErrorInvalidArgumentType | Rzk.TypeCheck |
| TypeErrorNotFunction | Rzk.TypeCheck |
| TypeErrorNotPair | Rzk.TypeCheck |
| TypeErrorOther | Rzk.TypeCheck |
| TypeErrorTopeNotSatisfied | Rzk.TypeCheck |
| TypeErrorTopesNotEquivalent | Rzk.TypeCheck |
| TypeErrorUndefined | Rzk.TypeCheck |
| TypeErrorUnexpectedLambda | Rzk.TypeCheck |
| TypeErrorUnexpectedPair | Rzk.TypeCheck |
| TypeErrorUnexpectedRefl | Rzk.TypeCheck |
| TypeErrorUnify | Rzk.TypeCheck |
| TypeErrorUnifyTerms | Rzk.TypeCheck |
| TypeErrorUnusedUsedVariables | Rzk.TypeCheck |
| TypeErrorUnusedVariable | Rzk.TypeCheck |
| typeExtension | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TypeFun | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeFunE | Language.Rzk.Free.Syntax |
| TypeFunF | Language.Rzk.Free.Syntax |
| TypeFunT | Language.Rzk.Free.Syntax |
| typeFunT | Rzk.TypeCheck |
| TypeFunTE | Language.Rzk.Free.Syntax |
| TypeId | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeIdE | Language.Rzk.Free.Syntax |
| TypeIdF | Language.Rzk.Free.Syntax |
| TypeIdSimple | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| TypeIdT | Language.Rzk.Free.Syntax |
| typeIdT | Rzk.TypeCheck |
| TypeIdTE | Language.Rzk.Free.Syntax |
| TypeInfo | |
| 1 (Type/Class) | Language.Rzk.Free.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| typeOf | Rzk.TypeCheck |
| typeOfUncomputed | Rzk.TypeCheck |
| typeOfVar | Rzk.TypeCheck |
| TypeRestricted | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeRestrictedE | Language.Rzk.Free.Syntax |
| TypeRestrictedF | Language.Rzk.Free.Syntax |
| TypeRestrictedT | Language.Rzk.Free.Syntax |
| typeRestrictedT | Rzk.TypeCheck |
| TypeRestrictedTE | Language.Rzk.Free.Syntax |
| TypeSigma | |
| 1 (Data Constructor) | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| 2 (Data Constructor) | Language.Rzk.Free.Syntax |
| TypeSigmaE | Language.Rzk.Free.Syntax |
| TypeSigmaF | Language.Rzk.Free.Syntax |
| TypeSigmaT | Language.Rzk.Free.Syntax |
| typeSigmaT | Rzk.TypeCheck |
| TypeSigmaTE | Language.Rzk.Free.Syntax |
| T_HoleIdent | Language.Rzk.Syntax.Lex |
| T_VarIdent | Language.Rzk.Syntax.Lex |
| unescapeInitTail | Language.Rzk.Syntax.Lex |
| unicode_TypeFun | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| unicode_TypeSigma | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| unicode_TypeSigmaAlt | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| unify | Rzk.TypeCheck |
| unifyInCurrentContext | Rzk.TypeCheck |
| unifyTerms | Rzk.TypeCheck |
| unifyTopes | Rzk.TypeCheck |
| unifyTypes | Rzk.TypeCheck |
| 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 |
| unsafeTraceAction' | Rzk.TypeCheck |
| unsetOption | Rzk.TypeCheck |
| untyped | Free.Scoped |
| utf8Encode | Language.Rzk.Syntax.Lex |
| valueOfVar | Rzk.TypeCheck |
| Var | Language.Rzk.Syntax.Abs, Language.Rzk.Syntax |
| varDeclaredAssumptions | Rzk.TypeCheck |
| VarIdent | |
| 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 |
| varOrig | Rzk.TypeCheck |
| varOrigs | 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 |
| withLocation | Rzk.TypeCheck |
| withSection | Rzk.TypeCheck |
| Z | Free.Scoped |