diff options
Diffstat (limited to 'compiler/ExtractBase.ml')
| -rw-r--r-- | compiler/ExtractBase.ml | 8 |
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") |