define-term in pattern position

[wilbowma]

I usually think of any term being allowed in pattern position and simply acting as "unify with this".

I think of define-term as simply introducing a meta-variable that means literally the term being defined.

However, both of these mental models are broken when combined:

(require redex/reduction-semantics)
(define-language L)
(define-term T true)
> (redex-match? L true (term T))
#t
> (redex-match? L T (term true))
#f
> (define-judgment-form L
    #:mode (eval I O)
    [(eval true true)])
> (judgment-holds (eval T true))
#t
> (judgment-holds (eval T T))
#f

Is there a reason? Could this be supported?

[rfindler]

That would indeed be better, in this example (and many many similar ones), but the full ramifications of that seem quite subtle. It might be easy to do this but it might also be hard. I'll try to take a look.