fstar 2025.02.17 · OCaml Package

type !'ty seq = 'ty Prims.list

val length : 'ty seq -> Prims.nat

val empty : Prims.unit -> 'ty seq

val singleton : 'ty -> 'ty seq

val index : 'ty seq -> Prims.nat -> 'ty

val op_Dollar_At : Prims.unit -> 'uuuuu seq -> Prims.nat -> 'uuuuu

val build : 'ty seq -> 'ty -> 'ty seq

val op_Dollar_Colon_Colon : Prims.unit -> 'uuuuu seq -> 'uuuuu -> 'uuuuu seq

val append : 'ty seq -> 'ty seq -> 'ty seq

val op_Dollar_Plus : Prims.unit -> 'uuuuu seq -> 'uuuuu seq -> 'uuuuu seq

val update : 'ty seq -> Prims.nat -> 'ty -> 'ty seq

type ('ty, 's, 'v) contains = Obj.t

val take : 'ty seq -> Prims.nat -> 'ty seq

val drop : 'ty seq -> Prims.nat -> 'ty seq

type ('ty, 's0, 's1) equal = Prims.unit

type ('uuuuu, 's0, 's1) op_Dollar_Equals_Equals = Prims.unit

type ('ty, 's0, 's1) is_prefix = Prims.unit

type ('uuuuu, 's0, 's1) op_Dollar_Less_Equals = Prims.unit

val rank : 'ty -> 'ty

type length_of_empty_is_zero_fact = Prims.unit

type length_zero_implies_empty_fact = Prims.unit

type singleton_length_one_fact = Prims.unit

type build_increments_length_fact = Prims.unit

type 'uuuuu index_into_build_fact = Prims.unit

type append_sums_lengths_fact = Prims.unit

type 'uuuuu index_into_singleton_fact = Prims.unit

type 'uuuuu index_after_append_fact = Prims.unit

type update_maintains_length_fact = Prims.unit

type update_then_index_fact = Prims.unit

type contains_iff_exists_index_fact = Prims.unit

type empty_doesnt_contain_anything_fact = Prims.unit

type build_contains_equiv_fact = Prims.unit

type take_contains_equiv_exists_fact = Prims.unit

type drop_contains_equiv_exists_fact = Prims.unit

type equal_def_fact = Prims.unit

type extensionality_fact = Prims.unit

type is_prefix_def_fact = Prims.unit

type take_length_fact = Prims.unit

type 'uuuuu index_into_take_fact = Prims.unit

type drop_length_fact = Prims.unit

type 'uuuuu index_into_drop_fact = Prims.unit

type 'uuuuu drop_index_offset_fact = Prims.unit

type 'uuuuu append_then_take_or_drop_fact = Prims.unit

type 'uuuuu take_commutes_with_in_range_update_fact = Prims.unit

type 'uuuuu take_ignores_out_of_range_update_fact = Prims.unit

type 'uuuuu drop_commutes_with_in_range_update_fact = Prims.unit

type 'uuuuu drop_ignores_out_of_range_update_fact = Prims.unit

type 'uuuuu drop_commutes_with_build_fact = Prims.unit

type rank_def_fact = Prims.unit

type element_ranks_less_fact = Prims.unit

type drop_ranks_less_fact = Prims.unit

type take_ranks_less_fact = Prims.unit

type append_take_drop_ranks_less_fact = Prims.unit

type drop_zero_fact = Prims.unit

type take_zero_fact = Prims.unit

type 'uuuuu drop_then_drop_fact = Prims.unit

type all_seq_facts = Prims.unit

package fstar