Commit 2024-06-08 02:35 acd84d3d
View on Github →feat: basic Vector.inductionOn API (#13616)
Also make the case names slightly nicer for when using the syntax:
induction v using Vector.inductionOn with
| nil => sorry
| cons ih => sorry
feat: basic Vector.inductionOn API (#13616)
Also make the case names slightly nicer for when using the syntax:
induction v using Vector.inductionOn with
| nil => sorry
| cons ih => sorry