Doc: definitions expressed as a table in constructive_ereal.v

[yoshihiro503]

Motivation for this change

Source code looks:

Html doc looks:

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[proux01]

I'm lost, didn't we said that bullet lists would be easier to use?
Otherwise, for what it's worth, as far as I remember, if we want to save characters, the last | at the end of the line is not mandatory (as well as the space before the first one).

[affeldt-aist]

I'm lost, didn't we said that bullet lists would be easier to use?

Yes, but also that we should try to use tables when reasonable.

[proux01]

Did we converge on some "definition" of reasonable?

[affeldt-aist]

Did we converge on some "definition" of reasonable?

I think that "unreasonable" was implicitly defined as "when formatting is too painful because there are many RHS that require several lines each"

[affeldt-aist]

Mmmhhh, I am concerned by the fact that the source file is much less readable.
In https://github.com/math-comp/analysis/blob/master/classical/classical_sets.v, we only used a table to format a summary of the documentation, and then providing the full documentation in verbatim centered lists (this was really just a test).
What about doing the same here? (LaTeXified digest at the top, and full doc in ASCII.)

[affeldt-aist]

The last commit has restored the detailed documentation and kept the table as well, which acts a a digest of the detailed documentation: this provides an overview of the documentation while keeping the source code file readable.

[affeldt-aist]

arg, the last commit was rejected, looks I do not have the rights to push @yoshihiro503

[affeldt-aist]

@yoshihiro503 I PRed to your PR instead