fact: Fixpoint int_of_decimal_uint (d : Decimal.uint) : Int := match d with | Decimal.Nil => zero | Decimal.D0 l => int_of_decimal_uint l | Decimal.D1 l => pos (pos_of_uint_acc l 1) | Decimal.D2 l => pos (pos_of_uint_acc l 1~0) | Decimal.D3 l => pos (pos_of_uint_acc l 1~1) | Decimal.D4 l => pos (pos_of_uint_acc l 1~0~0) | Decimal.D5 l => pos (pos_of_uint_acc l 1~0~1) | Decimal.D6 l => pos (pos_of_uint_acc l 1~1~0) | Decimal.D7 l => pos (pos_of_uint_acc l 1~1~1) | Decimal.D8 l => pos (pos_of_uint_acc l 1~0~0~0) | Decimal.D9 l => pos (pos_of_uint_acc l 1~0~0~1) end.
imports: Basics Spaces.Pos.Core