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 ('uuuuu, 'uuuuu1, 'f, 'g) inverses = Prims.unitval uu___is_View : ('a, 'b) view -> Prims.booltype !'dest buffer = | Buffer of Prims.unit * Obj.t LowStar_BufferView_Down.buffer * (Obj.t, 'dest) view
val uu___is_Buffer : 'dest buffer -> Prims.boolval __proj__Buffer__item__down_buf :
'dest buffer ->
Prims.unit LowStar_BufferView_Down.bufferval __proj__Buffer__item__v : 'dest buffer -> (Prims.unit, 'dest) viewtype ('b, 'bv) buffer_src = Obj.tval as_down_buffer : 'b buffer -> Obj.t LowStar_BufferView_Down.buffertype ('b, 'h, 'vb) live =
(Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
LowStar_Monotonic_Buffer.livetype ('b, 'vb, 'h, 'hu) modifies =
(Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.modifies