Missing DV_PROPORTION validity rule?

Hi, I’m adding support to more datatypes to EHRServer and was surprised that the DV_PROPORTION specs doesn’t define that the denominator should be != 0.

Is this on purpose?
Is infinite a valid value for DV_PROPORTION.magnitude()?
Or is just a missing validity rule?

thanks!