fstar 2025.02.17 · OCaml Package

type ('a, 'f, 'xs) has_elements = Prims.unit

type !'a set = ('a, Prims.bool) FStar_FunctionalExtensionality.restricted_t

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

val list_nonrepeating : 'a Prims.list -> Prims.bool

val remove_repeats : 'a Prims.list -> 'a Prims.list

val intro_set : 
  ('a, Prims.bool) FStar_FunctionalExtensionality.restricted_t ->
  Prims.unit ->
  'a set

val emptyset : Prims.unit -> 'a set

val insert : 'a -> 'a set -> 'a set

val singleton : 'a -> 'a set

val union_lists : 'a Prims.list -> 'a Prims.list -> 'a Prims.list

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

val intersect_lists : 'a Prims.list -> 'a Prims.list -> 'a Prims.list

val intersection : 'a set -> 'a set -> 'a set

val difference_lists : 'a Prims.list -> 'a Prims.list -> 'a Prims.list

val difference : 'a set -> 'a set -> 'a set

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

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

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

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

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

type empty_set_contains_no_elements_fact = Prims.unit

type length_zero_fact = Prims.unit

type singleton_contains_argument_fact = Prims.unit

type singleton_contains_fact = Prims.unit

type singleton_cardinality_fact = Prims.unit

type insert_fact = Prims.unit

type insert_contains_argument_fact = Prims.unit

type insert_contains_fact = Prims.unit

type insert_member_cardinality_fact = Prims.unit

type insert_nonmember_cardinality_fact = Prims.unit

type union_contains_fact = Prims.unit

type union_contains_element_from_first_argument_fact = Prims.unit

type union_contains_element_from_second_argument_fact = Prims.unit

type union_of_disjoint_fact = Prims.unit

type intersection_contains_fact = Prims.unit

type union_idempotent_right_fact = Prims.unit

type union_idempotent_left_fact = Prims.unit

type intersection_idempotent_right_fact = Prims.unit

type intersection_idempotent_left_fact = Prims.unit

type intersection_cardinality_fact = Prims.unit

type difference_contains_fact = Prims.unit

type difference_doesnt_include_fact = Prims.unit

type difference_cardinality_fact = Prims.unit

type subset_fact = Prims.unit

type equal_fact = Prims.unit

type equal_extensionality_fact = Prims.unit

type disjoint_fact = Prims.unit

type insert_remove_fact = Prims.unit

type remove_insert_fact = Prims.unit

type set_as_list_cardinality_fact = Prims.unit

type all_finite_set_facts = Prims.unit

val remove_from_nonrepeating_list : 'a -> 'a Prims.list -> 'a Prims.list

package fstar