fact: Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) := match d with | Decimal.Nil => acc | Decimal.D0 d => of_uint_acc d (tail_mul ten acc) | Decimal.D1 d => of_uint_acc d (S (tail_mul ten acc)) | Decimal.D2 d => of_uint_acc d (S (S (tail_mul ten acc))) | Decimal.D3 d => of_uint_acc d (S (S (S (tail_mul ten acc)))) | Decimal.D4 d => of_uint_acc d (S (S (S (S (tail_mul ten acc))))) | Decimal.D5 d => of_uint_acc d (S (S (S (S (S (tail_mul ten acc)))))) | Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (tail_mul ten acc))))))) | Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc)))))))) | Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc))))))))) | Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))) end.
imports: Notations Logic Datatypes