Fixes #4 : attribute __name__ of class Number is "Number", not "$$Number"