fact: Fixpoint of_uint_acc (d:Decimal.uint)(acc:positive) := match d with | Decimal.Nil => acc | Decimal.D0 l => of_uint_acc l (mul ten acc) | Decimal.D1 l => of_uint_acc l (add 1 (mul ten acc)) | Decimal.D2 l => of_uint_acc l (add 1~0 (mul ten acc)) | Decimal.D3 l => of_uint_acc l (add 1~1 (mul ten acc)) | Decimal.D4 l => of_uint_acc l (add 1~0~0 (mul ten acc)) | Decimal.D5 l => of_uint_acc l (add 1~0~1 (mul ten acc)) | Decimal.D6 l => of_uint_acc l (add 1~1~0 (mul ten acc)) | Decimal.D7 l => of_uint_acc l (add 1~1~1 (mul ten acc)) | Decimal.D8 l => of_uint_acc l (add 1~0~0~0 (mul ten acc)) | Decimal.D9 l => of_uint_acc l (add 1~0~0~1 (mul ten acc)) end.
imports: BinNums