<div dir="ltr">These are not errors, technically. The side-condition form in a judgment-form is not unquoted, so that&#39;s a redex expression, not a Racket one. In other words, the side-condition is not (/ 1 0), but &#39;(/ 1 0). Ditto for the &quot;different&quot; example. <div>
<br></div><div>Or perhaps you&#39;re already getting that and you&#39;re saying that side-conditions in judgment-forms should insist on receiving booleans?</div><div><br></div><div>I see that the current behavior for side-condition was first released more than a year ago, so I&#39;m a bit worried about backwards compatibility. What do you think about that?</div>
<div><br></div><div>Robby</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Sep 3, 2013 at 9:10 PM, Eric Tanter <span dir="ltr">&lt;<a href="mailto:etanter@dcc.uchile.cl" target="_blank">etanter@dcc.uchile.cl</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
Strangely, `side-condition&#39; matches when the associated expression fails with an error.<br>
<br>
For instance, using the redex tutorial example, if one writes:<br>
<br>
  [(types Γ x_1 t_1)<br>
   (side-condition (/ 1 0))<br>
   ------------------------------------<br>
   (types (x_2 : t_2 Γ) x_1 t_1)]<br>
<br>
Then the rule applies, as if it was (side-condition #t).<br>
<br>
Of course, (/ 1 0) is not really realistic, but the same happens if one writes:<br>
<br>
  [(types Γ x_1 t_1)<br>
   (side-condition (different x_1 x_2))<br>
   ------------------------------------<br>
   (types (x_2 : t_2 Γ) x_1 t_1)]<br>
<br>
and forgets to define `different&#39; (assuming it is a standard Redex metafunction)... Instead of a nice error that `different&#39; is undefined, the rule silently applies.<br>
<br>
I understand that anything that is not #f is true, but arguably this should not apply to an error. Or is there a good reason why this is so?<br>
<br>
Cheers,<br>
<br>
-- Éric<br>
<br>
____________________<br>
  Racket Users list:<br>
  <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br>
</blockquote></div><br></div>