def f_mul {v e w f : Nat} (a : FixedPoint v e) (b : FixedPoint w f) : FixedPoint (v + w) (e + f)

Equations

• f_mul a b = { sign := a.sign ^^ b.sign, val := BitVec.setWidth' ⋯ a.val * BitVec.setWidth' ⋯ b.val, hExOffset := ⋯ }

def e_mul {v e w f : Nat} (a : EFixedPoint v e) (b : EFixedPoint w f) : EFixedPoint (v + w) (e + f)

Equations

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

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

Equations

• mulfixed he a b m = round e s m (e_mul (a.toEFixed he) (b.toEFixed he))

theorem f_mul_comm (a b : FixedPoint 34 16) : f_mul a b = f_mul b a

theorem e_mul_comm (a b : EFixedPoint 34 16) : e_mul a b = e_mul b a

theorem mulfixed_comm (a b : PackedFloat 5 2) (m : RoundingMode) : mulfixed ⋯ a b m = mulfixed ⋯ b a m

def mul {e s : Nat} (a b : PackedFloat e s) (m : RoundingMode) : PackedFloat e s

Equations

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

theorem mul_comm (a b : PackedFloat 5 2) (m : RoundingMode) : mul a b m = mul b a m

theorem mul_one_is_id (a : PackedFloat 5 2) (m : RoundingMode) (ha : ¬a.isNaN = true) : mul a oneE5M2 m = a