diff options
Diffstat (limited to 'backends/fstar')
| -rw-r--r-- | backends/fstar/Primitives.fst | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index cd18cf29..e9391834 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -352,6 +352,9 @@ let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range us let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = admit() +let array_repeat (a : Type0) (n : usize) (x : a) : array a n = + admit() + let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = admit() |