Merge pull request #602 from hacspec/better-error-message-for-464

fix(engine/f*): better error for #464
cryspen · Apr 15, 2024 · 02936d9 · 02936d9
2 parents e8140e4 + 4bbeac0
commit 02936d9
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -127,13 +127,16 @@ struct
           | S32 -> Int32
           | S64 -> Int64
           | S128 ->
-              Error.unimplemented
+              Error.unimplemented ~issue_id:464
                 ~details:
-                  "128 literals (fail if pattern maching, otherwise TODO)" span
+                  "Matching on u128 or i128 literals is not yet supported." span
           | SSize ->
-              Error.unimplemented
+              Error.unimplemented ~issue_id:464
                 ~details:
-                  "usize literals (fail if pattern maching, otherwise TODO)"
+                  "Matching on usize or isize literals is not yet supported. \
+                   As a work-around, instead of `match expr { 0 => ... }`, \
+                   please cast for instance to `u64` before: `match expr as \
+                   u64 { 0 => ... }`."
                 span
         in
         F.Const.Const_int