[isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
makarius at sketis.net
Tue Oct 6 14:12:10 CEST 2015
On Tue, 22 Sep 2015, Tobias Nipkow wrote:
> The "op" noation is idiosyncratic, but there are examples (not in
> individual formulae) where I find some such notation convenient. I would
> welcome Haskell's "(+)", but that has a problem with "(*)". Unless we
> can make that notation work, I don't think we profit much by a change.
> Hence I am inclined to leave things as they are.
"(*)" does not work, because it is in conflict with "(* comment *)" in
inner syntax. I have recently encountered a situation where it would have
been better to replace inner comments by "-- ‹comment›", as known in outer
syntax, but the double-minus was in conflict with some infix operators.
The next idea was to replace "-- ‹comment›" by "— ‹comment›" with a newly
introduced Isabelle symbol for the mdash.
So many clouds of dust, caused by trying to clean up obscure corners ...
At the moment I am also inclined to leave things unchanged.
More information about the isabelle-dev