JovanGerb 11aff52fb1 fix: abstractNestedProofs should see into the head of an application (#7353) ... This PR changes `abstractNestedProofs` so that it also visits the subterms in the head of an application. This oversight caused some definitions in mathlib to have unabstracted proofs, such as [CategoryTheory.StructuredArrow.commaMapEquivalenceInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.html#CategoryTheory.StructuredArrow.commaMapEquivalenceInverse) Mathlib [bench](https://github.com/leanprover-community/mathlib4/pull/22613#issuecomment-2704288815): build instructions -0,166 % lint instructions -0.72 % This speedup comes from files containing `CategoryTheory.Functor`, which contains beta unreduced expressions, where abstracting proofs used to not happen. Zulip: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/dsimp.20simplifies.20proofs.2C.20which.20is.20slow/near/503630173		2025-03-06 20:08:38 +00:00
..
bench	perf: optimize sorry detection in unused variables linter (#7129)	2025-02-22 16:43:39 +00:00
compiler	feat: cleanup of get and back functions on List/Array (#7059)	2025-02-17 01:43:45 +00:00
elabissues
ir
lean	fix: abstractNestedProofs should see into the head of an application (#7353)	2025-03-06 20:08:38 +00:00
pkg	feat: debug_assert! (#7256)	2025-03-03 16:34:44 +00:00
playground
plugin
simpperf
.gitignore
bv_relation.lean	fix: bv_decide structures pass instantiate mvars (#7309)	2025-03-03 21:27:53 +00:00
common.sh
lean-toolchain