<br><br>On Sunday, August 26, 2012, Matthias Felleisen  wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
On Aug 25, 2012, at 10:53 PM, Robby Findler wrote:<br>
<br>
&gt; On Thu, Aug 23, 2012 at 8:11 AM, Matthias Felleisen<br>
&gt; &lt;<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;matthias@ccs.neu.edu&#39;)">matthias@ccs.neu.edu</a>&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt; I would almost prefer the use of &#39;when&#39; for &#39;where&#39; and the introduction of &#39;unless&#39;.<br>
&gt;<br>
&gt; If we did this, then there could be no judgment-forms name &#39;when&#39; or<br>
&gt; &#39;unless&#39;, which makes me think we shouldn&#39;t do this.<br>
<br>
I don&#39;t understand this point at all.<br>
<br></blockquote><div><br></div><div>See the docs for define-judgement-form and imagine a judgment-form whose name was &quot;unless&quot;. You&#39;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">

<br>
&gt;&gt; The type setting of &#39;when&#39; could still use &#39;where&#39; as the English word (and perhaps we can have a way to override it).<br>
&gt;&gt;<br>
&gt;&gt; I am not sure how to type set &#39;unless&#39; other than by providing a the negative operator as an argument !=<br>
&gt;<br>
&gt; Using \neq{} seems right to me.<br>
<br>
What if you want \not\in or \not\subtype and such?<br>
<br></blockquote><div><br></div><div>You can&#39;t use where or unless for such things already. Either that or I don&#39;t understand you?<span></span></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

-- Matthias<br>
<br>
<br>
<br>
<br>
&gt;<br>
&gt; Robby<br>
&gt;<br>
&gt;&gt; -- Matthias<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; On Aug 22, 2012, at 3:47 PM, Asumu Takikawa wrote:<br>
&gt;&gt;<br>
&gt;&gt;&gt; Hi all,<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Had a question/feature request for Redex. In various models, I&#39;ve<br>
&gt;&gt;&gt; encountered situations where I wanted the dual behavior to the<br>
&gt;&gt;&gt; (where pattern term) clause of Redex (i.e., does term *not* match this<br>
&gt;&gt;&gt; pattern).<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; In the past, I&#39;ve used side-conditions or where clauses with predicate<br>
&gt;&gt;&gt; metafunctions for this case. For example,<br>
&gt;&gt;&gt; (side-condition ,(not (redex-match ...)))<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; or<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; (where #f (matches this that))<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Both of these have the disadvantage that it&#39;s more work to typeset.<br>
&gt;&gt;&gt; It would be convenient to have a form like<br>
&gt;&gt;&gt; (where-not pattern term)<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; that would typeset like the following:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; where term ≠ pattern<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; This seems like a common enough pattern that it would be nice to support<br>
&gt;&gt;&gt; it as a built-in (and typeset) construct. Does that seem like a<br>
&gt;&gt;&gt; reasonable thing to add?<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Cheers,<br>
&gt;&gt;&gt; Asumu<br>
&gt;&gt;&gt; ____________________<br>
&gt;&gt;&gt; Racket Users list:<br>
&gt;&gt;&gt; <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; ____________________<br>
&gt;&gt;  Racket Users list:<br>
&gt;&gt;  <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br>
&gt;&gt;<br>
<br>
</blockquote>