diff options
Diffstat (limited to 'riscv/riscv_extras.lem')
| -rw-r--r-- | riscv/riscv_extras.lem | 5 |
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 |