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 position. So any standard way to express this intention? more concrete example is in https://github.com/juniorxxue/applicative-intersection-semantics/blob/main/definition.rkt#L94 Regards Xu -- 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 https://groups.google.com/d/msgid/racket-users/25e4ec2e-ba34-4a53-8284-37cbac422ae2n%40googlegroups.com.
