diff options
| author | Son Ho | 2023-10-26 16:15:35 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-26 16:15:35 +0200 |
| commit | 1110b3da85e93ba0755a665edd5b8c986c54cef0 (patch) | |
| tree | e668d3ca33cd412a031189ae6f281a663192a1d1 /tests/fstar/array/Array.Clauses.Template.fst | |
| parent | c8c9be9b7d9866f9761a21adbadd923d4a79bb09 (diff) | |
Make minor modifications and update the array test for F*
Diffstat (limited to 'tests/fstar/array/Array.Clauses.Template.fst')
| -rw-r--r-- | tests/fstar/array/Array.Clauses.Template.fst | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tests/fstar/array/Array.Clauses.Template.fst b/tests/fstar/array/Array.Clauses.Template.fst index 8a15e230..06056d61 100644 --- a/tests/fstar/array/Array.Clauses.Template.fst +++ b/tests/fstar/array/Array.Clauses.Template.fst @@ -8,11 +8,12 @@ open Array.Types (** [array::sum]: decreases clause *) unfold -let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat = admit () +let sum_loop_decreases (s : slice u32) (sum0 : u32) (i : usize) : nat = + admit () (** [array::sum2]: decreases clause *) unfold -let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32) +let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum0 : u32) (i : usize) : nat = admit () |