fact: Fixpoint of_hex_uint (d:Hexadecimal.uint) : N := match d with | Hexadecimal.Nil => N0 | Hexadecimal.D0 l => of_hex_uint l | Hexadecimal.D1 l => Npos (of_hex_uint_acc l 1) | Hexadecimal.D2 l => Npos (of_hex_uint_acc l 1~0) | Hexadecimal.D3 l => Npos (of_hex_uint_acc l 1~1) | Hexadecimal.D4 l => Npos (of_hex_uint_acc l 1~0~0) | Hexadecimal.D5 l => Npos (of_hex_uint_acc l 1~0~1) | Hexadecimal.D6 l => Npos (of_hex_uint_acc l 1~1~0) | Hexadecimal.D7 l => Npos (of_hex_uint_acc l 1~1~1) | Hexadecimal.D8 l => Npos (of_hex_uint_acc l 1~0~0~0) | Hexadecimal.D9 l => Npos (of_hex_uint_acc l 1~0~0~1) | Hexadecimal.Da l => Npos (of_hex_uint_acc l 1~0~1~0) | Hexadecimal.Db l => Npos (of_hex_uint_acc l 1~0~1~1) | Hexadecimal.Dc l => Npos (of_hex_uint_acc l 1~1~0~0) | Hexadecimal.Dd l => Npos (of_hex_uint_acc l 1~1~0~1) | Hexadecimal.De l => Npos (of_hex_uint_acc l 1~1~1~0) | Hexadecimal.Df l => Npos (of_hex_uint_acc l 1~1~1~1) end.
imports: BinNums