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. Tobias On 11/01/2018 13:20, Lawrence Paulson wrote:
On 10 Jan 2018, at 21:26, Makarius <makar...@sketis.net> 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. Larry
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
