pub open spec fn decimal2(bytes: Seq<u8>, pos: usize) -> u8
{ ((bytes[pos as int] - ASCII_0) * 10 + (bytes[pos as int + 1] - ASCII_0)) as u8 }