fact: Fixpoint N_of_uint_acc (d : Decimal.uint) (acc : N) : N := match d with | Decimal.Nil => acc | Decimal.D0 d => N_of_uint_acc d (acc * 10) | Decimal.D1 d => N_of_uint_acc d (acc * 10 + 1) | Decimal.D2 d => N_of_uint_acc d (acc * 10 + 2) | Decimal.D3 d => N_of_uint_acc d (acc * 10 + 3) | Decimal.D4 d => N_of_uint_acc d (acc * 10 + 4) | Decimal.D5 d => N_of_uint_acc d (acc * 10 + 5) | Decimal.D6 d => N_of_uint_acc d (acc * 10 + 6) | Decimal.D7 d => N_of_uint_acc d (acc * 10 + 7) | Decimal.D8 d => N_of_uint_acc d (acc * 10 + 8) | Decimal.D9 d => N_of_uint_acc d (acc * 10 + 9) end.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)