Re: [racket-users] PLT Redex: how to falsify the judgment in define-judgment-form

I think this boils down to a question about how redex executes judgment forms. Leaving aside modeless judgment forms (where redex will only check a derivation for you but won't ever make them up), redex is turning each judgment form into a (fancy) function from the inputs to sets of the outputs

[racket-users] PLT Redex: how to falsify the judgment in define-judgment-form

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