Macros/operations in abstract syntax

[PeterLjunglof]

Specifying a list in abstract syntax is cumbersome: (ConsA a (ConsA b (BaseA c)))

Simpler would be (ListA3 a b c), where ListAn is series of macros (which is autogeneraded, just as ConsA and BaseA):

oper ListA1 : A -> [A] = \a -> BaseA a;
oper ListA2 : A -> A -> [A] = \a,b -> ConsA a (BaseA b);
oper ListA3 : A -> A -> A -> [A] = \a,b,c -> ConsA a (ConsA b (BaseA c));
...

Overloading would make it even simpler, but perhaps that's too difficult

There are also other circumstances, but this is what I thought of now.