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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and