This is kind of awkward, tho. Do you plan to typeset this portion of your model?
Robby On Wed, Aug 22, 2012 at 10:07 AM, Stephen Chang <stch...@ccs.neu.edu> wrote: > Oh yeah, this first solution should work (I want to keep it as an > output though). Thanks. > > > On Wed, Aug 22, 2012 at 9:01 AM, Robby Findler > <ro...@eecs.northwestern.edu> wrote: >> You could do the below, but can you say a little bit more about what >> the metafunction and judgment-form you want to combine are? >> (Presumably they both are type checking?) >> >> #lang racket >> (require redex) >> >> (define-language L >> (e integer true false) >> (τ bool int)) >> >> (define-judgment-form L >> #:mode (⊢ I O) >> #:contract (⊢ e τ) >> [(⊢ integer int)] >> [(⊢ true bool)] >> [(⊢ false bool)]) >> >> (define-metafunction L >> [(type-checks? e τ) >> ,(member (term τ) (judgment-holds (⊢ e τ) τ)) >> (side-condition (printf "τ = ~a\n" (term τ)))]) >> >> (term (type-checks? true int)) >> (term (type-checks? true bool)) _________________________ Racket Developers list: http://lists.racket-lang.org/dev
