Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
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 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
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
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 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
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
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
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
>> Personally I would appreciate some move here, but this only makes sense >> if we agree what the goal is and whether it is worth the effort. > 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. Ditto. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
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. Tobias On 22/09/2015 16:21, Florian Haftmann wrote: The »op •« is infamous. Whatever you wish instead (my personal favorite being no special syntax at all), problems include a) to detect unintended printing behaviour b) a suitable migration mechanisms Concerning b), one you could imagine things like a) alternative declarations (infix(l/r)_new beside infix(l/r), infix(l/r) beside infix(l/r)_old) b) a flag to control the semantics of infix(l/r) c) a flag combined with a data slot to modify existing mixfix declarations afterwards also Personally I would appreciate some move here, but this only makes sense if we agree what the goal is and whether it is worth the effort. Cheers, Florian ___ 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
Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]
Is there a consensus that there is a problem with this notation? Having no special syntax might work, especially with jEdit, where one can click on an unexpected constant to see what it refers to. Larry > On 22 Sep 2015, at 15:21, Florian Haftmann > wrote: > > The »op •« is infamous. Whatever you wish instead (my personal favorite > being no special syntax at all), problems include > a) to detect unintended printing behaviour > b) a suitable migration mechanisms > > Concerning b), one you could imagine things like > a) alternative declarations (infix(l/r)_new beside infix(l/r), > infix(l/r) beside infix(l/r)_old) > b) a flag to control the semantics of infix(l/r) > c) a flag combined with a data slot to modify existing mixfix > declarations afterwards also > > Personally I would appreciate some move here, but this only makes sense > if we agree what the goal is and whether it is worth the effort. > > Cheers, > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
