我们可以在Coq中定义递归定义吗？

问题描述

我知道Coq允许定义相互递归的归纳类型。但是有没有办法在Coq中编写递归定义？

例如，我想将定义写为：

DeFinition myDeFinition A := forall B C,(myDeFinition B) \/ (A = C).

上面定义中的重要部分是 myDeFinition B ，它在另一个参数上递归调用相同的定义。是否可以在Coq中做到这一点？

解决方法

您可以使用Fixpoint代替Definition。如果您想了解更多关于documentation的信息，建议您看看。

Fixpoint myDefinition A := 
  forall B C,(myDefinition B) \/ (A = C).

请注意，上述类似内容不会被Coq接受，因此是有效的定义。 documentation应该再次说明您可以使用示例或不可以使用示例。