归纳定义产生 "Ignoring recursive call"
Inductive definition yields "Ignoring recursive call"
我有一个归纳定义，它在求值后打印出警告 "Ignoring recursive call"。看起来这个定义工作得很好。但是，我仍然很好奇为什么会给出这个警告。下面是一个最小的例子。
Inductive testor :=
| Constr1 : list testor -> testor
| Constr2 : testor -> testor.
我认为罪魁祸首是第一个构造函数中的 list testor。另一方面，如果没有第二个构造函数，则不会给出警告。
Q: 为什么会发出警告？这是否意味着对归纳定义施加了限制？
我正在使用 Coq 8.5。
由于 list testor 的出现，类型 testor 被称为 嵌套归纳类型 。没有限制，你可以放心使用定义，只是自动生成的归纳原理不是很有用。 Coq-club thread 处理这个问题。以下是 Adam Chlipala 的回答摘录：
The warning is just about the heuristic attempts to generate a useful
induction principle. Nested inductive types (like your [AllList] use
here) call for some cleverness to build the right inductive case schemas.
有关详细信息，请参阅 CPDT this chapter 中的 "Nested Inductive Types" 部分。
我有一个归纳定义，它在求值后打印出警告 "Ignoring recursive call"。看起来这个定义工作得很好。但是，我仍然很好奇为什么会给出这个警告。下面是一个最小的例子。
Inductive testor :=
| Constr1 : list testor -> testor
| Constr2 : testor -> testor.
我认为罪魁祸首是第一个构造函数中的 list testor。另一方面，如果没有第二个构造函数，则不会给出警告。
Q: 为什么会发出警告？这是否意味着对归纳定义施加了限制？
我正在使用 Coq 8.5。
由于 list testor 的出现，类型 testor 被称为 嵌套归纳类型 。没有限制，你可以放心使用定义，只是自动生成的归纳原理不是很有用。 Coq-club thread 处理这个问题。以下是 Adam Chlipala 的回答摘录：
The warning is just about the heuristic attempts to generate a useful induction principle. Nested inductive types (like your [AllList] use here) call for some cleverness to build the right inductive case schemas.
有关详细信息，请参阅 CPDT this chapter 中的 "Nested Inductive Types" 部分。