fact: Fixpoint of_lu (d:uint) : N := match d with | Nil => 0 | D0 d => 0x10 * of_lu d | D1 d => 0x1 + 0x10 * of_lu d | D2 d => 0x2 + 0x10 * of_lu d | D3 d => 0x3 + 0x10 * of_lu d | D4 d => 0x4 + 0x10 * of_lu d | D5 d => 0x5 + 0x10 * of_lu d | D6 d => 0x6 + 0x10 * of_lu d | D7 d => 0x7 + 0x10 * of_lu d | D8 d => 0x8 + 0x10 * of_lu d | D9 d => 0x9 + 0x10 * of_lu d | Da d => 0xa + 0x10 * of_lu d | Db d => 0xb + 0x10 * of_lu d | Dc d => 0xc + 0x10 * of_lu d | Dd d => 0xd + 0x10 * of_lu d | De d => 0xe + 0x10 * of_lu d | Df d => 0xf + 0x10 * of_lu d end.
imports: Hexadecimal HexadecimalFacts PArith NArith