+ An Attempt to Find Consensus about Indenting Rules for Mizar

Block Rules

proof, now, hereby, suppose, case should increase indentation, end; should decrease it, OK? How about per cases? - has no matching end;

Formula Indenting

Please submit your tips.

Labels

Should be at the left margin? If so, if they are after a keyword like assume or consider, where should be that keyword?

Top level items

Top level items (theorem, definition, etc.) now increase indentation, but only some of them have matching "end;". Should proofs inside them start from zero indent, or increase their indent?

References

Spaces after commas or not? space between ":' and "def"?

Then, Hence

beginning or end of line?

-- JosefUrban - 19 Apr 2004