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
