[Python-ideas] int()