lean4
lean4 copied to clipboard
The `!` suffix
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