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