[racket-dev] Am I misusing judgment-holds ?

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))