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

[Blanchette, J.C.]

> 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