fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
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