diff options
| author | Aymeric Fromherz | 2023-09-22 17:27:54 +0200 |
|---|---|---|
| committer | Aymeric Fromherz | 2023-09-22 17:27:54 +0200 |
| commit | f4e2c2bb09d9d7b54afc0692b7f690f5ec2eb029 (patch) | |
| tree | bc8104aa03e77cc69deb3accf237351b95940a67 | |
| parent | a5f87ba02342ae0b96fe0d8ba16f1ec78469d760 (diff) | |
Add Lean extraction of shl/shr
| -rw-r--r-- | compiler/Extract.ml | 4 |
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 = |