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

The ! suffix #406

Open
leodemoura opened this issue Apr 14, 2021 · 0 comments
Open

The ! suffix #406

leodemoura opened this issue Apr 14, 2021 · 0 comments
Labels
refactoring Code refactoring
Milestone
4.0.0-m4

Comments

@leodemoura
Copy link
Member

Andrew Kent pointed out we were using the ! for both macros and functions that may panic at runtime.
We decided to use it only for functions that panic, and have started making the changes, but we still have to-do items.

  • The string interpolation notations are still using !.
  • Some functions that may panic at runtime still don't have !.
  • Add a[i]! notation for array access that may panic at runtime
@leodemoura leodemoura added the refactoring Code refactoring label Apr 14, 2021
@gebner gebner mentioned this issue Dec 23, 2021
Closed
@leodemoura leodemoura added this to the 4.0.0-m4 milestone Jan 17, 2022
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
@gebner @digama0
chore: bump to 2022-09-11 (leanprover#406)
dd1ecc5 
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
refactoring Code refactoring
Projects
None yet
Milestone
4.0.0-m4
Development

No branches or pull requests
1 participant
@leodemoura