diff options
Diffstat (limited to 'lib/coq/Sail2_operators_mwords.v')
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index cca52c1d..9b5888c7 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -396,9 +396,9 @@ val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*) (* TODO: check/redefine behaviour on out-of-range n *) -Definition shiftl {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift w (Z.to_nat n)) v. -Definition shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift w (Z.to_nat n)) v. -Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta w (Z.to_nat n)) v. +Definition shiftl {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift' w (Z.to_nat n)) v. +Definition shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift' w (Z.to_nat n)) v. +Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta' w (Z.to_nat n)) v. (* Definition rotl := rotl_bv Definition rotr := rotr_bv |