Compiling is an option. Even if I want syntax that resembles the written form of the data structures, a simple lang-extension like the at-reader would be enough.
Ideal syntax for abstract variables would just be a and g instead of alpha and gamma. Standalone abstract variables would not be interesting: typing something like @[a 1] is no more convenient than (a 1)...
Ideal syntax for abstract atoms would be like now. Something like @[...] could assume atoms. in the absence of wedges.
Ideal syntax for abstract functions would be the same. Would have to do something like alpha-f instead, though.
Ideal syntax for multi would dispense with cruft as much as possible: specify the multi ID once, automatically infer composite indices in the pattern and in the constraints. Use semicolon to separate pattern and constraints or use wedge instead of comma inside the pattern.
Ideal syntax for conjunctions could use a wedge: DrRacket makes them easy to input.
Also need something to interpret full evaluations. Abstract atom -> {.../...;.../...} seems acceptable.
For concrete data structures, gamma might be interesting. Does not have to be perfectly symmetrical if it makes things easier to write.
gamma[upper-case-symbol] could, for instance, be expanded to a variable
assumption of atom as the default, conjunction in the case of wedge, gamma-f would work. concrete multi could have atom syntax, just assume multi is excluded as an atom symbol.
Compiling is an option. Even if I want syntax that resembles the written form of the data structures, a simple lang-extension like the at-reader would be enough.