summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorAymeric Fromherz2023-09-22 17:27:54 +0200
committerAymeric Fromherz2023-09-22 17:27:54 +0200
commitf4e2c2bb09d9d7b54afc0692b7f690f5ec2eb029 (patch)
treebc8104aa03e77cc69deb3accf237351b95940a67 /compiler
parenta5f87ba02342ae0b96fe0d8ba16f1ec78469d760 (diff)
Add Lean extraction of shl/shr
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml4
1 files changed, 3 insertions, 1 deletions
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 =