feat: allow limiting the number of binders in delabConstWithSignature

[eric-wieser]

Read this section before submitting

• Ensure your PR follows the External Contribution Guidelines.
• Please make sure the PR has excellent documentation and tests. If we label it missing documentation or missing tests then it needs fixing!
• Include the link to your RFC or bug issue in the description.
• If the issue does not already have approval from a developer, submit the PR as draft.
• The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
• For feat/fix PRs, the first paragraph starting with "This PR" must be present and will become a changelog entry unless the PR is labeled with no-changelog. If the PR does not have this label, it must instead be categorized with one of the changelog-* labels (which will be done by a reviewer for external PRs).
• A toolchain of the form leanprover/lean4-pr-releases:pr-release-NNNN for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing release-ci on its own line.
• If you rebase your PR onto nightly-with-mathlib then CI will test Mathlib against your PR.
• You can manage the awaiting-review, awaiting-author, and WIP labels yourself, by writing a comment containing one of these labels on its own line.
• Remove this section, up to and including the --- before submitting.

---

This PR allows restricting the number of binders to place before the colon when using delabConstWithSignature.

This allows extract_goal in mathlib to (somewhat) respect the currently-reverted variables.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 64b35a8c194da9f36329ee2b5d04e0e757f8c553 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-15 16:01:25)

[kmill]

I might suggest that extract_goals could wrap the target type in some metadata instead. That should block delabConstWithSignature, since it looks for exact forallE's.

[eric-wieser]

Indeed, I have an alternate patch which does just that :).