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

On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> I would almost prefer the use of 'when' for 'where' and the introduction of 'unless'.

If we did this, then there could be no judgment-forms name 'when' or
'unless', which makes me think we shouldn't do this.

> The type setting of 'when' could still use 'where' as the English word (and perhaps we can have a way to override it).
>
> I am not sure how to type set 'unless' other than by providing a the negative operator as an argument !=

Using \neq{} seems right to me.

Robby

> -- Matthias
>
>
>
>
> On Aug 22, 2012, at 3:47 PM, Asumu Takikawa wrote:
>
>> 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
>> ____________________
>>  Racket Users list:
>>  http://lists.racket-lang.org/users
>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>