3

它们在 Idris 0.9.14 中实现，我成功地用于induction一些证明。但是，它们仅适用于某些库类型；例如，虽然Vect支持它们，但几乎同构All不支持：

-Main.h2> induction ys1 INTERNAL ERROR: induction needs an eliminator for Data.Vect.Quantifiers.All
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

不幸的是，没有大量的语言文档，而且我找不到如何为自定义类型实现消除/案例分析。深入研究 Prelude，我找到了%elim修饰符，但没有帮助。有人可以举个例子All吗？

4

1 回答 1

3

该induction策略只能用于以 . 声明的类型%elim。有些人认为 Idris 应该尽可能自动生成消除器，但这似乎存在一些技术困难。

任何人都可以举一个例子，比如前面提到的 All 吗？

%elim据我所知，添加到定义应该没有问题All（只需编辑文件Quantifiers.idr并重新编译idris）。您可能想在 Github 上提交拉取请求。

于 2014-12-17T20:22:11.260 回答