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