Require Extraction.

Primitive array := #array_type.

Definition a : array nat := [| 0%nat | 0%nat |].
Extraction a.