[Python-ideas] float('∞')=float('inf')