feat: consistent elaboration of tactic `have ... by`

Open Kha opened this issue 1 year ago • 2 comments

This implements a much smaller version of #4610: we make sure that any tactic have ... by does not allow postponing mvars in the type, but do not change any other have

Jul 02 '24 09:07 Kha

(seems to have created some issues with partial syntax trees in the test. Resolving this is not highest prio for me at the moment)

Jul 03 '24 08:07 Kha

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-4626 has successfully built against this PR. (2024-07-03 09:50:13) View Log

Jul 03 '24 09:07 leanprover-community-mathlib4-bot