fstar 2025.02.17 · OCaml Package

type uint32_t = FStar_UInt32.t

val max_uint32 : uint32_t

type !'a vector_str =

val uu___is_Vec : 'a vector_str -> Prims.bool

val __proj__Vec__item__sz : 'a vector_str -> uint32_t

val __proj__Vec__item__cap : 'a vector_str -> uint32_t

val __proj__Vec__item__vs : 'a vector_str -> 'a LowStar_Buffer.buffer

type !'a vector = 'a vector_str

val size_of : 'a vector -> uint32_t

val capacity_of : 'a vector -> uint32_t

val is_empty : 'a vector -> Prims.bool

type ('a, 'h, 'vec) live =
  ('a, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    LowStar_Monotonic_Buffer.live

type ('a, 'vec) freeable =
  ('a, Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.freeable

type ('h0, 'h1) hmap_dom_eq =
  (Prims.unit, Prims.unit, Prims.unit) FStar_Set.equal

val alloc_empty : Prims.unit -> 'a vector

val alloc_rid : uint32_t -> 'a -> Prims.unit -> 'a vector

val alloc : uint32_t -> 'a -> 'a vector

val alloc_reserve : uint32_t -> 'a -> Prims.unit -> 'a vector

val alloc_by_buffer : uint32_t -> 'a LowStar_Buffer.buffer -> 'a vector

val free : 'a vector -> Prims.unit

val index : 'a vector -> uint32_t -> 'a

val front : 'a vector -> 'a

val back : 'a vector -> 'a

val clear : 'a vector -> 'a vector

val assign : 'a vector -> uint32_t -> 'a -> Prims.unit

val resize_ratio : uint32_t

val new_capacity : uint32_t -> uint32_t

val insert : 'a vector -> 'a -> 'a vector

val flush : 'a vector -> 'a -> uint32_t -> 'a vector

val shrink : 'a vector -> uint32_t -> 'a vector

val fold_left_buffer : 
  uint32_t ->
  'a LowStar_Buffer.buffer ->
  ('b -> 'a -> 'b) ->
  'b ->
  'b

val fold_left : 'a vector -> ('b -> 'a -> 'b) -> 'b -> 'b

type ('a, 'seq, 'i, 'j, 'p) forall_seq = Prims.unit

type ('a, 'h, 'buf, 'i, 'j, 'p) forall_buffer = Prims.unit

type ('a, 'h, 'vec, 'i, 'j, 'p) forall_ = Prims.unit

type ('a, 'h, 'vec, 'p) forall_all = Prims.unit

type ('a, 'seq, 'i, 'j, 'p) forall2_seq = Prims.unit

type ('a, 'h, 'buf, 'i, 'j, 'p) forall2_buffer = Prims.unit

type ('a, 'h, 'vec, 'i, 'j, 'p) forall2 = Prims.unit

type ('a, 'h, 'vec, 'p) forall2_all = Prims.unit

package fstar