%% It is more efficient to implement successor in terms of
%% (binary) addition, while it is easier to specify addition
%% in terms of successor than in terms of binary addition.
%% Thus, the structure of the implementation differs from
%% the structure of the specification:
Num_Monoid -> |
{ Num_Monoid then op succ(n:Num):Num=n+1 } |
%% We have now that Efficient_Add_Num is a refinement of Add_Num.