Coq：与 InteractionTrees 库中的 [mrec] 相互递归定义

Question

我正在学习 这个伟大的库，用于在 Coq 中表示递归和不纯程序

我在相互递归方面遇到问题（文档中的第一个示例给了我一个错误） https://deepspec.github.io/InteractionTrees/5.0.0/ITree.Interp.Recursion.html#mrec

Inductive D : Type -> Type :=
| Even : nat -> D bool
| Odd : nat -> D bool.

Definition def : D ~> itree (D +' void1) := fun _ d =>
  match d with
  | Even n => match n with
              | O => ret true
              | S m => ITree.trigger (Odd m)
              end
  | Odd n => match n with
             | O => ret false
             | S m => ITree.trigger (Even m)
             end
end. 

这是我遇到的错误

Error:
In environment
T : Type
d : D T
n : nat
m : nat
The term "ITree.trigger (Odd m)" has type "itree (D +' void1) ?T0"
while it is expected to have type
 "itree (D +' void1) ?T@{T0:=T; T1:=bool}" (cannot satisfy constraint
"D bool" == "(D +' void1) ?T0").

我应该怎么做才能解决这个问题？

顺便说一句，我设法使用库的 [Interp] 模块的通用 [rec] 接口来定义单个递归函数（没有错误，没有问题，教程中给出了工作示例（Introduction.v 文件）） 。但我找不到更通用的 [mrec] 的工作示例，它允许多个相互递归的定义。

谢谢你。

Answer 1

将

ITree.trigger

（未超载）替换为

trigger

（超载）。