racket - 判决中的离奇合同违反

Question

我有judgement以下合同：

(define-judgment-form DynamicLam
  #:mode     (down I I O O)
  #:contract (down Γ e Γ e)

  [----------------"Lambda"
   (down Γ_0 z_0 Γ_0 z_0)]
  ;; rest of the code ...
)

当我运行这个：

(define empty (term ()))
(redex-match? DynamicLam Γ empty)
(redex-match? DynamicLam e lam1^*)
(redex-match? DynamicLam z lam1^*)
(judgment-holds (down empty lam1^* empty lam1^*))

我回来了：

#t

#t

#t

. . down：判断输入值与其合约不匹配；（由_表示的未知输出值）合约：（down Γ e Γ e）值：（down empty lam1^* _ _）

但这没有意义，因为我redex-match?上面明明用过来测试：

• 那empty匹配Γ
• 那lam1^*匹配e
• 而且那lam1^*匹配z。

我错过了什么？#:contract除了匹配之外，还有更多的含义Γ e Γ e吗？

Answer 1

我通过改变#:modeto(down I I I I)而不是(down I I O O)和改变解决了这个问题

(judgment-holds (down empty lam1^* empty lam1^*))

至

(judgment-holds (down ,empty ,lam1^* ,empty ,lam1^*))

这种,变化对我来说很有意义，但我仍然不明白为什么需要将两个输出作为输入，所以如果有人可以编辑这个答案来解释这一点，或者提供评论或另一个解释这个微妙之处的答案，那将是极好的。