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

is actually much more readable than

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

        foo ==> bar ==>

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.


isabelle-dev mailing list

Reply via email to