Well-founded induction

Stream: general

[Simon Hudon]

There's a cool trick with induction where you can specify an induction principle with using my_type.rec_on. It does not seem to work for well_founded.induction. Does anyone know why?

[Mario Carneiro]

The best thing I can say about the induction using feature is that it exists

[Mario Carneiro]

It almost never works the way you would expect