fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type uint32_t = FStar_UInt32.t
val max_uint32 : uint32_t
type !'a vector_str =
  1. | Vec of uint32_t * uint32_t * 'a LowStar_Buffer.buffer
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 ('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