On writing type size in its name
Since number type sizes are powers of 2, I propose to denote a number type of size 2**N by int${N}. int7 is much shorter than, say, int128. (The word int is not important here. Replace it with i, Word, or whatever you want.)