Hi, Racketeers

Since Redex can calculate all possible results in the judgment, Can I add 
some negative premise to help derive the output? like

(define-judgment-form Lambda
#: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 racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 

Reply via email to