Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: make cdot anonymous function notation handle ambiguous notation #4833

Merged
merged 4 commits into from
Aug 9, 2024
Merged

fix: make cdot anonymous function notation handle ambiguous notation #4833

merged 4 commits into from
Aug 9, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Jul 25, 2024

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

@kmill kmill mentioned this pull request Jul 25, 2024
Closed
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 25, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 25, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4833
1d63856
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 25, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4833
10e33be
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases labels Jul 25, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jul 25, 2024 •
edited
Loading

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)

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jul 25, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4833
5165f15
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4833
430e1bd
kmill added 3 commits August 9, 2024 10:54
@kmill
fix: make cdot anonymous function notation handle ambiguous notation
68ef095 
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 leanprover#4832
@kmill
simplify implementation
54ec1ca
@kmill
adjust module doc in test
8e9a913
@kmill kmill marked this pull request as ready for review August 9, 2024 18:10
@kmill kmill enabled auto-merge August 9, 2024 18:10
@kmill kmill added this pull request to the merge queue Aug 9, 2024
Merged via the queue into leanprover:master with commit 95bf679 Aug 9, 2024
21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

cdot function notation fails to macro expand properly when there is ambiguous syntax
2 participants
@kmill @leanprover-community-mathlib4-bot