У меня есть отношение, определенное в PLT Redex, которое принимает два входа и выхода.
(define-judgment-form
L
#:mode (Meet I I O)
[---------------------------
(Meet xpr xpr xpr)]
)
По другому мнению, я хотел бы иметь в качестве побочного условия, что не существует никакоговыход для двух заданных входов.Я попытался сформулировать это следующим образом:
(side-condition (empty? (judgment-holds (Meet xpr1 xpr2 xpr3) xpr3)))
т.е. xpr1 и xpr2 являются связанными входными данными из предпосылки суждения, а xpr3 является метавариабельной величиной для вывода.
но я получаю следующую ошибку:
term: judgment forms with output mode ("O") positions disallowed
Есть ли способ выразить это побочное условие, что для определенного набора входов, для суждения, не определены выходные данные?