关闭Coq中的自动归纳原理
关闭Coq中的自动归纳原理
提问于 2018-08-06 08:13:05
我定义了一个嵌套归纳数据类型，并为它定义了一个自定义归纳原则。然而，来自我正在使用的库的自动化策略(具体地说，用于de Bruijn索引的DBLib )期望归纳是基于通常的归纳原理的。既然我从来没有打算使用最初生成的归纳原理，那么有没有办法替代自动生成的原理呢？或者，如果没有，有没有办法暂时关闭这种自动生成？
回答 1
Stack Overflow用户
回答已采纳
发布于 2018-08-06 16:36:15
您可以使用Elimination Schemes选项来完成此操作。例如,
Unset Elimination Schemes.
Inductive nat_tree : Set :=
| NNode' : nat -> list nat_tree -> nat_tree.
Set Elimination Schemes.此外，如果您有一个更简单的(非递归)归纳类型，则可以使用Variant关键字来使Coq不生成归纳原则：
Variant foo : Type := Foo.页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/51699205
复制相关文章
相似问题
腾讯云开发者
