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
Description: S/MIME Cryptographic Signature