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
