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

[Tobias Nipkow]

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
> 

-------------- 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/20180118/3bc8a8d4/attachment.bin>