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

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 get : unit -> FStar_Monotonic_HyperStack.mem'

val recall : 'a -> unit

val recall_region : 'a -> unit

val witness_region : 'a -> unit

val witness_hsref : 'a -> unit

type erid = FStar_Monotonic_HyperHeap.rid

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

type drgn = FStar_Monotonic_HyperHeap.rid

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