f package:sbv

Uninterpreted function in the theorem

An uninterpreted function

Declare an uninterpreted function that works over Q's

Helper type synonym

Unique length used for firstified higher-order function names

Compute the floating point absolute value.

Add two floating point values, using the given rounding mode

Divide two floating point values, using the given rounding mode

Fused-multiply-add three floating point values, using the given rounding mode. fpFMA x y z = x*y+z but with only one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since Haskell lacks an FMA implementation.

Make from an integer value.

Are the two given floats exactly the same. That is, NaN will compare equal to itself, +0 will not compare equal to -0 etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use .==.)

Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.)

Is the floating-point number a NaN value?

Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not.

Is the floating point number -0?

Is the floating-point number a normal value. (i.e., not denormalized.)

Is the floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed.

Is the floating-point number positive? Note that +0 satisfies this predicate but -0 does not.

Is the floating point number +0?

Is the floating-point number a subnormal value. (Also known as denormal.)

Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.)

Compute the maximum of two floats, respects infinity and NaN values

Compute the minimum of two floats, respects infinity and NaN values

Multiply two floating point values, using the given rounding mode