pub exec fn exec_mul<T: ExecSpecFixedWidthArith>(a: T, b: T) -> res : TExpand description
ensures
res == a.spec_fixed_mul(b),pub exec fn exec_mul<T: ExecSpecFixedWidthArith>(a: T, b: T) -> res : Tres == a.spec_fixed_mul(b),