Inductive bin : Type :=
  | Z
  | A (n : bin)
  | B (n : bin).

Fixpoint bin_to_nat (m:bin) : nat :=
  (* What to do here? *)

#include <stdio.h>

unsigned int pow2(unsigned int power)
{
    if(power != 0)
        return 2 << (power - 1);
    else
        return 1;
}

void rec_converter(char str[], size_t i)
{
    if(str[i] == 'Z')
        printf("%c", 'Z');
    else if(str[i] == '0')
        rec_converter(str, ++i);
    else if(str[i] == '1')
    {
        unsigned int n = pow2(i);

        for (size_t j = 0; j < n; j++)
        {
            printf("%c", 'S');
        }
        rec_converter(str, ++i);
    }
}

int main(void)
{
    char str[] = "11Z";

    rec_converter(str, 0);
    printf("n");

    return 0;
}

unsigned int n = pow2(i);

for (size_t j = 0; j < n; j++)
{
    printf("%c", 'S');
}
rec_converter(str, ++i);

Fixpoint bin_to_nat (m: bin): nat :=
  match m with
  | Z => 0
  | A n => 2 * (bin_to_nat n)
  | B n => 2 * (bin_to_nat n) + 1
  end.

Inductive Positive :=
| one
| times_two (x: Positive): Positive
| times_two_plus_one (x: Positive): Positive.

Inductive BinNat :=
| zero
| pos (x: Positive).