Definition u64 := BiU64.
