package fstar
-
fstar.lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type rid = Prims.inttype t = (rid, FStar_Monotonic_Heap.heap) FStar_Map.ttype st_pre = Prims.unittype ('a, 'pre) st_post' = Prims.unittype 'a st_post = Prims.unittype 'a st_wp = Prims.unittype ('id, !'a) rref = 'a FStar_Heap.refval as_ref : rid -> 'a FStar_Heap.ref -> 'a FStar_Heap.refval ref_as_rref : rid -> 'a FStar_Heap.ref -> 'a FStar_Heap.refval new_region : Prims.unit -> ridval ralloc : rid -> 'a -> 'a FStar_Heap.refval op_Colon_Equals : rid -> 'a FStar_Heap.ref -> 'a -> Prims.unitval op_Bang : rid -> 'a FStar_Heap.ref -> 'aval get : Prims.unit -> ttype ('s, 'm0, 'm1) modifies =
(rid, FStar_Monotonic_Heap.heap, Prims.unit, Prims.unit) FStar_Map.equaltype ('i, 'm0, 'm1) fresh_region = Prims.unittype ('a, 'i, 'r, 'm) contains_ref = Prims.unittype ('a, 'i, 'r, 'm0, 'm1) fresh_rref = Prims.unit