fact: Definition ascii_of_pos : positive -> ascii := let loop := fix loop n p := match n with | O => zero | S n' => match p with | xH => one | xI p' => shift true (loop n' p') | xO p' => shift false (loop n' p') end end in loop 8.
imports: Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte