Idris case/induction tactics

Question

They were implemented in Idris 0.9.14 and I successfully used induction for some proofs. However, they work only for some library types; while, for example, Vect supports them, nearly-isomorphic All does not:

-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

Unfortunately there isn't plenty of language documentation, and I couldn't find how to implement elimination/case analysis for custom types. Digging into Prelude, I found the %elim modifier, but it didn't help. Could anybody give an example for, say, the aforementioned All?

Answer 1

The induction tactic can only be used on types that were declared with %elim. Some people feel that Idris should be automatically generating eliminators whenever possible, but there would appear to be some technical difficulties with that.

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

As far as I can tell, there should be no problem adding %elim to the definition of All (just edit the file Quantifiers.idr and recompile idris). You may want to submit a pull request on Github.