rzk-0.11.3: An experimental proof assistant for synthetic ∞-categories

Index - D

dataAppliedIndicesRzk.TypeCheck.Decl.Data
DataBodyLanguage.Rzk.Syntax.Abs, Language.Rzk.Syntax
DataBody'Language.Rzk.Syntax.Abs, Language.Rzk.Syntax
dataBodyPartsRzk.TypeCheck.Decl, Rzk.TypeCheck
DataComputeLanguage.Rzk.Syntax.Abs, Language.Rzk.Syntax
dataConFieldPatsRzk.TypeCheck.Decl.Data
dataConFieldsRzk.TypeCheck.Decl.Data
DataConKindRzk.TypeCheck.Context, Rzk.TypeCheck
dataConLocalNamesRzk.TypeCheck.Decl.Data
dataConNameRzk.TypeCheck.Decl.Data
dataConNonRecRzk.TypeCheck.Decl.Data
DataConPathRzk.TypeCheck.Decl.Data
DataConPointRzk.TypeCheck.Decl.Data
dataConProbeRzk.TypeCheck.Decl.Data
dataConRecursiveRzk.TypeCheck.Decl.Data
dataConRetIndicesRzk.TypeCheck.Decl.Data
DataConSortRzk.TypeCheck.Decl.Data
dataConSortRzk.TypeCheck.Decl.Data
dataConstructorsOfRzk.TypeCheck.Judgements, Rzk.TypeCheck
DataConSurface 
1 (Type/Class)Rzk.TypeCheck.Decl.Data
2 (Data Constructor)Rzk.TypeCheck.Decl.Data
dataConSurfaceRzk.TypeCheck.Decl, Rzk.TypeCheck
dataConTypeRzk.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
dataEliminatorsOfRzk.TypeCheck.Judgements, Rzk.TypeCheck
DataElimKindRzk.TypeCheck.Context, Rzk.TypeCheck
dataFieldToParamDeclRzk.TypeCheck.Decl, Rzk.TypeCheck
dataParamVarsRzk.TypeCheck.Decl, Rzk.TypeCheck
DataRole 
1 (Type/Class)Rzk.TypeCheck.Context, Rzk.TypeCheck
2 (Data Constructor)Rzk.TypeCheck.Context, Rzk.TypeCheck
dataRoleDataTypeRzk.TypeCheck.Context, Rzk.TypeCheck
DataRoleKindRzk.TypeCheck.Context, Rzk.TypeCheck
dataRoleKindRzk.TypeCheck.Context, Rzk.TypeCheck
dataRoleNumParamsRzk.TypeCheck.Context, Rzk.TypeCheck
DataSortLanguage.Rzk.Syntax.Abs, Language.Rzk.Syntax
DataSort'Language.Rzk.Syntax.Abs, Language.Rzk.Syntax
dataSortIndicesRzk.TypeCheck.Decl, Rzk.TypeCheck
DebugRzk.TypeCheck.Context, Rzk.TypeCheck
Decl 
1 (Type/Class)Rzk.TypeCheck.Decl, Rzk.TypeCheck
2 (Data Constructor)Rzk.TypeCheck.Decl, Rzk.TypeCheck
declBinderTypesRzk.TypeCheck.BinderTypes, Rzk.TypeCheck
declIsAssumptionRzk.TypeCheck.Decl, Rzk.TypeCheck
DeclKindRzk.TypeCheck.Decl, Rzk.TypeCheck
DeclKindDataRzk.TypeCheck.Decl, Rzk.TypeCheck
DeclKindDataConRzk.TypeCheck.Decl, Rzk.TypeCheck
DeclKindDataElimRzk.TypeCheck.Decl, Rzk.TypeCheck
DeclKindDefineRzk.TypeCheck.Decl, Rzk.TypeCheck
DeclKindPostulateRzk.TypeCheck.Decl, Rzk.TypeCheck
declLocationRzk.TypeCheck.Decl, Rzk.TypeCheck
declNameRzk.TypeCheck.Decl, Rzk.TypeCheck
declNameOfRzk.TypeCheck.Decl, Rzk.TypeCheck
declTypeRzk.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
declUsedVarsRzk.TypeCheck.Decl, Rzk.TypeCheck
DeclUsedVars'Language.Rzk.Syntax.Abs, Language.Rzk.Syntax
declValueRzk.TypeCheck.Decl, Rzk.TypeCheck
DeclView 
1 (Type/Class)Rzk.TypeCheck.Decl, Rzk.TypeCheck
2 (Data Constructor)Rzk.TypeCheck.Decl, Rzk.TypeCheck
declViewIsAssumptionRzk.TypeCheck.Decl, Rzk.TypeCheck
declViewKindRzk.TypeCheck.Decl, Rzk.TypeCheck
declViewLocationRzk.TypeCheck.Decl, Rzk.TypeCheck
declViewNameRzk.TypeCheck.Decl, Rzk.TypeCheck
declViewsRzk.TypeCheck.Decl, Rzk.TypeCheck
declViewTypeRzk.TypeCheck.Decl, Rzk.TypeCheck
defaultCameraRzk.Render.Geometry
defaultRzkEnvLanguage.Rzk.VSCode.Env
defaultVarIdentsLanguage.Rzk.Foil.Names
DefinitiveLanguage.Rzk.Syntax.Layout
delimCloseLanguage.Rzk.Syntax.Layout
delimOpenLanguage.Rzk.Syntax.Layout
delimSepLanguage.Rzk.Syntax.Layout
destructuringBinderRzk.TypeCheck.Judgements, Rzk.TypeCheck
desugarTupleLanguage.Rzk.Foil.Names
diagnoseCheckWarningRzk.Diagnostic
diagnoseHoleRzk.Diagnostic
diagnoseTypeErrorRzk.Diagnostic
Diagnostic 
1 (Type/Class)Rzk.Diagnostic
2 (Data Constructor)Rzk.Diagnostic
diagnosticCodeRzk.Diagnostic
diagnosticHoleRzk.Diagnostic
diagnosticLocationRzk.Diagnostic
diagnosticMessageRzk.Diagnostic
diagnosticSeverityRzk.Diagnostic
dimOfRzk.TypeCheck.Render
discreteAxiomOfRzk.TypeCheck.Eval, Rzk.TypeCheck
DisplayLanguage.Rzk.Foil.Names
displayNameOfLanguage.Rzk.Foil.Print
displayOfRzk.TypeCheck.Display, Rzk.TypeCheck
DocLanguage.Rzk.Syntax.Print
docLanguage.Rzk.Syntax.Print
doesShadowNameRzk.TypeCheck.Judgements, Rzk.TypeCheck
domainEntailsRzk.TypeCheck.Unify
DontKnowRzk.TypeCheck.NbE
drawCubeRzk.TypeCheck.Render
duplicateBindersRzk.TypeCheck.Decl, Rzk.TypeCheck