fix: handle reordered indices in structural recursion

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 428 forks source link

fix: handle reordered indices in structural recursion #6116

Closed nomeata closed 1 week ago

nomeata commented 1 week ago

This PR fixes a bug where structural recursion did not work when indices of the recursive argument appeared as function parameters in a different order than in the argument's type's definition.

Fixes #6015.

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-6116 has successfully built against this PR. (2024-11-18 11:30:07) View Log
✅ Mathlib branch lean-pr-testing-6116 has successfully built against this PR. (2024-11-18 12:10:09) View Log