[isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

[Michael Norrish]

HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax fixities.  I don't think HOL Light supports comments at this level.  HOL4 does, using SML's (* ... *).  So, if you want to write the escaped *, you have to use our older syntax for the same (using a $ for "op": $*), or you can just add spaces and write ( *), or ( * ).

Michael

> On 6 Oct 2015, at 23:12, Makarius <makarius at sketis.net> wrote:
>
> 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.
>
>
>       Makarius_______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.