[racket] [redex] side-condition matching upon errors
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