I'm working on defining a language which has casts and subtyping as follows:
(define-language base
(t ::= int any)
(e ::= number (cast t e))
#| stuff ... |#)
I then define the following judgment form over it:
(define-judgment-form base
#:mode (<: I I)
#:contract (<: t t)
[------
(<: t t)]
[------
(<: int any)])
And now, in my reduction relation, I want to write something like
(define b-> (reduction-relation base
(--> (cast t v)
v
(where-judgment-holds (<: (typeof v) t)))))
Where we assume that (typeof v) returns the type of the value v. As far as I can tell, there isn't anything like where-judgment-holds 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.
What you are looking for actually is called judgment-holds, and it works in your example exactly where you put where-judgment-holds:
(define b-> (reduction-relation base
(--> (cast t v)
v
(judgment-holds (<: (typeof v) t)))))