summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/Extract.ml8
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