[racket] Multiple ellipses after judgment form premises?

From: Jonathan Schuster (schuster at ccs.neu.edu)
Date: Thu Feb 6 14:59:11 EST 2014

Right, that's exactly what I've done so far. It's just strange that this
doesn't match up with the usual intuition for ellipses in Racket.
Enhancement for the next release, perhaps?


On Thu, Feb 6, 2014 at 2:52 PM, Robby Findler
<robby at eecs.northwestern.edu>wrote:

> Not really.
>
> You can do it like this, tho.
>
> #lang racket
> (require redex/reduction-semantics)
>
> (define-language L)
>
> (define-judgment-form L
>   #:mode (is-number I)
>   #:contract (is-number any)
>   [(side-condition ,(number? (term any)))
>    ----------------
>    (is-number any)])
>
> (define-judgment-form L
>   #:mode (nested-number-list I)
>   #:contract (nested-number-list any)
>   [(where (any_2 ...) (any_1 ... ...))
>    (is-number any_2) ...
>    ------------------------
>    (nested-number-list ((any_1 ...) ...))])
>
> (judgment-holds (nested-number-list ((1 2 3) (4 5 6) (7 8 9))))
>
>
> On Thu, Feb 6, 2014 at 1:44 PM, Jonathan Schuster <schuster at ccs.neu.edu>wrote:
>
>> Is there a reason that judgments in Redex don't allow multiple ellipses
>> after a premise? I have a case where I have a list of lists of items, and I
>> want to check that a certain property holds on each item. Here's a very
>> simplified example:
>>
>> (define-language L)
>>
>> (define-judgment-form L
>>   #:mode (is-number I)
>>   #:contract (is-number any)
>>   [(side-condition ,(number? (term any)))
>>    ----------------
>>    (is-number any)])
>>
>> (define-judgment-form L
>>   #:mode (nested-number-list I)
>>   #:contract (nested-number-list any)
>>   [(where ((any_item ...) ...) any_list)
>>    (is-number any_item) ... ...
>>    ------------------------
>>    (nested-number-list any_list)])
>>
>> (judgment-holds (nested-number-list ((1 2 3) (4 5 6) (7 8 9))))
>>
>> ____________________
>>   Racket Users list:
>>   http://lists.racket-lang.org/users
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140206/8cd3fd3d/attachment-0001.html>

Posted on the users mailing list.