The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

to_nnreal x returns x if it is real, otherwise 0.

to_real x returns x if it is real, 0 otherwise.

of_real x returns x if it is nonnegative, 0 otherwise.