Relationship between induction and catamorphisms

Stream: new members

[Andre Popovitch]

It seems to me that induction is basically just the recursion scheme catamorphism. Is that actually the case? If so, are there tactics for the other recursion schemes?

[Eric Wieser]

I don't know the category theory to answer your question fully, but note that there is an induction x using some_custom_scheme variant of the induction tactic.

[Stuart Presnell]

I don’t know what we already have, but it might be interesting to try implementing other revision schemes as in, e.g. Hinze, Wu & Gibbons “Unifying Structured Recursion Schemes”

[Eric Taucher]

For those looking for the paper "Unifying Structured Recursion Schemes" by Hinze, Wu & Gibbons (pdf)