package fstar

You can search for identifiers within the package.

in-package search v0.2.0

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type ('a, 's1, 's2) immutable_preorder =
  ('a, Prims.unit, Prims.unit) FStar_Seq_Base.equal

type !'a ibuffer =
  ('a,
    ('a, Prims.unit, Prims.unit) immutable_preorder,
    ('a, Prims.unit, Prims.unit) immutable_preorder)
    LowStar_Monotonic_Buffer.mbuffer

val inull : Prims.unit -> 'a ibuffer

type !'a ipointer = 'a ibuffer

type !'a ipointer_or_null = 'a ibuffer

val isub : 
  Prims.unit ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  Prims.unit ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val ioffset : 
  Prims.unit ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

type ('a, 's, 's1) cpred = ('a, Prims.unit, Prims.unit) FStar_Seq_Base.equal

type ('a, 's, 'su) seq_eq = ('a, Prims.unit, Prims.unit) FStar_Seq_Base.equal

type ('a, 'b, 's) value_is =
  ('a,
    ('a, Prims.unit, Prims.unit) immutable_preorder,
    ('a, Prims.unit, Prims.unit) immutable_preorder,
    Prims.unit,
    ('a, Prims.unit, Prims.unit) seq_eq)
    LowStar_Monotonic_Buffer.witnessed

type (!'a, 'len, 's) libuffer =
  ('a,
    ('a, Prims.unit, Prims.unit) immutable_preorder,
    ('a, Prims.unit, Prims.unit) immutable_preorder)
    LowStar_Monotonic_Buffer.mbuffer

type (!'a, 'len, 'r, 's) libuffer_or_null =
  ('a,
    ('a, Prims.unit, Prims.unit) immutable_preorder,
    ('a, Prims.unit, Prims.unit) immutable_preorder)
    LowStar_Monotonic_Buffer.mbuffer

val igcmalloc : 
  Prims.unit ->
  'a ->
  FStar_UInt32.t ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

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

val igcmalloc_partial : 
  Prims.unit ->
  'a ->
  FStar_UInt32.t ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val imalloc : 
  Prims.unit ->
  'a ->
  FStar_UInt32.t ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

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

val imalloc_partial : 
  Prims.unit ->
  'a ->
  FStar_UInt32.t ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val ialloca : 
  'a ->
  FStar_UInt32.t ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val ialloca_and_blit : 
  ('a, 'rrel1, 'rel1) LowStar_Monotonic_Buffer.mbuffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val ialloca_of_list : 
  'a Prims.list ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val igcmalloc_of_list : 
  Prims.unit ->
  'a Prims.list ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val igcmalloc_of_list_partial : 
  Prims.unit ->
  'a Prims.list ->
  ('a, Prims.unit, Prims.unit) LowStar_Monotonic_Buffer.mbuffer

val witness_contents : 'a ibuffer -> 'a FStar_Seq_Base.seq -> Prims.unit

val recall_contents : 'a ibuffer -> 'a FStar_Seq_Base.seq -> Prims.unit

val witness_value : 'a ibuffer -> Prims.unit

val recall_value : 'a ibuffer -> Prims.unit -> Prims.unit