val vector (a: Type0): Tot Type0
let vector a = vector_str a
val vector (a: Type0): Tot Type0
let vector a =
vector_str a
LowStar.Vector.fst.checked
prims.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
LowStar.Vector.fst
LowStar.Vector.vector_str
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module LowStar.Vector


(**
 * This module provides support for mutable, partially filled arrays
 * whose contents may grow up to some fixed capacity determined
 * during initialization.
 *
 * Vectors support an insertion operation that may, if the capacity
 * has been reached, involve copying its contents to a new
 * vector of twice the capacity (so long as the capacity has not
 * already reached max_uint32).
 *
 * Conversely, an operation called `flush` is also provided to
 * shrink a vector to some prefix of its current contents.
 *
 * Other operations are fairly standard, and involve reading,
 * writing, and iterating over a vector.
 *
 *)

open FStar.Integers
open LowStar.Modifies

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
module S = FStar.Seq

type uint32_t = UInt32.t

val max_uint32: uint32_t
let max_uint32 = 4294967295ul // UInt32.uint_to_t (UInt.max_int UInt32.n)

module U32 = FStar.UInt32

/// Abstract vector type

inline_for_extraction noeq type vector_str a =
| Vec: sz:uint32_t ->
       cap:uint32_t{cap >= sz} ->
       vs:B.buffer a{B.len vs = cap} ->
       vector_str a
val vector (a: Type0): Tot Type0
a: Type0 -> Type0