I have a lot of sets in my semantics, which I've been representing as a list (myset element ...).
I define helper metafunctions for sets and typeset them. Is this a good way to do it?
I'm thinking of writing a helper library for using redex with sets.
I could imagine writing a macro that defines a bunch of set helpers for you, as well as providing a bunch of rewrites for use in with-compound-rewriter
That could work nicely. I've long thought that sets should be built into Redex's pattern matcher. That is, if someone uses curly braces instead of parens around a (syntax) sequence then it should turn out to be a set instead of a sequence. But I've not found the time to really do it. (The other one that I've long thought would be nice to have is maps but the notation isn't as obvious.)
The one thing I'd worry about is set-builder notation. I'm not sure how far you'd get without it and I'm not sure how well it would integrate.
Building it into redex and using curly braces would be pretty cool and better than my library, but a lot more effort.
Yeah, set-builder notation sounds a bit tricky. I do have one place where I have a custom-formatted metafunction that uses set-builder notation, but it doesn't generalize to a library like my other set helpers.