diff options
author | Son Ho | 2023-10-24 16:15:38 +0200 |
---|---|---|
committer | Son Ho | 2023-10-24 16:15:38 +0200 |
commit | b2cbbb48494e8079eb000293e7734850e4ce3d05 (patch) | |
tree | 152b3c93f3908a97c0334c64429c1746093d1016 | |
parent | 9ddd174959970f87658191034b70d0cfa02ff451 (diff) |
Fix a printing issue with scalar values
Diffstat (limited to '')
-rw-r--r-- | compiler/Extract.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index bf90a411..0260b78b 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -862,10 +862,12 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* We need to add parentheses if the value is negative *) if sv.PV.value >= Z.of_int 0 then F.pp_print_string fmt (Z.to_string sv.PV.value) - else + else if !backend = Lean then + (* TODO: parsing issues with Lean because there are ambiguous + interpretations between int values and nat values *) F.pp_print_string fmt - ("(" ^ Z.to_string sv.PV.value - ^ if !backend = Lean then ":Int" else "" ^ ")"); + ("(-(" ^ Z.to_string (Z.neg sv.PV.value) ^ ":Int))") + else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")"); (match !backend with | Coq -> let iname = int_name sv.PV.int_ty in |