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

[Tobias Nipkow]

On 07/10/2015 00:37, Michael Norrish wrote:
> 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 ( * ).

Of course, "( * )" is ok. The only reason I have been a little wary of "(*)" is 
that people who are unaware of comments inside formulas would be totaly confused 
by the syntax error they get. But if your HOL4 experience suggests that this is 
not an issue, I would be in favour of "(sym)".

Tobias

> 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.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151011/dcef9d5f/attachment.bin>