fact: Fixpoint of_pos (p : positive) (rest : string) : string := match p with | 1 => String "1" rest | 2 => String "2" rest | 3 => String "3" rest | 4 => String "4" rest | 5 => String "5" rest | 6 => String "6" rest | 7 => String "7" rest | p'~0~0~0 => of_pos p' (String "0" rest) | p'~0~0~1 => of_pos p' (String "1" rest) | p'~0~1~0 => of_pos p' (String "2" rest) | p'~0~1~1 => of_pos p' (String "3" rest) | p'~1~0~0 => of_pos p' (String "4" rest) | p'~1~0~1 => of_pos p' (String "5" rest) | p'~1~1~0 => of_pos p' (String "6" rest) | p'~1~1~1 => of_pos p' (String "7" rest) end.
imports: Ascii String BinNums