// ... but in the header, we give another definition,
// the one for a 128 bit int.
typedef __int128_t int128;