fact: Fixpoint positive_of_digits (l : list bool) (p : positive) : positive := match l with | [] => p | b :: l' => if b then xI (positive_of_digits l' p) else xO (positive_of_digits l' p) end.
imports: Coq(ZArith) Coq(FMapInterface FMapPositive) Coq(FMapList FMapFacts) Coq(String Ascii List) StructTact(StructTactics StringOrders)