Thanks for this discussion. Although I agree with Larry and Andreas, it is clear that there is no concensus. Hence there will be no blanket change of where line breaks go for infix operators.

Tobias

On 16/01/2018 17:34, Blanchette, J.C. wrote:

This sort of claim needs to be justified by evidence. We had it the first way 
until the late 1990s. I changed it to the other way while working on large 
proof states connected with crypto protocols. It seemed more readable to me for 
such proofs.

I was taught at school to avoid starting every sentence with "I think" or "I 
believe", since obviously whatever I say is my opinion, but since this apparently leads to 
confusion, I'll happily relativize my previous statement: Just as you found one style more readable 
than another (without giving any evidence), *I* find

        foo ==>
        bar

and especially

        foo ==> bar ==>
        baz

much more readable than the alternative, because they yield less opportunities for what 
Bryan Garner (Modern Am. E. Usage) refers to as "miscues" when parsing. When I 
read the alternative, I get the same effect as when I listen to the Murder City Devils 
and they sing

        God knows she's pretty
        messed up

I don't think there's a need for a big empirical study to observe the miscue; 
it should be easily reproducible by any left-to-right reader. By the same 
token, I can understand that in the presence of [| ... |], the opposite 
convention has its benefits (as stressed by Andreas).

One more case: Suppose you have

        foo ==>
        bar ==> baz

Notice how the break falls naturally where you would insert the parentheses:

        foo ==>
        (bar ==> baz)

Compare with

        foo ==> (bar
        ==> baz)

So I will be apologized, surely, for preferring the end-of-line treatment for 
operators that bind to the right, while realizing that I might be in the 
minority on this mailing list.

Jasmin


Attachment: 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

Reply via email to