Constant JSVAL_TAG_MAX_DOUBLE 

const JSVAL_TAG_MAX_DOUBLE: u32 = 0x1FFF0u32;