diff options
Diffstat (limited to 'fstar')
| -rw-r--r-- | fstar/Primitives.fst | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index 78697259..fbf8140a 100644 --- a/fstar/Primitives.fst +++ b/fstar/Primitives.fst @@ -242,7 +242,16 @@ let vec_len (a : Type0) (v : vec a) : usize = length v // The **forward** function shouldn't be used let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = () -let vec_push_back (a : Type0) (v : vec a) (x : a) : result (vec a) = + +// The **forward** function shouldn't be used +let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = () +let vec_push_back (a : Type0) (v : vec a) (x : a) : + Pure (result (vec a)) + (requires True) + (ensures (fun res -> + match res with + | Fail -> True + | Return v' -> length v' = length v + 1)) = if length v < usize_max then begin (**) assert_norm(length [x] == 1); (**) append_length v [x]; |