diff options
| author | Brian Campbell | 2018-07-07 23:30:45 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-09 13:08:05 +0100 |
| commit | 0ebe1cc6e52ccc28b8629b0cdfa4a00ed1b60988 (patch) | |
| tree | 5667a5ec616a348f2b44fc2c2dcc7336761b1962 /aarch64/prelude.sail | |
| parent | 2c1dfb042ecc10c0ca7868ab186ff8235926d8d3 (diff) | |
Bits for bits of aarch64 in coq
Diffstat (limited to 'aarch64/prelude.sail')
| -rwxr-xr-x | aarch64/prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 6ce47ae3..6837c366 100755 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -151,9 +151,9 @@ val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int -val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) +val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w) -val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n) +val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n) function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o) |