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.


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 ==>

and especially

        foo ==> bar ==>

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.


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

isabelle-dev mailing list

Reply via email to