fact: Fixpoint pos_of_uint_acc (d : Decimal.uint) (acc : Pos) := match d with | Decimal.Nil => acc | Decimal.D0 l => pos_of_uint_acc l (pos_mul ten acc) | Decimal.D1 l => pos_of_uint_acc l (pos_add 1 (pos_mul ten acc)) | Decimal.D2 l => pos_of_uint_acc l (pos_add 1~0 (pos_mul ten acc)) | Decimal.D3 l => pos_of_uint_acc l (pos_add 1~1 (pos_mul ten acc)) | Decimal.D4 l => pos_of_uint_acc l (pos_add 1~0~0 (pos_mul ten acc)) | Decimal.D5 l => pos_of_uint_acc l (pos_add 1~0~1 (pos_mul ten acc)) | Decimal.D6 l => pos_of_uint_acc l (pos_add 1~1~0 (pos_mul ten acc)) | Decimal.D7 l => pos_of_uint_acc l (pos_add 1~1~1 (pos_mul ten acc)) | Decimal.D8 l => pos_of_uint_acc l (pos_add 1~0~0~0 (pos_mul ten acc)) | Decimal.D9 l => pos_of_uint_acc l (pos_add 1~0~0~1 (pos_mul ten acc)) end.
imports: Basics.Overture Basics.Tactics Basics.Decidable Spaces.Nat.Core