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".