Skip to content

Pre/post &mut argument: remove future in favor of old #773

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.

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

Open
W95Psp opened this issue Jul 15, 2024 · 4 comments
Open

Pre/post &mut argument: remove future in favor of old #773

W95Psp opened this issue Jul 15, 2024 · 4 comments
Labels
engine Issue in the engine enhancement New feature or request needs-triage Mark an issue that needs triage: add label, add more contents

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented Jul 15, 2024

  • make the proc macro parse both ::hax_lib::_final and _final
  • detect if (locally) there is any name clash, and ask the user to use ::hax_lib::_final instead

We chatted about that, and we'll adopt the style of Verus / Prusti / Rustc proposal: use old to refer to the old value, and otherwise that's the future value.

@W95Psp W95Psp added enhancement New feature or request engine Issue in the engine labels Jul 15, 2024
@W95Psp W95Psp changed the title Pre/post &mut argument: rename future to _final Pre/post &mut argument: remove future in favor of old Jul 18, 2024
Copy link

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

@github-actions github-actions bot added the stale label Sep 17, 2024
@W95Psp
Copy link
Collaborator Author

W95Psp commented Sep 18, 2024

Still something we want, we need to schedule it before too much code is written in that style.

@W95Psp W95Psp removed the stale label Sep 18, 2024
Copy link

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

@github-actions github-actions bot added the stale label Nov 18, 2024
@W95Psp
Copy link
Collaborator Author

W95Psp commented Nov 18, 2024

I'll bump priority for that one, it's still important to get that done soon.

@W95Psp W95Psp removed the stale label Nov 18, 2024
@franziskuskiefer franziskuskiefer added the needs-triage Mark an issue that needs triage: add label, add more contents label Jan 9, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
engine Issue in the engine enhancement New feature or request needs-triage Mark an issue that needs triage: add label, add more contents
Projects
None yet
Development

No branches or pull requests

2 participants