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, 14 insertions, 0 deletions

diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs
index bc4017c0..f9421659 100644
--- a/Source/Dafny/Util.cs
+++ b/Source/Dafny/Util.cs
@@ -68,6 +68,20 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

+    /// Returns s but with all occurrences of '_' removed.

+    /// </summary>

+    public static string RemoveUnderscores(string s) {

+      Contract.Requires(s != null);

+      while (true) {

+        var j = s.IndexOf('_');

+        if (j == -1) {

+          return s;

+        }

+        s = s.Substring(0, j) + s.Substring(j + 1);

+      }

+    }

+

+    /// <summary>

     /// For "S" returns S and false.

     /// For @"S" return S and true.

     /// Assumes that s has one of these forms.