def f_add {w e : Nat} (mode : RoundingMode) (a b : FixedPoint w e) : FixedPoint (w + 1) e

Addition of two fixed-point numbers.

When the sum is zero, the sign of the zero is dependent on the provided rounding mode.

Equations

• One or more equations did not get rendered due to their size.

def e_add {w e : Nat} (mode : RoundingMode) (a b : EFixedPoint w e) : EFixedPoint (w + 1) e

Addition of two extended fixed-point numbers.

When the sum is zero, the sign of the zero is dependent on the provided rounding mode.

Equations

• One or more equations did not get rendered due to their size.

def add {e s : Nat} (he : 0 < e) (a b : PackedFloat e s) (mode : RoundingMode) : PackedFloat e s

Addition of two floating point numbers, rounded to a floating point number using the provided rounding mode.

Equations

• add he a b mode = round e s mode (e_add mode (a.toEFixed he) (b.toEFixed he))