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

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Wed Aug 29 17:49:17 EDT 2012

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/fddbd7ca/attachment.p7s>

Posted on the users mailing list.