fstar 2025.02.17 · OCaml Package

type (!'a, 'l) lseq = 'a FStar_Seq_Base.seq

type ('a, 's, 'j) indexable = Prims.unit

val head : 'a FStar_Seq_Base.seq -> 'a

val tail : 'a FStar_Seq_Base.seq -> 'a FStar_Seq_Base.seq

val last : 'a FStar_Seq_Base.seq -> 'a

val split : 
  'a FStar_Seq_Base.seq ->
  Prims.nat ->
  'a FStar_Seq_Base.seq * 'a FStar_Seq_Base.seq

val split_eq : 
  'a FStar_Seq_Base.seq ->
  Prims.nat ->
  'a FStar_Seq_Base.seq * 'a FStar_Seq_Base.seq

val count : 'a -> 'a FStar_Seq_Base.seq -> Prims.nat

val mem : 'a -> 'a FStar_Seq_Base.seq -> Prims.bool

val index_mem : 'a -> 'a FStar_Seq_Base.seq -> Prims.nat

val swap : 
  'a FStar_Seq_Base.seq ->
  Prims.nat ->
  Prims.nat ->
  'a FStar_Seq_Base.seq

val sorted : ('a -> 'a -> Prims.bool) -> 'a FStar_Seq_Base.seq -> Prims.bool

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

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

val split_5 : 
  'a FStar_Seq_Base.seq ->
  Prims.nat ->
  Prims.nat ->
  'a FStar_Seq_Base.seq FStar_Seq_Base.seq

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

val splice : 
  'a FStar_Seq_Base.seq ->
  Prims.nat ->
  'a FStar_Seq_Base.seq ->
  Prims.nat ->
  'a FStar_Seq_Base.seq

val replace_subseq : 
  'a FStar_Seq_Base.seq ->
  Prims.nat ->
  Prims.nat ->
  'a FStar_Seq_Base.seq ->
  'a FStar_Seq_Base.seq

val snoc : 'a FStar_Seq_Base.seq -> 'a -> 'a FStar_Seq_Base.seq

val find_l : 
  ('a -> Prims.bool) ->
  'a FStar_Seq_Base.seq ->
  'a FStar_Pervasives_Native.option

val un_snoc : 'a FStar_Seq_Base.seq -> 'a FStar_Seq_Base.seq * 'a

val find_r : 
  ('a -> Prims.bool) ->
  'a FStar_Seq_Base.seq ->
  'a FStar_Pervasives_Native.option

type 'i found = Prims.unit

val seq_find_aux : 
  ('a -> Prims.bool) ->
  'a FStar_Seq_Base.seq ->
  Prims.nat ->
  'a FStar_Pervasives_Native.option

val seq_find : 
  ('a -> Prims.bool) ->
  'a FStar_Seq_Base.seq ->
  'a FStar_Pervasives_Native.option

val for_all : ('a -> Prims.bool) -> 'a FStar_Seq_Base.seq -> Prims.bool

type ('a, 'l, 's) createL_post = Prims.unit

val createL : 'a Prims.list -> 'a FStar_Seq_Base.seq

type ('a, 's, 'x) contains = Prims.unit

type ('a, 'susuff, 's) suffix_of = Prims.unit

val of_list : 'a Prims.list -> 'a FStar_Seq_Base.seq

type ('a, 'i, 's, 'l) explode_and = Obj.t

type ('uuuuu, 's, 'l) pointwise_and = Obj.t

val sortWith : 
  ('a -> 'a -> Prims.int) ->
  'a FStar_Seq_Base.seq ->
  'a FStar_Seq_Base.seq

val sort_lseq : 
  Prims.nat ->
  'a tot_ord ->
  'a FStar_Seq_Base.seq ->
  'a FStar_Seq_Base.seq

val foldr : ('b -> 'a -> 'a) -> 'b FStar_Seq_Base.seq -> 'a -> 'a

val foldr_snoc : ('b -> 'a -> 'a) -> 'b FStar_Seq_Base.seq -> 'a -> 'a

val map_seq : ('a -> 'b) -> 'a FStar_Seq_Base.seq -> 'b FStar_Seq_Base.seq

package fstar