package fstar

You can search for identifiers within the package.

in-package search v0.2.0

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type ('a, 'f) total_order = Prims.unit

type !'a cmp = 'a -> 'a -> Prims.bool

type (!'k, !'v, 'f, 'd) map_t =
  ('k, 'v FStar_Pervasives_Native.option)
    FStar_FunctionalExtensionality.restricted_t

type (!'k, !'v, !'f) ordmap =

| Mk_map of ('k, Prims.unit) FStar_OrdSet.ordset * ('k, 'v, Prims.unit, Prims.unit) map_t

val uu___is_Mk_map : 
  'k FStar_OrdSet.cmp ->
  ('k, 'v, Prims.unit) ordmap ->
  Prims.bool

val __proj__Mk_map__item__d : 
  'k FStar_OrdSet.cmp ->
  ('k, 'v, Prims.unit) ordmap ->
  'k Prims.list

val __proj__Mk_map__item__m : 
  'k FStar_OrdSet.cmp ->
  ('k, 'v, Prims.unit) ordmap ->
  ('k, 'v FStar_Pervasives_Native.option)
    FStar_FunctionalExtensionality.restricted_t

val empty : 'k FStar_OrdSet.cmp -> ('k, 'v, Prims.unit) ordmap

val const_on : 
  'k FStar_OrdSet.cmp ->
  'k Prims.list ->
  'v ->
  ('k, 'v, Prims.unit) ordmap

val select : 
  'k FStar_OrdSet.cmp ->
  'k ->
  ('k, 'v, Prims.unit) ordmap ->
  'v FStar_Pervasives_Native.option

val insert : 'a FStar_OrdSet.cmp -> 'a -> 'a Prims.list -> 'a Prims.list

val update : 
  'k FStar_OrdSet.cmp ->
  'k ->
  'v ->
  ('k, 'v, Prims.unit) ordmap ->
  ('k, 'v, Prims.unit) ordmap

val contains : 
  'k FStar_OrdSet.cmp ->
  'k ->
  ('k, 'v, Prims.unit) ordmap ->
  Prims.bool

val dom : 'k FStar_OrdSet.cmp -> ('k, 'v, Prims.unit) ordmap -> 'k Prims.list

val remove : 
  'k FStar_OrdSet.cmp ->
  'k ->
  ('k, 'v, Prims.unit) ordmap ->
  ('k, 'v, Prims.unit) ordmap

val choose : 
  'k FStar_OrdSet.cmp ->
  ('k, 'v, Prims.unit) ordmap ->
  ('k * 'v) FStar_Pervasives_Native.option

val size : 'k FStar_OrdSet.cmp -> ('k, 'v, Prims.unit) ordmap -> Prims.nat

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