我正在尝试使用Program Fixpoint在 Coq 中实现 STLC 的依赖类型评估器。由于该语言没有定点运算符，我认为评估器应该终止，尽管终止条件不是结构性的。
在我的开发过程中，我发现一个令人头疼的原因是我根本无法同时跟踪太多变量，而且模式匹配太嵌套了。
如果只是一Fixpoint，我可以用战术来实施身体，但是当使用Program Fixpoint或Function时，我就是不能。在这种情况下，有什么技巧可以用战术来建立身体吗？
我被困在最后：https://gist.github.com/HuStmpHrrr/0d92e646916ae9ec7ced3ff21724ba2d
使用Program时，您只需使用校样模式为要填写的术语部分留下下划线即可。任何可以推断的下划线将自动填写，其余的将产生义务。例如，可以在证明模式下编写所有run，方法是编写Program Fixpoint run ... {measure ...} := _.度量值将显示为要在上下文中run的参数。