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 ('a, 's1, 's2) initialization_preorder = Prims.unittype !'a ubuffer =
('a FStar_Pervasives_Native.option, Prims.unit, Prims.unit)
LowStar_Monotonic_Buffer.mbufferval unull : Prims.unit -> 'a ubuffertype !'a pointer = 'a ubuffertype !'a pointer_or_null = 'a ubuffertype ('a, 'i, 's) ipred = Prims.unittype ('a, 'b, 'i) initialized_at =
('a FStar_Pervasives_Native.option,
Prims.unit,
Prims.unit,
Prims.unit,
Prims.unit)
LowStar_Monotonic_Buffer.witnessedval uindex : 'a ubuffer -> FStar_UInt32.t -> 'aval uupd : 'a ubuffer -> FStar_UInt32.t -> 'a -> Prims.unittype (!'a, 'len) lubuffer = 'a ubuffertype (!'a, 'len, 'r) lubuffer_or_null = 'a ubufferval ugcmalloc : Prims.unit -> FStar_UInt32.t -> 'a ubufferval ugcmalloc_partial : Prims.unit -> FStar_UInt32.t -> 'a ubufferval umalloc : Prims.unit -> FStar_UInt32.t -> 'a ubufferval umalloc_partial : Prims.unit -> FStar_UInt32.t -> 'a ubufferval ualloca : FStar_UInt32.t -> 'a ubuffertype ('a, 'rrel, 'rel, 'src, 'idxusrc, 'dst, 'idxudst, 'j) valid_j_for_blit =
Prims.unittype ('a, 'rrel, 'rel, 'src, 'idxusrc, 'dst, 'idxudst, 'j, 'h0, 'h1)
ublit_post_j =
Prims.unitval ublit :
('a, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer ->
FStar_UInt32.t ->
'a ubuffer ->
FStar_UInt32.t ->
FStar_UInt32.t ->
Prims.unitval witness_initialized : 'a ubuffer -> Prims.nat -> Prims.unitval recall_initialized : 'a ubuffer -> Prims.nat -> Prims.unit