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 set = ('a, Prims.bool) FStar_FunctionalExtensionality.restricted_t

type ('a, 's1, 's2) equal = Prims.unit

val mem : 'a -> 'a set -> Prims.bool

val empty : Prims.unit -> 'a set

val singleton : 'a -> 'a set

val union : 'a set -> 'a set -> 'a set

val intersect : 'a set -> 'a set -> 'a set

val complement : 'a set -> 'a set

type ('a, 's1, 's2) disjoint = Prims.unit

type ('a, 's1, 's2) subset = Prims.unit

val add : 'a -> 'a set -> 'a set

val remove : 'a -> 'a set -> 'a set

val as_set' : 'a Prims.list -> 'a set

val as_set : 'a Prims.list -> 'a set