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

Multiplication of two fixed-point numbers.

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)

Multiplication of two extended fixed-point numbers.

Equations

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

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

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

Implemented using e_mul, by conversion to extended fixed-point numbers.

Equations

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

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

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

A bit-blastable version of multiplication, without using e_mul.

Equations

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

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

Doubles the given floating point number, rounding to infinity if applicable.

Equations

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