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 and
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 wit
2 matches
Mail list logo