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