Skip to main content

🍃 Array.v

Environment

Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.Variant.

Definition t (a : Set) : Set := array a.

Parameter concat : {a : Set}, list (t a) t a.

Parameter length : {a : Set}, t a int.

Parameter to_list : {a : Set}, t a list a.

Parameter get : Variant.t.

Parameter unsafe_get : Variant.t.

Parameter set : Variant.t.

Parameter unsafe_set : Variant.t.

Parameter to_seq : Variant.t.

Parameter to_seqi : Variant.t.

Parameter make : Variant.t.

Parameter create : Variant.t.

Parameter make_matrix : Variant.t.

Parameter create_float : Variant.t.

Parameter make_float : Variant.t.

Parameter sub : Variant.t.

Parameter fill : Variant.t.

Parameter blit : Variant.t.

Parameter iter2 : Variant.t.

Parameter map2 : Variant.t.

Parameter combine : Variant.t.

Parameter sort : Variant.t.

Parameter stable_sort : Variant.t.

Parameter fast_sort : Variant.t.

Module Floatarray.
End Floatarray.