Lean statement not rendered for theorems defined as def thm : Prop := statement

[utensil]

Lean statement not rendered for theorems defined as def thm : Prop := statement

Issue Example

For FltRegular doc, it shows only Prop instead 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.ofConstant or DocGen4.Process.DefinitionInfo.ofDefinitionVal.

Related Zulip discussion

here