To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
package fstar
-
fstarlib
-
fstartaclib
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type ('a, 'b, 'f, 'g) inverses = Prims.unitval uu___is_View : ('a, 'b) view -> Prims.booltype (!'src, !'rrel, !'rel, !'dest) buffer_view = | BufferView of ('src, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer * ('src, 'dest) view
val uu___is_BufferView : ('src, 'rrel, 'rel, 'dest) buffer_view -> Prims.boolval __proj__BufferView__item__buf :
('src, 'rrel, 'rel, 'dest) buffer_view ->
('src, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbufferval __proj__BufferView__item__v :
('src, 'rrel, 'rel, 'dest) buffer_view ->
('src, 'dest) viewtype !'dest buffer =
(Prims.unit,
Prims.unit,
Prims.unit,
(Obj.t, Obj.t, Obj.t, 'dest) buffer_view)
FStar_Pervasives.dtuple4type ('dest, 'b) as_buffer_t =
(Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbufferval as_buffer :
'b buffer ->
(Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbufferval get_view : 'b buffer -> (Prims.unit, 'b) viewtype ('b, 'h, 'vb) live =
(Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
LowStar_Monotonic_Buffer.livetype ('b, 'vb, 'h, 'hu) mods =
(Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.modifiestype ('b, 'vb, 'h, 'hu) modifies =
(Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.modifies