package fstar

You can search for identifiers within the package.

in-package search v0.2.0

package fstar

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type (!'a, !'b) map' = 'a -> 'b FStar_Pervasives_Native.option

type (!'a, !'b, 'inv) map = ('a, 'b) map'

val upd : ('a, 'b) map' -> 'a -> 'b -> ('a, 'b) map'

val sel : ('a, 'b) map' -> 'a -> 'b FStar_Pervasives_Native.option

type ('a, 'b, 'inv, 'm1, 'm2) grows_aux = Prims.unit

type ('a, 'b, 'inv, 'uuuuu, 'uuuuu1) grows = Prims.unit

type ('r, !'a, !'b, 'inv) t =
  (Prims.unit, ('a, 'b, 'inv) map, Prims.unit) FStar_HyperStack_ST.m_rref

val empty_map : ('a, 'b) map'

type rid = Prims.unit

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

type ('r, 'a, 'b, 'inv, 'm, 'x, 'h) defined = Prims.unit

type ('r, 'a, 'b, 'inv, 'm, 'x, 'y, 'h) contains = Prims.unit

type ('r, 'a, 'b, 'inv, 'm, 'x, 'h) fresh = Prims.unit

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

val lookup : 
  Prims.unit ->
  Prims.unit ->
  Prims.unit ->
  Prims.unit ->
  (Prims.unit, Obj.t, Obj.t, Obj.t) t ->
  Obj.t ->
  Obj.t FStar_Pervasives_Native.option