Formatting section headers

Alexander van der Vekens

unread,

Mar 21, 2021, 5:21:26 AM3/21/21

to Metamath

Recently, Benoît performed some reformattings of the section headers in set.mm. It seems that there are the following (hidden) conventions:

* two empty lines before a section header (after a theorem)

* indentation of the section header comment by two spaces

If these are/shall become official conventions, they should be documented in section "Conventions" (which does not, by the way, obey the second rule).

Benoit

unread,

Mar 21, 2021, 6:57:25 AM3/21/21

to Metamath

I was aiming for consistency with what seemed most common, maybe a bit too obsessively ! I hope this did not create merge conflicts with your recent PR.

Whatever is decied, I can add it to ~conventions.

Benoît

Alexander van der Vekens

unread,

Mar 21, 2021, 10:55:26 AM3/21/21

to Metamath

The conventions are fine for me (they can/should be added to the ~conventions if nobody objects) , and I had only a small merge conflict ;-).

Alexander

Zheng Fan

unread,

Mar 24, 2021, 4:49:50 PM3/24/21

to Metamath

So is it specified somewhere that the header of each hierarchy of sections has two specific repeating patterns around the section name?

David A. Wheeler

unread,

Mar 24, 2021, 5:02:03 PM3/24/21

to Metamath Mailing List

> On Mar 24, 2021, at 3:04 PM, Zheng Fan <fanzhe...@outlook.com> wrote:
>
> So is it specified somewhere that the header of each hierarchy of sections has two specific repeating patterns around the section name?

Yes, it’s in the Metamath book section 4.1.1 on page 140 (see “Headings”).

You can also see this by running metamath.exe & saying “help write theorem_list”.

--- David A. Wheeler

Benoit

unread,

Mar 25, 2021, 6:21:55 AM3/25/21

to Metamath

Thanks Alexander and David. I'm going to add something to it to ~conventions.

Benoît

Reply all

Reply to author

Forward