# The name of this type starts with a digit, which is not allowed

@sealed