diff options
| author | Son HO | 2024-05-29 01:01:45 +0200 |
|---|---|---|
| committer | GitHub | 2024-05-29 01:01:45 +0200 |
| commit | 6d024213541c0f87f1fde991d860c35cd4e5747b (patch) | |
| tree | 7fc94f32e32674892154e7e72c2d589470c17f9a /tests/fstar | |
| parent | 95cb0eee7f9af0a0fd0d24a2531b5395b98b861f (diff) | |
| parent | 7a8dffc0bb0888b40c9be4e6a69a98bcffca883f (diff) | |
Merge pull request #220 from AeneasVerif/son/collisions
Fix name collision issues
Diffstat (limited to 'tests/fstar')
| -rw-r--r-- | tests/fstar/arrays/Arrays.Funs.fst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst index 289e603d..26a695bb 100644 --- a/tests/fstar/arrays/Arrays.Funs.fst +++ b/tests/fstar/arrays/Arrays.Funs.fst @@ -241,9 +241,9 @@ let index_all : result u32 = let* (s1, to_slice_mut_back) = array_to_slice_mut u32 2 (mk_array u32 2 [ 0; 0 ]) in let* (i7, s2) = index_mut_slice_u32_0 s1 in - let* i8 = u32_add i6 i7 in + let* i9 = u32_add i6 i7 in let* _ = to_slice_mut_back s2 in - Ok i8 + Ok i9 (** [arrays::update_array]: Source: 'tests/src/arrays.rs', lines 187:0-187:36 *) |