[isabelle] Syntax

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.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.