Oh, this variation may also be a better fit for what you want, depending (note changed mode).
Robby #lang racket (require redex) (define-language L (e integer true false) (τ bool int)) (define-judgment-form L #:mode (⊢ I I) #:contract (⊢ e τ) [(⊢ integer int)] [(⊢ true bool)] [(⊢ false bool)]) (define-metafunction L [(type-checks? e τ) ,(judgment-holds (⊢ e τ))]) (term (type-checks? true int)) (term (type-checks? true bool)) _________________________ Racket Developers list: http://lists.racket-lang.org/dev
