package fstar

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type ('a, 'b, 'f, 'g) inverses = Prims.unit

type (!'a, !'b) view =

val uu___is_View : ('a, 'b) view -> Prims.bool

val __proj__View__item__n : ('a, 'b) view -> Prims.pos

type (!'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.bool

val __proj__BufferView__item__buf : 
  ('src, 'rrel, 'rel, 'dest) buffer_view ->
  ('src, 'rrel, 'rel) LowStar_Monotonic_Buffer.mbuffer

val __proj__BufferView__item__v : 
  ('src, 'rrel, 'rel, 'dest) buffer_view ->
  ('src, 'dest) view

type !'dest buffer =
  (Prims.unit,
    Prims.unit,
    Prims.unit,
    (Obj.t, Obj.t, Obj.t, 'dest) buffer_view)
    FStar_Pervasives.dtuple4

type ('dest, 'b) as_buffer_t =
  (Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val as_buffer : 
  'b buffer ->
  (Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val get_view : 'b buffer -> (Prims.unit, 'b) view

type ('b, 'h, 'vb) live =
  (Prims.unit, Prims.unit, Prims.unit, Prims.unit, Prims.unit)
    LowStar_Monotonic_Buffer.live

type ('b, 'vb, 'h, 'hu) mods =
  (Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.modifies

type ('b, 'vb, 'h, 'hu) modifies =
  (Prims.unit, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.modifies