package fstar

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type u8 = FStar_UInt8.t

type u16 = FStar_UInt16.t

type u32 = FStar_UInt32.t

type u64 = FStar_UInt64.t

type u128 = FStar_UInt128.t

val htole16 : FStar_UInt16.t -> FStar_UInt16.t

val le16toh : FStar_UInt16.t -> FStar_UInt16.t

val htole32 : FStar_UInt32.t -> FStar_UInt32.t

val le32toh : FStar_UInt32.t -> FStar_UInt32.t

val htole64 : FStar_UInt64.t -> FStar_UInt64.t

val le64toh : FStar_UInt64.t -> FStar_UInt64.t

val htobe16 : FStar_UInt16.t -> FStar_UInt16.t

val be16toh : FStar_UInt16.t -> FStar_UInt16.t

val htobe32 : FStar_UInt32.t -> FStar_UInt32.t

val be32toh : FStar_UInt32.t -> FStar_UInt32.t

val htobe64 : FStar_UInt64.t -> FStar_UInt64.t

val be64toh : FStar_UInt64.t -> FStar_UInt64.t

type ('a, 'rrel, 'rel, 'b, 'i, 'j, 'predicate, 'h) store_pre = Prims.unit

type ('a, 'rrel, 'rel, 'b, 'i, 'j, 'predicate, 'h0, 'uuuuu, 'h1) store_post =
  Prims.unit

val store16_le_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt16.t ->
  Prims.unit

val load16_le_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt16.t

val store16_be_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt16.t ->
  Prims.unit

val load16_be_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt16.t

val store32_le_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  Prims.unit

val load32_le_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t

val store32_be_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  Prims.unit

val load32_be_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t

val store64_le_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt64.t ->
  Prims.unit

val load64_le_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt64.t

val store64_be_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt64.t ->
  Prims.unit

val load64_be_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt64.t

val store128_le_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt128.t ->
  Prims.unit

val load128_le_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt128.t

val store128_be_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt128.t ->
  Prims.unit

val load128_be_i : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt128.t

val store16_le : 
  FStar_UInt8.t LowStar_Buffer.buffer ->
  FStar_UInt16.t ->
  Prims.unit

val load16_le : FStar_UInt8.t LowStar_Buffer.buffer -> FStar_UInt16.t

val store16_be : 
  FStar_UInt8.t LowStar_Buffer.buffer ->
  FStar_UInt16.t ->
  Prims.unit

val load16_be : FStar_UInt8.t LowStar_Buffer.buffer -> FStar_UInt16.t

val store32_le : 
  FStar_UInt8.t LowStar_Buffer.buffer ->
  FStar_UInt32.t ->
  Prims.unit

val load32_le : FStar_UInt8.t LowStar_Buffer.buffer -> FStar_UInt32.t

val store32_be : 
  FStar_UInt8.t LowStar_Buffer.buffer ->
  FStar_UInt32.t ->
  Prims.unit

val load32_be : FStar_UInt8.t LowStar_Buffer.buffer -> FStar_UInt32.t

val store64_le : 
  FStar_UInt8.t LowStar_Buffer.buffer ->
  FStar_UInt64.t ->
  Prims.unit

val load64_le : FStar_UInt8.t LowStar_Buffer.buffer -> FStar_UInt64.t

val load64_be : FStar_UInt8.t LowStar_Buffer.buffer -> FStar_UInt64.t

val store64_be : 
  FStar_UInt8.t LowStar_Buffer.buffer ->
  FStar_UInt64.t ->
  Prims.unit

val load128_le : FStar_UInt8.t LowStar_Buffer.buffer -> FStar_UInt128.t

val store128_le : 
  FStar_UInt8.t LowStar_Buffer.buffer ->
  FStar_UInt128.t ->
  Prims.unit

val load128_be : FStar_UInt8.t LowStar_Buffer.buffer -> FStar_UInt128.t

val store128_be : 
  FStar_UInt8.t LowStar_Buffer.buffer ->
  FStar_UInt128.t ->
  Prims.unit

val index_32_be : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t

val index_32_le : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t

val index_64_be : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt64.t

val index_64_le : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt64.t

val upd_32_be : 
  (FStar_UInt8.t, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  Prims.unit