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 (!'k, !'v) t =
  ('k, 'v FStar_Pervasives_Native.option)
    FStar_FunctionalExtensionality.restricted_t

val empty : Prims.unit -> ('uuuuu, 'uuuuu1) t

val literal : ('k -> 'v FStar_Pervasives_Native.option) -> ('k, 'v) t

val sel : ('k, 'v) t -> 'k -> 'v FStar_Pervasives_Native.option

val upd : ('k, 'v) t -> 'k -> 'v -> ('k, 'v) t

val remove : ('k, 'v) t -> 'k -> ('k, 'v) t

val contains : ('k, 'v) t -> 'k -> Prims.bool

val const : 'v -> ('k, 'v) t

type ('k, 'v, 'm1, 'm2) equal = Prims.unit