From f4e2c2bb09d9d7b54afc0692b7f690f5ec2eb029 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 22 Sep 2023 17:27:54 +0200
Subject: Add Lean extraction of shl/shr

---
 compiler/Extract.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index c4238d83..61856f0a 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -472,7 +472,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
   (match (!backend, binop) with
   | HOL4, (Eq | Ne)
   | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt)
-  | Lean, (Div | Rem | Add | Sub | Mul) ->
+  | Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr) ->
       let binop =
         match binop with
         | Eq -> "="
@@ -486,6 +486,8 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
         | Add -> "+"
         | Sub -> "-"
         | Mul -> "*"
+        | Shl -> "<<<"
+        | Shr -> ">>>"
         | _ -> raise (Failure "Unreachable")
       in
       let binop =
-- 
cgit v1.2.3