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

[Blanchette, J.C.]

> On 11 Jan 2018, at 16:44, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> 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.

Short version: I would generally support such a change if it excludes operators that bind to the right, especially => and ==>.

Long version: My impression is that people like to have "boring" operators on the right and "interesting" ones on the left. Boring operators include "=" on lists, conjunction for logical formulas, cons and append for lists, and + for numbers. Oh, I was about to forget the absolutely most boring operator of all: commas in lists. There's a reason why commas on the left look so revolting (even if the convention has some advantages).

If you're playing with lists or strings, then # and @ will tend to be boring operators, and something like

	"blah blah blah " @ my_file_name @
	" blah blah"

will feel quite natural; there's usually no need to draw attention to the @. Ditto for commas in lists.

In logic, often conjunction is a boring connective, but one could argue that there is no "default" connective (logic being so subtle) and they should all be displayed prominently, on the left, Lamport-style (possibly without the leading bullet-like conjunction on the first line), to prevent any misreadings.

However, for operators like ==>, which bind on the right,

	foo ==>
	bar

is actually much more readable than

	foo
	==> bar

When reading the first line, "foo ==>", we immediately see that something is missing, and that "foo" has negative polarity. In the second version, "foo" looks positive, until one reads "==> bar". Things get even worse when you have either

	foo ==> bar ==>
	baz

which is good, or

	foo ==> bar
	==> baz

which really looks like "foo implies bar" until you keep reading.

> - 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 agree.

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

This might be an instance of the boring vs. non-boring phenomenon. There is, I guess, a strong tradition for the statu quo, but were it to be changed, then "=" should be the one that goes on the left. Given that "=" is used perhaps 10 times more often than "<=" and friends, this could turn out to be more distracting than the current inconsistency.

Jasmin