fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 as_list : 'uuuuu cmp -> 'uuuuu Prims.list -> 'uuuuu Prims.list
val empty : 'uuuuu cmp -> 'uuuuu Prims.list
val mem : 'uuuuu cmp -> 'uuuuu -> 'uuuuu Prims.list -> Prims.bool
val insert' : 'uuuuu cmp -> 'uuuuu -> 'uuuuu Prims.list -> 'uuuuu Prims.list
val union : 'uuuuu cmp -> 'uuuuu Prims.list -> 'uuuuu Prims.list -> 'uuuuu 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 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 singleton : 'a cmp -> 'a -> 'a Prims.list
val remove_le : 'a cmp -> 'a -> 'a Prims.list -> 'a Prims.list
val minus' : 'a cmp -> 'a -> 'a Prims.list -> 'a Prims.list -> 'a Prims.list
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 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
val as_set : 'a cmp -> 'a Prims.list -> 'a FStar_Set.set