Allow underscores in numeric literals (and in field/destructor names that are written as numeric strings). The

underscores have no semantic meaning, but can help a human parse the numbers.

1 files changed, 17 insertions, 0 deletions

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 2bff422f..d8ff3989 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -210,3 +210,20 @@ module GhostLetExpr {
     G(5, xyz)

   }

 }

+

+class DigitUnderscore_Names {

+  // the following would be the same integers, but they are different fields

+  var 0_1_0: int;

+  var 010: int;

+  var 10: int;

+  // ... as we see here:

+  method M()

+    modifies this;

+  {

+    this.0_1_0 := 007;

+    this.010 := 000_008;

+    this.10 := 0x0000_0009;

+    assert this.0_1_0 == int(00_07.0_0) && this.010 == 8 && this.10 == 9;

+    this.10 := 20;

+  }

+}