Re: [isabelle] flatten of tuples



An operator such as your @ seems unlikely to exist, because its operands would not have fixed types. What you mean by âsyntactic constructâ isnât clear, unless you never need to write a thing like x at y.

I imagine that you cannot use lists because you need a variety of types. But is there is no possibility of creating a super type for them?

Larry Paulson


> On 27 Feb 2015, at 02:09, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote:
> 
> Hello,
> 
> 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.