Zulip Chat Archive
Stream: lean4
Topic: underscores in numeric literals?
Alok Singh (Jan 24 2024 at 07:41):
Of the many possible syntax sugars, I was surprised lean doesn't have this.
Like 1_000 for 1,000 or 1.000
Last updated: May 02 2025 at 03:31 UTC