Closed utensil closed 1 year ago
Lean statement not rendered for theorems defined as def thm : Prop := statement
def thm : Prop := statement
For FltRegular doc, it shows only Prop instead of the statement:
Prop
corresponding source code:
For definitions of the type Prop, treat it like a theorem, renders the part aftet :=, like the following example:
:=
Possibly fixable by adding a branch for DocGen4.Process.DocInfo.ofConstant or DocGen4.Process.DefinitionInfo.ofDefinitionVal.
DocGen4.Process.DocInfo.ofConstant
DocGen4.Process.DefinitionInfo.ofDefinitionVal
here
Lean statement not rendered for theorems defined as
def thm : Prop := statementIssue Example
For FltRegular doc, it shows only
Propinstead of the statement:corresponding source code:
Expected solution
For definitions of the type
Prop, treat it like a theorem, renders the part aftet:=, like the following example:Possibly fixable by adding a branch for
DocGen4.Process.DocInfo.ofConstantorDocGen4.Process.DefinitionInfo.ofDefinitionVal.Related Zulip discussion
here