let pr_nat =
  let rec f = (* Converts a nat_3 value to an int value *)
              function Z -> 0 | TTNZ (n) -> 2 * f (n) | STT (n) -> 2 * f (n) + 1
  in
    function
      ppf -> function n -> Format.open_box 0 ;
                           Format.print_string (string_of_int (f (n))) ;
                           Format.close_box () ;