diff options
Diffstat (limited to 'mppa_k1c/ExtValues.v')
| -rw-r--r-- | mppa_k1c/ExtValues.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 32d84b60..284d55f3 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -201,4 +201,7 @@ Proof. Qed. Definition addx sh v1 v2 := - Val.add v2 (Val.shl v1 (Vint sh)).
\ No newline at end of file + Val.add v2 (Val.shl v1 (Vint sh)). + +Definition addxl sh v1 v2 := + Val.addl v2 (Val.shll v1 (Vint sh)).
\ No newline at end of file |