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
