> 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
