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

On Sunday, August 26, 2012, Matthias Felleisen wrote:

>
> On Aug 25, 2012, at 10:53 PM, Robby Findler wrote:
>
> > On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen
> > <matthias at ccs.neu.edu <javascript:;>> 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.
>
> I don't understand this point at all.
>
>
See the docs for define-judgement-form and imagine a judgment-form whose
name was "unless". You'll notice a conflict in the premise grammar.


>
> >> 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.
>
> What if you want \not\in or \not\subtype and such?
>
>
You can't use where or unless for such things already. Either that or I
don't understand you?


> -- Matthias
>
>
>
>
> >
> > 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
> >>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120826/4b23e5de/attachment.html>