Zulip Chat Archive

Stream: lean4

Topic: banning `!` suffix from keywords

view this post on Zulip Leonardo de Moura (Mar 13 2021 at 02:19):

@Andrew Kent and @Joe Hendrix pointed out that we were using ! inconsistently. It was used in functions that may invoke "panic", macros and builtin notation . So, we decided to remove ! suffix from all macros, but panic!, assert!, and unreachable! since they are just syntax sugar on top of panic. We are also enforcing the use of snake_case for keywords. For example, natLit! is now called nat_lit.

Last updated: May 07 2021 at 12:15 UTC