fix: allow generalization in let

[eric-wieser]

As suggested by @kmill, removing an unnecessary let (possibly only there in the first place for copy/paste reasons) seems to fix the included test.

This makes ~q() matching in quote4 noticeably more useful in things like norm_num (as it fixes leanprover-community/quote4#29)

It also makes a quote4 bug slightly more visible (leanprover-community/quote4#30), but the bug there already existed anyway, and isn't caused by this patch.

Fixes #3065

[eric-wieser]

awaiting-review

[leanprover-community-mathlib4-bot]

• 💥 Mathlib branch lean-pr-testing-3060 build failed against this PR. (2023-12-15 15:16:57) View Log
• 💥 Mathlib branch lean-pr-testing-3060 build failed against this PR. (2023-12-15 15:37:43) View Log
• ✅ Mathlib branch lean-pr-testing-3060 has successfully built against this PR. (2023-12-15 23:44:56) View Log
• ✅ Mathlib branch lean-pr-testing-3060 has successfully built against this PR. (2023-12-16 01:12:40) View Log
• ✅ Mathlib branch lean-pr-testing-3060 has successfully built against this PR. (2024-01-04 02:58:22) View Log
• 🟡 Mathlib branch lean-pr-testing-3060 build this PR didn't complete normally. (2024-01-23 21:03:00) View Log
• ✅ Mathlib branch lean-pr-testing-3060 has successfully built against this PR. (2024-01-25 12:27:16) View Log

[eric-wieser]

@semorrison, is there any hope of this landing in the 4.5.0 release?

[kim-em]

@semorrison, is there any hope of this landing in the 4.5.0 release?

I'm sorry, this didn't make it.

[eric-wieser]

And just to check I understand the rc process, the fact this missed 4.5.0rc1 means it certainly will miss any future rcs?

[kim-em]

And just to check I understand the rc process, the fact this missed 4.5.0rc1 means it certainly will miss any future rcs?

Well, hopefully it can make v4.6.0-rc1!

The status of rc2 is still a bit up in the air. If there is really substantial demand (like 10 maintainers have +1'd a post saying that Mathlib wants something asap), I think we're open to cutting a rc2 solely for the sake a new features. But the preference is that we only make rc2 when there is a bad problem that needs fixing.

[eric-wieser]

If rc2 happens it would be great if this could land in it, but certainly this PR isn't important enough to justify rc2 existing!

[kim-em]

@Kha, I know @eric-wieser is keen to get this in, as it will enable new uses of Qq in writing tactic (positivity) extensions in Mathlib. As it touches do notation I think it needs review from you.

[Kha]

It looks like a strict improvement to me but I'll give @leodemoura a chance to look at it as well since he wrote the code. In general we haven't gone back to the do code in a long time so it's not a good time for any larger changes (which this one isn't).

[eric-wieser]

@Kha, if Leo doesn't have the time, are you comfortable merging this without his approval?

[Kha]

Ok, I still don't see any possible downsides