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
MichaelOn 6 Oct 2015, at 23:12, Makarius <makar...@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-...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
