package why3find

  1. Overview
  2. Docs

Module Why3findUtils.DarraySource

Dynamic Arrays

Sourcetype 'a t
Sourceval get : 'a t -> int -> 'a
Sourceval length : 'a t -> int
Sourceval map : ('a -> 'b) -> 'a t -> 'b t
Sourceval iter : ('a -> unit) -> 'a t -> unit
Sourceval iteri : (int -> 'a -> unit) -> 'a t -> unit
Sourceval empty : 'a t
Sourceval const : ?length:int -> 'a -> 'a t
Sourceval option : 'a option -> 'a t
Sourceval array : 'a array -> 'a t
Sourceval list : 'a list -> 'a t
Sourceval concat : 'a t -> 'a t -> 'a t
Sourcetype 'a buffer
Sourceval create : unit -> 'a buffer
Sourceval add : 'a buffer -> 'a -> unit
Sourceval addi : 'a buffer -> 'a -> int

Returns the index of the added element.

Sourceval contents : 'a buffer -> 'a t

Returns all the elements added to the buffer so far.

Sourceval sequence : ?overhead:int -> 'a Seq.t -> 'a t

Build the collection from a sequence. Can not be reversed.

Sourceval reverse : 'a t -> 'a t

Reverse the order of elements.

Sourceval delayed : ('a -> 'b t) -> 'a -> 'b t

Delayed computation

Sourceval make : length:(unit -> int) -> value:(int -> 'a) -> 'a t

Low-level constructor

Sourceval cache : length:(unit -> int) -> value:(int -> 'a) -> 'a t

Low-level constructor, with cache