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 <ro...@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 <schus...@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 >> >> >
____________________ Racket Users list: http://lists.racket-lang.org/users
