From 1ba26f5c815509911965b6f90f75e8f8cc3c0417 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Wed, 8 Feb 2023 20:21:42 -0800
Subject: WIP

---
 compiler/Extract.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index a2ad37f5..c90d2170 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1809,7 +1809,8 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
           match !backend with
           | FStar -> "="
           | Coq -> ":="
-          | Lean -> if monadic then "<-" else ":="
+          (* TODO: switch to ⟵ once issues are fixed *)
+          | Lean -> if monadic then "←" else ":="
         in
         F.pp_print_string fmt eq;
         F.pp_print_space fmt ();
@@ -1867,6 +1868,8 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       (* Open a box for the [if e] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       F.pp_print_string fmt "if";
+      if !backend = Lean then
+        F.pp_print_string fmt " h:";
       F.pp_print_space fmt ();
       let scrut_inside = PureUtils.texpression_requires_parentheses scrut in
       extract_texpression ctx fmt scrut_inside scrut;
@@ -1924,7 +1927,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       F.pp_open_hovbox fmt ctx.indent_incr;
       (* Print the [match ... with] *)
       let match_begin =
-        match !backend with FStar -> "begin match" | Coq | Lean -> "match"
+        match !backend with FStar -> "begin match" | Coq -> "match" | Lean -> "match h:"
       in
       F.pp_print_string fmt match_begin;
       F.pp_print_space fmt ();
@@ -2647,7 +2650,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
           F.pp_print_space fmt ();
           F.pp_print_string fmt "()");
         F.pp_print_space fmt ();
-        F.pp_print_string fmt "=";
+        F.pp_print_string fmt "==";
         F.pp_print_space fmt ();
         let success = ctx_get_variant (Assumed Result) result_return_id ctx in
         F.pp_print_string fmt ("." ^ success ^ " ())"));
-- 
cgit v1.2.3