[racket] (where-not ...) in Redex
Hi all,
Had a question/feature request for Redex. In various models, I've
encountered situations where I wanted the dual behavior to the
(where pattern term) clause of Redex (i.e., does term *not* match this
pattern).
In the past, I've used side-conditions or where clauses with predicate
metafunctions for this case. For example,
(side-condition ,(not (redex-match ...)))
or
(where #f (matches this that))
Both of these have the disadvantage that it's more work to typeset.
It would be convenient to have a form like
(where-not pattern term)
that would typeset like the following:
where term ≠ pattern
This seems like a common enough pattern that it would be nice to support
it as a built-in (and typeset) construct. Does that seem like a
reasonable thing to add?
Cheers,
Asumu