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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/25e4ec2e-ba34-4a53-8284-37cbac422ae2n%40googlegroups.com.
