fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type u8 = FStar_UInt8.t
type u32 = FStar_UInt32.t
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 'len lbuffer = buffer
type ('r, 'len) malloc_pre = Prims.unit
type ('h0, 'b, 'h1) alloc_post_mem_common = 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