Since Redex can calculate all possible results in the judgment, Can I add
some negative premise to help derive the output? like
#:mode (infer I O)
[(infer A B)
*(not (infer number B)*
(Infer C B)]
I tried to replace bold line with (side-condition (not (judgment-holds
(infer number B, which is disallowed in Redex since B is in the output
So any standard way to express this intention?
more concrete example is in
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
To view this discussion on the web visit