These are not errors, technically. The side-condition form in a judgment-form is not unquoted, so that's a redex expression, not a Racket one. In other words, the side-condition is not (/ 1 0), but '(/ 1 0). Ditto for the "different" example.
Or perhaps you're already getting that and you're saying that side-conditions in judgment-forms should insist on receiving booleans? I see that the current behavior for side-condition was first released more than a year ago, so I'm a bit worried about backwards compatibility. What do you think about that? Robby On Tue, Sep 3, 2013 at 9:10 PM, Eric Tanter <etan...@dcc.uchile.cl> wrote: > Hi, > > Strangely, `side-condition' matches when the associated expression fails > with an error. > > For instance, using the redex tutorial example, if one writes: > > [(types Γ x_1 t_1) > (side-condition (/ 1 0)) > ------------------------------------ > (types (x_2 : t_2 Γ) x_1 t_1)] > > Then the rule applies, as if it was (side-condition #t). > > Of course, (/ 1 0) is not really realistic, but the same happens if one > writes: > > [(types Γ x_1 t_1) > (side-condition (different x_1 x_2)) > ------------------------------------ > (types (x_2 : t_2 Γ) x_1 t_1)] > > and forgets to define `different' (assuming it is a standard Redex > metafunction)... Instead of a nice error that `different' is undefined, the > rule silently applies. > > 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? > > Cheers, > > -- Éric > > ____________________ > Racket Users list: > http://lists.racket-lang.org/users >
____________________ Racket Users list: http://lists.racket-lang.org/users
