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

Subtraction of two extended fixed-point numbers.

Equations

• e_sub mode a b = e_add mode a (e_neg b)

def subfixed {e s : Nat} (a b : PackedFloat e s) (mode : RoundingMode) : PackedFloat e s

Subtraction of two floating-point numbers.

Implemented entirely within EFixedPoint using e_sub.

Equations

• subfixed a b mode = round e s mode (e_sub mode a.toEFixed b.toEFixed)

def sub {e s : Nat} (a b : PackedFloat e s) (mode : RoundingMode) : PackedFloat e s

Subtraction of two floating-point numbers.

Implemented as a negation followed by an addition.

Equations

• sub a b mode = add a (neg b) mode