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} (he : 0 < e) (a : PackedFloat e s) (mode : RoundingMode) : PackedFloat e s

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

Equations

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

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 }

theorem f_neg_involutive (a : FixedPoint 16 8) : f_neg (f_neg a) = a

theorem e_neg_involutive (a : EFixedPoint 16 8) : (e_neg (e_neg a)).equal_denotation a = true

theorem negfixed_eq_neg (a : PackedFloat 5 2) (m : RoundingMode) : negfixed ⋯ a m = neg a

negfixed and neg implement the same function.

theorem neg_involutive {e s : Nat} (a : PackedFloat e s) (h : ¬a.isNaN = true) : neg (neg a) = a

Applying neg twice gives you the identity.