algebraic-data-types - idris 案例/归纳策略

Question

它们在 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 吗？

Answer 1

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

Could anybody give an example for, say, the aforementioned All?

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