fstar
  1. Overview
  2. Docs
package fstar
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 extend : Prims.unit -> ('a, 'b) map FStar_HyperStack_ST.ref -> 'a -> 'b -> Prims.unit
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