> On 11 Jan 2018, at 16:44, Tobias Nipkow <nip...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev