fstar
  1. Overview
  2. Docs
package fstar
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
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