> On 10 Jan 2018, at 21:26, Makarius <makar...@sketis.net> wrote:
> The Haskell community appears to have picked up a lot of such (slightly
> odd) styles from Lamport. E.g. they put commas at the start of the line
> instead of the end, which is typographically very strange.
> I was educated by the original TeX Book, which in turn refers to the
> top-quality mathematical typesetting from around 1900. Here the
> operators and commas are in the traditional position: end of line.
I got in the habit of putting arithmetic operators at the start of a line while
at university, having made too many errors from forgetting that the symbol at
the end of the previous line was a minus sign. Of course, that consideration
doesn't apply to commas, and it's amazing that Lamport (and Dijkstra?) managed
to persuade people to adopt such crazy conventions.
Interactive theorem proving isn't the same thing as solving physics problems by
hand, so I'm not against having operators at the end of the line if that's what
people think would be best. Note however that the equals sign is an infix
operator and is invariably put at the start of a line, never at the end.
isabelle-dev mailing list