Hi,
I have a simple data type based on strings:
val _ = Datatype `Label = name string | coname string`;
Is is possible to set up pretty-printing (or gammar) rules, such that:
1. The term `` `a` `` can be interpreted as `` name “a” ``
2. The term`` -`a` `` can be interpreted as `` coname “a” ``
There’s no great way to do this at the moment, because it’s not possible to
have all the things that are possible inside string literals (e.g., \n) appear
in other contexts. My inclination would be overload n to name, and to overload
unary negation to coname, and then you could write
n"a" an
