On Sunday, August 26, 2012, Matthias Felleisen wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> On Aug 25, 2012, at 10:53 PM, Robby Findler wrote: > On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen > <<a href="javascript:;" onclick="_e(event, 'cvml', 'matthias@ccs.neu.edu')">matthias@ccs.neu.edu</a>> 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. </blockquote><div> </div><div>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. </div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> >> 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? </blockquote><div> </div><div>You can't use where or unless for such things already. Either that or I don't understand you?</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> -- 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: >>> <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a> >> >> >> ____________________ >> Racket Users list: >> <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a> >> </blockquote>