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
val buffer_dummy : Prims.unit -> 'uuuuu LowStar_Buffer.buffertype nonzero = FStar_UInt32.ttype ('a, 'len, 'h, 'v) buffer_r_inv = Prims.unittype (!'a, 'len) buffer_repr = 'a FStar_Seq_Base.seqtype ('a, 'v) buffer_r_alloc_p = Prims.unitval buffer_r_alloc :
Prims.unit ->
('a * nonzero) ->
Prims.unit ->
'a LowStar_Buffer.bufferval buffer_r_free :
Prims.unit ->
('a * nonzero) ->
'a LowStar_Buffer.buffer ->
Prims.unitval buffer_copy :
Prims.unit ->
('a * nonzero) ->
'a LowStar_Buffer.buffer ->
'a LowStar_Buffer.buffer ->
Prims.unitval buffer_regional :
'a ->
nonzero ->
('a * nonzero, 'a LowStar_Buffer.buffer) LowStar_Regional.regionalval buffer_copyable :
'a ->
nonzero ->
('a * nonzero, 'a LowStar_Buffer.buffer, Prims.unit) LowStar_RVector.copyableval vector_dummy : Prims.unit -> 'a LowStar_Vector.vectortype ('a, 'rst, 'rg, 'h, 'v) vector_r_inv = Prims.unittype ('a, 'rst, 'rg) vector_repr = Prims.unit FStar_Seq_Base.seqtype ('a, 'rst, 'rg, 'v) vector_r_alloc_p = Prims.unitval vector_r_alloc :
('rst, 'a) LowStar_Regional.regional ->
Prims.unit ->
'a LowStar_Vector.vectorval vector_r_free :
Prims.unit ->
('uuuuu1, 'uuuuu) LowStar_Regional.regional ->
'uuuuu LowStar_Vector.vector ->
Prims.unitval vector_regional :
('rst, 'a) LowStar_Regional.regional ->
(('rst, 'a) LowStar_Regional.regional, 'a LowStar_Vector.vector)
LowStar_Regional.regional