Library Coq.extraction.ExtrOCamlPArray


Extraction to OCaml of persistent arrays.

From Coq Require PArray Extraction.

Primitive types and operators.
Extract Constant PArray.array "'a" => "'a Parray.t".
Extraction Inline PArray.array.

Extract Constant PArray.make => "Parray.make".
Extract Constant PArray.get => "Parray.get".
Extract Constant PArray.default => "Parray.default".
Extract Constant PArray.set => "Parray.set".
Extract Constant PArray.length => "Parray.length".
Extract Constant PArray.copy => "Parray.copy".
Extract Constant PArray.reroot => "Parray.reroot".