From 7d00c246dd0a8c1f0a843ee95f843a800d0fc5f2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 10 Feb 2022 02:12:02 +0100
Subject: Update Primitives.fst

---
 fstar/Primitives.fst | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'fstar')

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];
-- 
cgit v1.2.3