Have sign_extend in common Sail Lem library, use it and zero_extend in

mono rewrites

1 files changed, 0 insertions, 5 deletions

diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index fb4f7f31..491dd56d 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -51,11 +51,6 @@ let get_slice_int len n lo =
   let bits = bits_of_int (hi + 1) n in
   of_bits_failwith (subrange_list false bits hi lo)
 
-val sign_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
-let sign_extend v len = exts_vec len v
-val zero_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
-let zero_extend v len = extz_vec len v
-
 val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
 let shift_bits_right v m = shiftr v (uint m)
 val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a