Merge pull request #82 from AeneasVerif/son/switch

Improve tuple projections and matches over integers in Lean

1 files changed, 6 insertions, 2 deletions

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")