Add Vec API (#876)

boogie-org · Apr 25, 2024 · 443683c · 443683c
1 parent ba61f31
commit 443683c
Showing 1 changed file with 11 additions and 5 deletions.
diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl
@@ -126,11 +126,17 @@ function {:inline} Vec_Swap<T>(v: Vec T, i: int, j: int): Vec T
   )
 }
 
-function {:inline} Vec_Remove<T>(v: Vec T): Vec T {
-    (
-      var cond, new_len := 0 < v->len, v->len - 1;
-      Vec(v->contents[new_len := if (cond) then Default() else v->contents[new_len]], if (cond) then new_len else v->len)
-    )
+function {:inline} Vec_Remove<T>(v: Vec T): Vec T
+{
+  (
+    var cond, new_len := 0 < v->len, v->len - 1;
+    Vec(v->contents[new_len := if (cond) then Default() else v->contents[new_len]], if (cond) then new_len else v->len)
+  )
+}
+
+function {:inline} Vec_Contains<T>(v: Vec T, i: int): bool
+{
+  0 <= i && i < Vec_Len(v)
 }
 
 // extensionality lemma to be used explicitly by the programmer