function print_u64_hex

fn print_u64_hex(val: u64) { .. }