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 bytes = FStar_UInt8.t FStar_Seq_Base.seq

val le_to_n : bytes -> Prims.nat

val be_to_n : bytes -> Prims.nat

val n_to_le : Prims.nat -> Prims.nat -> bytes

val n_to_be : Prims.nat -> Prims.nat -> bytes

val uint32_of_le : bytes -> FStar_UInt32.t

val le_of_uint32 : FStar_UInt32.t -> bytes

val uint32_of_be : bytes -> FStar_UInt32.t

val be_of_uint32 : FStar_UInt32.t -> bytes

val uint64_of_le : bytes -> FStar_UInt64.t

val le_of_uint64 : FStar_UInt64.t -> bytes

val uint64_of_be : bytes -> FStar_UInt64.t

val be_of_uint64 : FStar_UInt64.t -> bytes

val seq_uint32_of_le : Prims.nat -> bytes -> FStar_UInt32.t FStar_Seq_Base.seq

val le_of_seq_uint32 : FStar_UInt32.t FStar_Seq_Base.seq -> bytes

val seq_uint32_of_be : Prims.nat -> bytes -> FStar_UInt32.t FStar_Seq_Base.seq

val be_of_seq_uint32 : FStar_UInt32.t FStar_Seq_Base.seq -> bytes

val seq_uint64_of_le : Prims.nat -> bytes -> FStar_UInt64.t FStar_Seq_Base.seq

val le_of_seq_uint64 : FStar_UInt64.t FStar_Seq_Base.seq -> bytes

val seq_uint64_of_be : Prims.nat -> bytes -> FStar_UInt64.t FStar_Seq_Base.seq

val be_of_seq_uint64 : FStar_UInt64.t FStar_Seq_Base.seq -> bytes