[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Tobias Nipkow]

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 <makarius at 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180111/4366f90f/attachment.bin>