Email Gateway (Aug 22 2022 at 17:12): Email Gateway (Aug 22 2022 at 17:12):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Isabelle Users,
Many years ago I introduced the syntax "[x <- xs. b]" for "filter (%x. b) xs".
At the time I made it output syntax as well, which means that certain filter
expressions would be displayed in that syntax, which can confuse users
unfamiliar with it. Thus I have recently restricted it to input syntax. I am
undecided whether to remove it completely or not:
It complicates the syntax
(although I don't think it gives rise to ambiguities)
It is an ad hoc extension of list comprehension (which we also support as
input syntax)
However, it is quite concise and readable and I have recently seen a close
relative in some book.
Let me know in case you feel strongly about it one way or the other.
Tobias
smime.p7s
Last updated: Apr 25 2024 at 08:20 UTC