summaryrefslogtreecommitdiff
path: root/compiler/ExtractBase.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/ExtractBase.ml')
-rw-r--r--compiler/ExtractBase.ml8
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")