feat: `_` separators in numeric literals

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

Open kmill opened 23 hours ago

kmill commented 23 hours ago

This PR allows _ in numeric literals as a separator. For example, 1_000_000, 0xff_ff or 0b_10_11_01_00.

Closes #6199

leanprover-community-bot commented 21 hours ago

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-6204 has successfully built against this PR. (2024-11-25 01:35:48) View Log