fix: make cdot anonymous function notation handle ambiguous notation

Open kmill opened this issue 1 year ago • 1 comments

Fixes an issue where each alternative in choice nodes would get their own arguments. Now cdot function expansion is aware of choice nodes.

Also modifies the variable naming so that multi-argument functions like (· + ·) expand as fun x1 x2 => x1 + x2 rather than fun x x_1 => x + x_1.

Closes #4832

Jul 25 '24 21:07 kmill

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-4833 built against this PR, but testing failed. (2024-07-25 22:32:09) View Log
✅ Mathlib branch lean-pr-testing-4833 has successfully built against this PR. (2024-07-25 23:01:39) View Log
✅ Mathlib branch lean-pr-testing-4833 has successfully built against this PR. (2024-07-25 23:43:22) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 30cf3bb3bfdac33a7ab385b25e0d262e0e3d8599 --onto dd6ed124baef64a26ef5860f49597fdcef371239. (2024-08-09 21:26:01)

Jul 25 '24 22:07 leanprover-community-mathlib4-bot