[racket] (where-not ...) in Redex

From: Asumu Takikawa (asumu at ccs.neu.edu)
Date: Wed Aug 22 15:47:06 EDT 2012

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

In the past, I've used side-conditions or where clauses with predicate
metafunctions for this case. For example,
  (side-condition ,(not (redex-match ...)))


  (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?


Posted on the users mailing list.