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

No they are just special instances of 'side' but I think for all of these keywords would be better. 


On Aug 29, 2012, at 5:54 PM, Robby Findler wrote:

> 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.
>> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4373 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20120829/6f2512bb/attachment.p7s>