fstar 2025.02.17 (latest) · OCaml Package

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

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

val sorted : 'a cmp -> 'a Prims.list -> Prims.bool

type (!'a, 'f) ordset = 'a Prims.list

val empty : 'uuuuu cmp -> 'uuuuu Prims.list

val tail : 'a cmp -> 'a Prims.list -> 'a Prims.list

val head : 'uuuuu cmp -> 'uuuuu Prims.list -> 'uuuuu

val mem : 'uuuuu cmp -> 'uuuuu -> 'uuuuu Prims.list -> Prims.bool

val mem_of : 'a cmp -> 'a Prims.list -> 'a -> Prims.bool

val last_direct : 'a cmp -> 'a Prims.list -> 'a

val last_lib : 'a cmp -> 'a Prims.list -> 'a

val last : 'a cmp -> 'a Prims.list -> 'a

val liat_direct : 'a cmp -> 'a Prims.list -> 'a Prims.list

val liat_lib : 'a cmp -> 'a Prims.list -> 'a Prims.list

val liat : 'a cmp -> 'a Prims.list -> 'a Prims.list

val unsnoc : 'a cmp -> 'a Prims.list -> 'a Prims.list * 'a

val as_list : 'a cmp -> 'a Prims.list -> 'a Prims.list

val insert' : 'uuuuu cmp -> 'uuuuu -> 'uuuuu Prims.list -> 'uuuuu Prims.list

val distinct' : 'a cmp -> 'a Prims.list -> 'a Prims.list

val distinct : 'a cmp -> 'a Prims.list -> 'a Prims.list

val union : 
  'uuuuu cmp ->
  'uuuuu Prims.list ->
  'uuuuu Prims.list ->
  'uuuuu Prims.list

val remove' : 'a cmp -> 'a -> 'a Prims.list -> 'a Prims.list

val size' : 'a cmp -> 'a Prims.list -> Prims.nat

val subset' : 'a cmp -> 'a Prims.list -> 'a Prims.list -> Prims.bool

val remove_until_greater_than : 
  'a cmp ->
  'a ->
  'a Prims.list ->
  'a Prims.list * Prims.bool

val smart_intersect : 'a cmp -> 'a Prims.list -> 'a Prims.list -> 'a Prims.list

val intersect : 'a cmp -> 'a Prims.list -> 'a Prims.list -> 'a Prims.list

val choose : 'a cmp -> 'a Prims.list -> 'a FStar_Pervasives_Native.option

val remove : 'a cmp -> 'a -> 'a Prims.list -> 'a Prims.list

val size : 'a cmp -> 'a Prims.list -> Prims.nat

val subset : 'a cmp -> 'a Prims.list -> 'a Prims.list -> Prims.bool

val superset : 'a cmp -> 'a Prims.list -> 'a Prims.list -> Prims.bool

val singleton : 'a cmp -> 'a -> 'a Prims.list

val smart_minus : 'a cmp -> 'a Prims.list -> 'a Prims.list -> 'a Prims.list

val ncmp : Prims.nat -> Prims.nat -> Prims.bool

val minus : 'a cmp -> 'a Prims.list -> 'a Prims.list -> 'a Prims.list

val strict_subset : 'a cmp -> 'a Prims.list -> 'a Prims.list -> Prims.bool

val strict_superset : 'a cmp -> 'a Prims.list -> 'a Prims.list -> Prims.bool

val disjoint : 'a cmp -> 'a Prims.list -> 'a Prims.list -> Prims.bool

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

val fold : 'a cmp -> ('acc -> 'a -> 'acc) -> 'acc -> 'a Prims.list -> 'acc

val map_internal : 
  'a cmp ->
  'b cmp ->
  ('a -> 'b) ->
  'a Prims.list ->
  'b Prims.list

val map : 'a cmp -> 'b cmp -> ('a -> 'b) -> 'a Prims.list -> 'b Prims.list

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

val inv : 'a condition -> 'a condition

val count : 'a cmp -> 'a Prims.list -> 'a condition -> Prims.nat

val all : 'a cmp -> 'a Prims.list -> 'a condition -> Prims.bool

val any : 'a cmp -> 'a Prims.list -> 'a condition -> Prims.bool

val find_first : 
  'a cmp ->
  'a Prims.list ->
  'a condition ->
  'a FStar_Pervasives_Native.option

val find_last' : 
  'a cmp ->
  'a Prims.list ->
  'a condition ->
  'a FStar_Pervasives_Native.option

val find_last : 
  'a cmp ->
  'a Prims.list ->
  'a condition ->
  'a FStar_Pervasives_Native.option

val where : 'a cmp -> 'a Prims.list -> 'a condition -> 'a Prims.list

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

package fstar