Giving an idea on what it takes to iterate over a Coq term in Ltac2

Ltac2_term.v

Require Import Ltac2.Ltac2.
Require Import Ltac2.Message.
Import Ltac2.Constr.Unsafe.
Require Ltac2.List.

Ltac2 rec message_indent (lvl:int) (m:message) :=
  match Int.equal lvl 0 with
  | true => m
  | false => concat (of_string " ") (message_indent (Int.sub lvl 1) m)
  end.

Ltac2 rec print_constr_array (a:constr array) (i:int) (len:int):= 
  let l := Array.length a in
    match Int.equal l i with
    | true => ()
    | false => 
      let v := Array.get a i in
        print_kind (kind v) len;
        print_constr_array a (Int.add i 1) (Int.add len 1)
    end

with print_kind (k:kind) (len:int) :=

  match k with
  | Rel int => print (of_string "Rel")
  | Var ident => print (of_string "Var")
  | Meta meta => print (of_string "Meta")
  | Evar evar arr_constr => print (of_string "Evar")
  | Sort sort => print (of_string "Sort")
  | Cast constr cast constr => print (of_string "Cast")
  | Prod binder constr => print (of_string "Prod")
  | Lambda binder constr => print (of_string "Lambda")
  | LetIn binder constr_a constr_b => print (of_string "LetIn")

  | App constr_func constr_arr_args => (
      print (message_indent len (of_string "App")); 
      print_kind (kind constr_func) (Int.add 2 len);
      print_constr_array constr_arr_args 0 (Int.add 2 len)
    )

  | Constant constant instance => 
      print (message_indent len (of_string "Constant"))

  | Ind inductive instance => print (of_string "Ind")

  | Constructor constructor instance =>
    print (message_indent len (of_string "Constructor"))

  | Case case_a constr_a case_b constr_b constr_arr => print (of_string "Case")
  | Fix int_arr int binder constr_arr => print (of_string "Fix")
  | CoFix int binder constr_arr => print (of_string "CoFix")
  | Proj projection constr => print (of_string "Proj")
  | Uint63 uint63 => print (of_string "Uint63")
  | Float float => print (of_string "Float")
  | Array instance constr_arr constr_a constr_b => print (of_string "Array")
  end.

Ltac2 print_term info term := 
  print (concat (of_string info) (of_constr (term)));
  print_kind (kind term) 0.

Ltac2 Eval (print_term "A function" constr:((fun x : nat => x+x) 3)).