I noticed a minor issue with the definition of the square root operator - it implies that the square root of negative 0 is a NaN:
- If z is a NaN, then return an element of nans_N{z}.
- Else if z has a negative sign, then return an element of nans_N{}.
- Else if z is positive infinity, then return positive infinity.
- Else if z is a zero, then return that zero.
- Else return the square root of z.
Note that this is a contradiction with the formal notation that follows (and which specifies that the result is negative 0).