Re: [isabelle] Confusing behavior of a paired set comprehension



On Thu, 5 Apr 2012, Brian Huffman wrote:

It might be possible to set up an ML parse translation for tuple abstractions (see section "Tuple syntax" in Product_Type.thy for how things are implemented now). The parse translation could produce a syntax error if any variable names are repeated.

I'm not sure whether it would be worth the trouble to implement it, though, unless more people ask for it.

Changing ML parse translations is always a very delicate process, and actually ongoing for several years. Instead of added new features, there is presently an attempt to make case syntax conceptually sound, possibly also list comprehensions.

This is motivated again by the IDE markup, because that reveals tiny conceptual mishaps in the existing syntax.


	Makarius





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