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 ('q, 'a) qbuf_cases = Obj.t

type ('q, 'a) q_preorder = Obj.t

type 'a qbuf = (Prims.unit, Obj.t) Prims.dtuple2

type ('a, 'c, 'uuuuu, 'uuuuu1) qbuf_pre = Obj.t

val qbuf_mbuf : 
  (Prims.unit, Obj.t) Prims.dtuple2 ->
  ('a, Obj.t, Obj.t) LowStar_Monotonic_Buffer.mbuffer

type 'a const_buffer = 'a qbuf

val as_qbuf : 
  (Prims.unit, Obj.t) Prims.dtuple2 ->
  (Prims.unit, Obj.t) Prims.dtuple2

type ('a, 'h, 'c) live =
  ('a, Obj.t, Obj.t, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.live

val of_buffer : 'a LowStar_Buffer.buffer -> 'a const_buffer

val of_ibuffer : 'a LowStar_ImmutableBuffer.ibuffer -> 'a const_buffer

val of_qbuf : 
  Prims.unit ->
  ('uuuuu, Obj.t, Obj.t) LowStar_Monotonic_Buffer.mbuffer ->
  'uuuuu const_buffer

val null : Prims.unit -> 'a const_buffer

val is_null : (Prims.unit, Obj.t) Prims.dtuple2 -> Prims.bool

val index : (Prims.unit, Obj.t) Prims.dtuple2 -> FStar_UInt32.t -> 'a

type ('a, 'i, 'len, 'csub, 'c) const_sub_buffer = Prims.unit

val sub : 
  (Prims.unit, Obj.t) Prims.dtuple2 ->
  FStar_UInt32.t ->
  Prims.unit ->
  (Prims.unit, Obj.t) Prims.dtuple2

val cast : 
  (Prims.unit, Obj.t) Prims.dtuple2 ->
  ('a, Obj.t, Obj.t) LowStar_Monotonic_Buffer.mbuffer

val to_buffer : (Prims.unit, Obj.t) Prims.dtuple2 -> 'a LowStar_Buffer.buffer

val to_ibuffer : 
  (Prims.unit, Obj.t) Prims.dtuple2 ->
  'a LowStar_ImmutableBuffer.ibuffer

val test : 
  FStar_UInt32.t LowStar_Buffer.buffer ->
  FStar_UInt32.t LowStar_ImmutableBuffer.ibuffer ->
  FStar_UInt32.t