Commit 2026-05-10 01:42 47e40c50
View on Github →feat: arbitrary-order induction on Nat (#38442)
This can be used as e.g.
induction n using stepInduction 3 with
| base n hn => ...
| step n ih => ...
The test file's examples are from a term project I did for an NUS module taught by Olivier Danvy himself.