# This is Python def double(x: int) -> int: return x * 2