[isabelle] flatten of tuples


Is it possible to have a semantic construct which works like

(a,b,c,d) @ (x,y,z) = (a,b,c,d,x,y,z)

for tuples of arbitrary lengths.
The elements a, b, ... should be of different types,
but they are not tuples.

I can also work with a version which has a terminator like:

(a,b,c,d,()) @ (x,y,z,()) = (a,b,c,d,x,y,z,())

If this is not possible at the semantic level, is it possible
to have a syntactic construct?

Best regards,

Viorel Preoteasa

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