def f_neg {w e : Nat} (a : FixedPoint w e) : FixedPoint w e

Negate the fixed point number

Equations

• f_neg a = { sign := !a.sign, val := a.val, hExOffset := ⋯ }

def e_neg {w e : Nat} (a : EFixedPoint w e) : EFixedPoint w e

Negate the extended fixed point number

Equations

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

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

Negate a floating-point number, by conversion to a fixed-point number.

Equations

• negfixed a mode = round e s mode (e_neg a.toEFixed)

def neg {e s : Nat} (a : PackedFloat e s) : PackedFloat e s

Negate a floating-point number, by flipping the sign bit.

This implements the same function as negfixed, but is much simpler.

Equations

• neg a = if a.isNaN = true then PackedFloat.getNaN e s else { sign := !a.sign, ex := a.ex, sig := a.sig }

def abs {e s : Nat} (a : PackedFloat e s) : PackedFloat e s

Equations

• abs a = if a.isNaN = true then PackedFloat.getNaN e s else { sign := false, ex := a.ex, sig := a.sig }