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

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