fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
val push_frame : unit -> unit
val pop_frame : unit -> unit
val root : unit
val def_rid : unit
val salloc : 'a -> 'a FStar_HyperStack.reference
val salloc_mm : 'a -> 'a FStar_HyperStack.reference
val sfree : 'a -> unit
val new_region : 'a -> unit
val new_colored_region : 'a -> 'b -> unit
val ralloc : Prims.unit -> 'a -> 'a FStar_HyperStack.reference
val ralloc_mm : Prims.unit -> 'a -> 'a FStar_HyperStack.reference
val rfree : 'a -> unit
val op_Colon_Equals : ('a, 'b) FStar_Monotonic_HyperStack.mreference' -> 'a -> unit
val op_Bang : ('a, 'b) FStar_Monotonic_HyperStack.mreference' -> 'a
val read : ('a, 'b) FStar_Monotonic_HyperStack.mreference' -> 'a
val write : ('a, 'b) FStar_Monotonic_HyperStack.mreference' -> 'a -> unit
val recall : 'a -> unit
val recall_region : 'a -> unit
val witness_region : 'a -> unit
val witness_hsref : 'a -> unit
type !'a ref = 'a FStar_HyperStack.reference
type (!'a, 'b) mreference = 'a ref
type !'a reference = 'a ref
val alloc : 'a -> 'a FStar_HyperStack.reference
type (!'a, 'b) mref = 'a ref
type ('a, !'b, 'c) m_rref = 'b ref
type ('a, 'b, 'c, 'd, 'e) stable_on_t = unit
val mr_witness : 'a -> 'b -> 'c -> 'd -> 'e -> unit
val testify : 'a -> unit
val testify_forall : 'a -> unit
val testify_forall_region_contains_pred : 'a -> 'b -> unit
type ex_rid = erid
type !'a witnessed = 'a FStar_CommonST.witnessed
type ('a, 'b, 'c, 'd) stable_on = unit
type ('a, 'b, 'c, 'd) token = unit
val witness_p : 'a -> 'b -> unit
val recall_p : 'a -> 'b -> unit
val new_drgn : 'a -> unit
val free_drgn : 'a -> unit
val ralloc_drgn : Prims.unit -> 'a -> 'a FStar_HyperStack.reference
val ralloc_drgn_mm : Prims.unit -> 'a -> 'a FStar_HyperStack.reference