package fstar

You can search for identifiers within the package.

in-package search v0.2.0

package fstar

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type u8 = FStar_UInt8.t

type u32 = FStar_UInt32.t

val le_to_n : u8 FStar_Seq_Base.seq -> Prims.nat

val frozen_until : u8 FStar_Seq_Base.seq -> Prims.nat

type ('s1, 's2) pre = Prims.unit

type ('uuuuu, 'uuuuu1) prefix_freezable_preorder = Prims.unit

type ('n, 's) frozen_until_at_least = Prims.unit

type ('i, 'j, 'snap, 's) slice_is = Prims.unit

type buffer = (u8, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

type 'len lbuffer = buffer

type ('r, 'len) malloc_pre = Prims.unit

type ('h0, 'b, 'h1) alloc_post_mem_common = Prims.unit

val update_frozen_until_alloc : 
  (u8,
    (Prims.unit, Prims.unit) prefix_freezable_preorder,
    (Prims.unit, Prims.unit) prefix_freezable_preorder)
    LowStar_Monotonic_Buffer.mbuffer ->
  Prims.unit

val gcmalloc : Prims.unit -> u32 -> buffer

val malloc : Prims.unit -> u32 -> buffer

type 'len alloca_pre = Prims.unit

val alloca : u32 -> buffer

val upd : buffer -> u32 -> u8 -> Prims.unit

val freeze : buffer -> u32 -> Prims.unit

val frozen_until_st : buffer -> u32

val witness_slice : buffer -> u32 -> u32 -> Prims.unit -> Prims.unit

val recall_slice : buffer -> u32 -> u32 -> Prims.unit -> Prims.unit

val witness_frozen_until : buffer -> Prims.nat -> Prims.unit

val recall_frozen_until : buffer -> Prims.nat -> Prims.unit

val recall_frozen_until_default : buffer -> Prims.unit