Open alreadydone opened 9 months ago
doc-gen has two approaches to rendering equations.
One is to use the simplification equations that you get for free. However these are not available on all definitions. In this situation it will instead decide to render basically defName = defBody
. And I would not really like to process the body myself in an effort to figure out where potentially omittable things are hidden. If there is some option that disables rendering Prop
stuff in terms we can definitely enable that and see how it goes though.
Some pretty modest definitions, like nonZeroDivisors, are not shown in the docs, and the message "One or more equations did not get rendered due to their size." is shown instead. Even though the proofs take four lines in this case, the only data field
carrier := { x | ∀ z, z * x = 0 → z = 0 }
is quite simple and people shouldn't need to open a new page to view the definition in the source.I guess maybe doc-gen sees the term-mode proofs generated by the tactics, which can be quite long, so it decides not to show the definition in the docs; if it sees
._proof_1
etc. maybe it will show them, but not showing proofs at all seems to be a better option.