Library Ltac2.Array

Require Import Ltac2.Init.

Ltac2 @external make : int -> 'a -> 'a array := "ltac2" "array_make".
Ltac2 @external length : 'a array -> int := "ltac2" "array_length".
Ltac2 @external get : 'a array -> int -> 'a := "ltac2" "array_get".
Ltac2 @external set : 'a array -> int -> 'a -> unit := "ltac2" "array_set".