Require Import Ltac2.Init.
Ltac2 @
external make :
int ->
char ->
string := "ltac2" "string_make".
Ltac2 @
external length :
string ->
int := "ltac2" "string_length".
Ltac2 @
external get :
string ->
int ->
char := "ltac2" "string_get".
Ltac2 @
external set :
string ->
int ->
char ->
unit := "ltac2" "string_set".