using judgment-holds within define-relation

[dvanhorn]

I wrote this program, whose behavior surprised me:

#lang racket/base
(require redex/reduction-semantics)
(define-language L)

;; the empty relation
(define-relation L
  empty ⊆ any
  [(empty any)
   (where #t #f)])

(test-equal (judgment-holds (empty 0)) #f)

;; x in wat if x in empty, so wat should be empty...
(define-relation L
  wat ⊆ any
  [(wat any)
   (judgment-holds (empty any))])

(test-equal (judgment-holds (wat 0)) #f) ; but it's not!

The problem here is that the grammar for define-relation in the docs says you can use metafunction-extras, which is what I'm doing in the wat definition, but doing so doesn't seem to have any effect and the wat relation contains everything instead of nothing.

If I replace (judgment-holds (empty any)) with (empty any), it works as expected, but I don't see why the original shouldn't work as well. Note sure if this is a bug, a documentation bug, or my own misunderstanding.

[rfindler]

Thanks for this extremely clear bug report!