Invoke judgment from from within reduction-relation
<p>I'm working on defining a language which has casts and subtyping as follows:</p>

<pre><code>(define-language base 
  (t ::= int any) 
  (e ::= number (cast t e)) 
  #| stuff ... |#)
</code></pre>

<p>I then define the following judgment form over it:</p>

<pre><code>(define-judgment-form base
   #:mode (&lt;: I I)
   #:contract (&lt;: t t)
   [------ 
    (&lt;: t t)]
   [------ 
    (&lt;: int any)])
</code></pre>

<p>And now, in my reduction relation, I want to write something like </p>

<pre><code>(define b-&gt; (reduction-relation base
    (--&gt; (cast t v)
         v
         (where-judgment-holds (&lt;: (typeof v) t)))))
</code></pre>

<p>Where we assume that <code>(typeof v)</code> returns the type of the value <code>v</code>. As far as I can tell, there isn't anything like <code>where-judgment-holds</code> in the Redex library, and while I can work around it with an unquote, it would be nice if there was something built into Redex.</p>