From e1e888f23935bfb34830fe160593e09df75a7f20 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 08:03:37 +0100
Subject: Update the code generation

---
 compiler/ExtractBase.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'compiler/ExtractBase.ml')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index db887539..5aa8323e 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -782,9 +782,13 @@ let ctx_get_termination_measure (def_id : A.FunDeclId.id)
 let unop_name (unop : unop) : string =
   match unop with
   | Not -> (
-      match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~")
+      match !backend with
+      | FStar -> "not"
+      | Lean -> "¬"
+      | Coq -> "negb"
+      | HOL4 -> "~")
   | Neg (int_ty : integer_type) -> (
-      match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg")
+      match !backend with Lean -> "-." | _ -> int_name int_ty ^ "_neg")
   | Cast _ ->
       (* We never directly use the unop name in this case *)
       raise (Failure "Unsupported")
-- 
cgit v1.2.3