为什么精益强制递归类型参数出现在非递归参数之后？
为什么精益强制递归类型参数出现在非递归参数之后？
提问于 2017-01-21 04:42:09
以下定义被精益拒绝：
inductive natlist
| nil : natlist
| cons: natlist → ℕ → natlist使用错误消息，“natlist.cons的arg #2不是递归的，但它发生在递归参数之后”。
并如预期的那样接受以下定义：
inductive natlist
| nil : natlist
| cons: ℕ → natlist → natlist勒恩执行这个命令的原因是什么？
回答 1
Stack Overflow用户
回答已采纳
发布于 2017-01-21 09:50:48
精益的归纳类型的实现是基于P. Dybjer (1994)的“归纳家族”的论文：
Backhouse Bac88和Coquand和Paulin COP90允许在非递归前提之前进行不必要的概括。我更喜欢将所有非递归前提放在递归前提之前，因为前者不能在这里依赖后者(但情况在Dyb92中发生了变化)。这一限制简化了方案的提出，并强调了与良好秩序的关系。
注意，最近的提交取消了这个限制，您的第一个定义现在生效了。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/41775816
复制相关文章
相似问题
腾讯云开发者
