package fstar

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type !'a array = 'a FStar_Seq_Base.seq FStar_ST.ref

type ('a, 'h, 's) contains =
  ('a FStar_Seq_Base.seq, Prims.unit, Prims.unit, Prims.unit)
    FStar_Monotonic_Heap.contains

type ('a, 'arr, 'h) unused_in =
  ('a FStar_Seq_Base.seq, Prims.unit, Prims.unit, Prims.unit)
    FStar_Monotonic_Heap.unused_in

val op_At_Bar : 'a array -> 'a array -> 'a array

type ('a, 's, 'h0, 'x, 'h1) create_post = Prims.unit

val of_seq : 'a FStar_Seq_Base.seq -> 'a array

val to_seq : 'a array -> 'a FStar_Seq_Base.seq

val of_list : 'a Prims.list -> 'a array

val create : Prims.nat -> 'a -> 'a array

val index : 'a array -> Prims.nat -> 'a

val upd : 'a array -> Prims.nat -> 'a -> Prims.unit

val length : 'a array -> Prims.nat

val op : 
  ('a FStar_Seq_Base.seq -> 'a FStar_Seq_Base.seq) ->
  'a array ->
  Prims.unit

val swap : 'a array -> Prims.nat -> Prims.nat -> Prims.unit

val copy_aux : 'a array -> 'a array -> Prims.nat -> Prims.unit

val copy : 'a array -> 'a array

val blit_aux : 
  'a array ->
  Prims.nat ->
  'a array ->
  Prims.nat ->
  Prims.nat ->
  Prims.nat ->
  Prims.unit

val blit : 
  'a array ->
  Prims.nat ->
  'a array ->
  Prims.nat ->
  Prims.nat ->
  Prims.unit

val sub : 'a array -> Prims.nat -> Prims.nat -> 'a array