diff options
| author | Brian Campbell | 2019-05-29 19:09:45 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-05-29 19:11:09 +0100 |
| commit | 1308bdc1fd4785e37f00e4436b2cd9f4c8e8fad7 (patch) | |
| tree | 3dd4f8c96d9dbbf3a730f79879a2171eb94a8de0 /lib/arith.sail | |
| parent | 9e60c03133b28dc177ef1f11c60a362a2125efa7 (diff) | |
Coq: need a proof for _shr32
Diffstat (limited to 'lib/arith.sail')
| -rw-r--r-- | lib/arith.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 1950080a..d04c7988 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -70,7 +70,7 @@ val _shl_int = "shl_int" : (int, int) -> int overload shl_int = {_shl8, _shl32, _shl_int} -val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)} +val _shr32 = {c: "shr_mach_int", coq: "shr_int_32", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)} val _shr_int = "shr_int" : (int, int) -> int |