There are a number of different points here.

- What is good style depends on what your math look like. Knuth writes nice
traditional math, whereas Isabelle proof states can get quite ugly. In such
cases I find that operator names on the next line improves readability,
independent of what the operator is. However, unless there is significant
support, I won't press for a uniform change.

- The issue of multiple line breaks in the current unparsing of long formulas
like _ + _ + _ + _ + _ + _ is independent and very annoying. I would be
surprised if we wanted anything but fill every line, not just the first or last
one as happens right now. A solution of that one would be much appreciated.

- I also noticed that "=" is still at the end of the line while "<=" and
friends are at the beginning. That is indeed inconsistent, also with
traditional notation. I agree with Larry and am strongly in favour of
changing that.


On 11/01/2018 13:20, Lawrence Paulson wrote:
On 10 Jan 2018, at 21:26, Makarius <> wrote:

The Haskell community appears to have picked up a lot of such (slightly
odd) styles from Lamport. E.g. they put commas at the start of the line
instead of the end, which is typographically very strange.

I was educated by the original TeX Book, which in turn refers to the
top-quality mathematical typesetting from around 1900. Here the
operators and commas are in the traditional position: end of line.

I got in the habit of putting arithmetic operators at the start of a line while 
at university, having made too many errors from forgetting that the symbol at 
the end of the previous line was a minus sign. Of course, that consideration 
doesn't apply to commas, and it's amazing that Lamport (and Dijkstra?) managed 
to persuade people to adopt such crazy conventions.

Interactive theorem proving isn't the same thing as solving physics problems by 
hand, so I'm not against having operators at the end of the line if that's what 
people think would be best. Note however that the equals sign is an infix 
operator and is invariably put at the start of a line, never at the end.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to