racket - 从约简关系中调用判断

我正在定义一种具有强制转换和子类型化的语言，如下所示：

(define-language base
  (t ::= int any)
  (e ::= number (cast t e))
  #| stuff ... |#)

然后，我在其上定义以下判断形式：

(define-judgment-form base
   #:mode (<: I I)
   #:contract (<: t t)
   [------
    (<: t t)]
   [------
    (<: int any)])

现在，在我的归约关系中，我想写一些像

(define b-> (reduction-relation base
    (--> (cast t v)
         v
         (where-judgment-holds (<: (typeof v) t)))))

我们假设(typeof v)返回值v的类型。据我所知，在Redex库中没有类似where-judgment-holds的东西，虽然我可以用unquote解决它，但是如果Redex内置了一些东西，那就太好了。

最佳答案

您实际上要查找的是judgment-holds，它在示例中的确切位置是where-judgment-holds：

(define b-> (reduction-relation base
    (--> (cast t v)
         v
         (judgment-holds (<: (typeof v) t)))))