[racket] (where-not ...) in Redex

Where is a binding form.

Did you mean #:when and #:unless to be binding forms or not?

Robby

On Wed, Aug 29, 2012 at 4:49 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> Good enough. I thought of using 'where' but 'side' is better.
>
>
> On Aug 29, 2012, at 5:46 PM, Robby Findler wrote:
>
>> (define-judgment-form L
>>  #:mode (-> I O)
>>  [(-> e v)
>>   (side-condition (positive-nat v))
>>   ---------------------------
>>   (foo e bar e_1) -> (v e_1)]
>>
>> (define-metafunction L
>>  [(positive-nat natural) ,(> (term natural) 0)]
>>  [(positive-nat any) #f])
>>
>> Then, you'd override the typesetting of calls to positive-nat to put
>> whatever unicode fanciness you wanted there instead.
>