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, 'x) opt = 'b FStar_Pervasives_Native.option

type (!'a, !'b) partial_dependent_map =
  ('a, ('a, 'b, Prims.unit) opt) FStar_DependentMap.t

val empty_partial_dependent_map : Prims.unit -> ('a, 'b) partial_dependent_map

type (!'a, !'b) map = ('a, 'b) Prims.dtuple2 Prims.list

val empty : Prims.unit -> ('a, 'b) map

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

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

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

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

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

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

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

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

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

val alloc : Prims.unit -> Prims.unit -> ('a, 'b) map FStar_HyperStack_ST.ref

val extend : 
  Prims.unit ->
  ('a, 'b) map FStar_HyperStack_ST.ref ->
  'a ->
  'b ->
  Prims.unit

val lookup : 
  Prims.unit ->
  ('a, 'b) map FStar_HyperStack_ST.ref ->
  'a ->
  'b FStar_Pervasives_Native.option

type ('a, 'b, 'inv, 'r, 't1, 'h, 'pred) forall_t = Prims.unit

val f_opt : 
  ('a -> 'b -> 'c) ->
  'a ->
  'b FStar_Pervasives_Native.option ->
  'c FStar_Pervasives_Native.option

val mmap_f : ('a, 'b) map -> ('a -> 'b -> 'c) -> ('a, 'c) map

val map_f : 
  Prims.unit ->
  Prims.unit ->
  ('a, 'b) map FStar_HyperStack_ST.ref ->
  ('a -> 'b -> 'c) ->
  ('a, 'c) map FStar_HyperStack_ST.ref