diff options
Diffstat (limited to 'fstar')
| -rw-r--r-- | fstar/Primitives.fst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index fbf8140a..4642d080 100644 --- a/fstar/Primitives.fst +++ b/fstar/Primitives.fst @@ -7,7 +7,10 @@ open FStar.List.Tot (*** Utilities *) val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) : - ls':list a{length ls' = length ls} + ls':list a{ + length ls' = length ls /\ + index ls' i == x + } #push-options "--fuel 1" let rec list_update #a ls i x = match ls with @@ -242,9 +245,6 @@ 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 = () - -// 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) |