Вызвать суждение изнутри редукционного отношения

Question

Я работаю над определением языка, который имеет приведение типов и подтипы следующим образом:

(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, Насколько я могу сказать, нет ничего подобного where-judgment-holds в библиотеке Redex, и хотя я могу обойти это без кавычек, было бы неплохо, если бы в Redex было что-то встроенное.

Answer 1

То, что вы ищете на самом деле называется judgment-holdsи это работает в вашем примере именно там, где вы положили where-judgment-holds:

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