diff options
| author | Son Ho | 2023-08-18 10:44:01 +0200 |
|---|---|---|
| committer | Son Ho | 2023-08-18 10:44:01 +0200 |
| commit | a9c256fe95523842a1ff025e73f6e9ce7c2db38a (patch) | |
| tree | 719ddcd09d212c4c69c6d406ee6e024c0ef277ef /tests/fstar/array | |
| parent | 26c25bf375742cf4d5a0ab160b9646e90c067f18 (diff) | |
Add tests which use const generics as values
Diffstat (limited to 'tests/fstar/array')
| -rw-r--r-- | tests/fstar/array/Array.Funs.fst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst index 7c1d0b09..72163585 100644 --- a/tests/fstar/array/Array.Funs.fst +++ b/tests/fstar/array/Array.Funs.fst @@ -139,6 +139,10 @@ let index_index_array_fwd let* a = array_index_shared (array u32 32) 32 s i in array_index_shared u32 32 a j +(** [array::const_gen_ret]: forward function *) +let const_gen_ret_fwd (n : usize) : result usize = + Return n + (** [array::update_update_array]: forward function *) let update_update_array_fwd (s : array (array u32 32) 32) (i : usize) (j : usize) : result unit = |