lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

The `!` suffix

Open leodemoura opened this issue 3 years ago • 0 comments

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 avatar Apr 14 '21 14:04 leodemoura